val empty : Zeta.MultiSet.mset Zeta.Steel.MultiSetHash.i_dom Zeta.Steel.MultiSetHash.mset_cmp
let empty = MS.empty #i_dom #mset_cmp
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

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

(* total ordering for mset_dom *)
let mset_cmp = MSD.ms_hashfn_dom_cmp app

(* the type of multisets we are interested in *)
let mset = MSD.mset_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
Zeta.MultiSet.mset Zeta.Steel.MultiSetHash.i_dom Zeta.Steel.MultiSetHash.mset_cmp
Zeta.MultiSet.empty Zeta.Steel.MultiSetHash.i_dom Zeta.Steel.MultiSetHash.mset_cmp
let empty =
  
MS.empty #i_dom #mset_cmp