val above_high_water_mark (h: high_water_mark) (e: M.epoch_id) : bool
val above_high_water_mark (h: high_water_mark) (e: M.epoch_id) : bool
let above_high_water_mark (h:high_water_mark) (e:M.epoch_id) : bool =
  match h with
  | None -> true
  | Some e0 -> e0 `U32.lt` e
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

inline_for_extraction
let hash : ETbl.hash_fn M.epoch_id = fun eid -> SizeT.uint32_to_sizet eid
/
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
h: Zeta.Steel.EpochMap.high_water_mark -> e: Zeta.Steel.ThreadStateModel.epoch_id -> Prims.bool
Zeta.Steel.EpochMap.high_water_mark Zeta.Steel.ThreadStateModel.epoch_id FStar.UInt32.lt Prims.bool
let above_high_water_mark (h: high_water_mark) (e: M.epoch_id) : bool =
  
match h with
| None -> true
| Some e0 -> e0 `U32.lt` e