val repr_to_eht_repr (#a: Type0) (m: repr a) : PartialMap.t M.epoch_id a
val repr_to_eht_repr (#a: Type0) (m: repr a) : PartialMap.t M.epoch_id a
let repr_to_eht_repr (#a:Type0) (m:repr a) : PartialMap.t M.epoch_id a =
  PartialMap.literal (fun x -> Some (Map.sel m x))
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

let high_water_mark = option M.epoch_id
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

//[@@CAbstractStruct] TODO restore after krml #247
noeq
type tbl #v #c vp = {
  etbl : ETbl.tbl #M.epoch_id #v #c vp hash;
  high : R.ref high_water_mark;
}
/
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
m: Zeta.Steel.EpochMap.repr a -> FStar.PartialMap.t Zeta.Steel.ThreadStateModel.epoch_id a
Zeta.Steel.EpochMap.repr FStar.PartialMap.literal Zeta.Steel.ThreadStateModel.epoch_id FStar.Pervasives.Native.Some FStar.Map.sel FStar.Pervasives.Native.option FStar.PartialMap.t
let repr_to_eht_repr (#a: Type0) (m: repr a) : PartialMap.t M.epoch_id a =
  
PartialMap.literal (fun x -> Some (Map.sel m x))