val related_msdom : s: Zeta.Steel.MultiSetHash.s_dom -> i: Zeta.Steel.MultiSetHash.i_dom -> Prims.logical
let related_msdom (s: s_dom) (i: i_dom)
  = let MSD.MHDom r t j = i in
    related_record s.r r /\
    related_timestamp s.t t /\
    related_tid s.tid j
module Zeta.Steel.MultiSetHash

(* This module defines the abstraction of multi-set hashing and relates it to Zeta.Steel.HashAccumulator *)

open Zeta.Steel.HashAccumulator
open Zeta.Steel.Rel

module AT = Zeta.Steel.ApplicationTypes
module MS = Zeta.MultiSet
module MSD = Zeta.MultiSetHashDomain
module TSM = Zeta.Steel.ThreadStateModel

let app = AT.aprm

(* multist domain *)
noeq
type s_dom = {
  r: s_record;
  t: s_timestamp;
  tid: s_tid;
}

(* multiset domain - spec level *)
let i_dom = MSD.ms_hashfn_dom app
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.MultiSet.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.MultiSetHash.fsti
s: Zeta.Steel.MultiSetHash.s_dom -> i: Zeta.Steel.MultiSetHash.i_dom -> Prims.logical
Zeta.Steel.MultiSetHash.s_dom Zeta.Steel.MultiSetHash.i_dom Zeta.Record.record Zeta.Steel.MultiSetHash.app Zeta.Time.timestamp Zeta.Thread.thread_id Prims.l_and Zeta.Steel.Rel.related_record Zeta.Steel.MultiSetHash.__proj__Mks_dom__item__r Zeta.Steel.Rel.related_timestamp Zeta.Steel.MultiSetHash.__proj__Mks_dom__item__t Zeta.Steel.Rel.related_tid Zeta.Steel.MultiSetHash.__proj__Mks_dom__item__tid Prims.logical
let related_msdom (s: s_dom) (i: i_dom) =
  
let MSD.MHDom r t j = i in
related_record s.r r /\ related_timestamp s.t t /\ related_tid s.tid j