val hash:ETbl.hash_fn M.epoch_id
val hash:ETbl.hash_fn M.epoch_id
let hash : ETbl.hash_fn M.epoch_id = fun eid -> SizeT.uint32_to_sizet eid
module Zeta.Steel.EpochMap

module G = FStar.Ghost
module U32 = FStar.UInt32

open Steel.FractionalPermission
open Steel.Memory
open Steel.ST.Effect.Ghost
open Steel.ST.Effect.Atomic
open Steel.ST.Effect
open Steel.ST.Util
module ZSU = Zeta.Steel.Util
module R = Steel.ST.Reference
module ETbl = Steel.ST.EphemeralHashtbl

module M = Zeta.Steel.ThreadStateModel
/
Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.EphemeralHashtbl.fsti.checked Steel.ST.Effect.Ghost.fsti.checked Steel.ST.Effect.Atomic.fsti.checked Steel.ST.Effect.fsti.checked Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.SizeT.fsti.checked FStar.Pervasives.fsti.checked FStar.PartialMap.fsti.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.EpochMap.fst
Steel.ST.EphemeralHashtbl.hash_fn Zeta.Steel.ThreadStateModel.epoch_id
Zeta.Steel.ThreadStateModel.epoch_id FStar.SizeT.uint32_to_sizet Steel.ST.EphemeralHashtbl.us
let hash:ETbl.hash_fn M.epoch_id =
  
fun eid -> SizeT.uint32_to_sizet eid