val i_dom : Type0
let i_dom = MSD.ms_hashfn_dom app
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;
}
/
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
Type0
Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.Steel.MultiSetHash.app
let i_dom =
  
MSD.ms_hashfn_dom app