val high_epoch_id_pred:
    #v: Type0 ->
    #c: Type0 ->
    default_value: c ->
    m: repr c ->
    b: borrows v ->
    r: R.ref high_water_mark ->
    high_water_mark
  -> vprop
val high_epoch_id_pred:
    #v: Type0 ->
    #c: Type0 ->
    default_value: c ->
    m: repr c ->
    b: borrows v ->
    r: R.ref high_water_mark ->
    high_water_mark
  -> vprop
let high_epoch_id_pred
  (#v #c:Type0)
  (default_value:c)
  (m:repr c)
  (b:borrows v)
  (r:R.ref high_water_mark)
  : high_water_mark -> vprop
  = fun e ->
    R.pts_to r full_perm e
      `star`
    pure (high_epoch_id_prop default_value m b 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

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;
}

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))

let high_epoch_id_prop
  (#v #c:Type0)
  (default_value:c)
  (m:repr c)
  (b:borrows v)
  (e:high_water_mark)
  : prop
  = (forall (e':M.epoch_id). above_high_water_mark e e' ==> Map.sel m e' == default_value) /\
    (forall (e':M.epoch_id). PartialMap.contains b e' ==>  not(above_high_water_mark e e'))
/
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

    default_value: c ->
    m: Zeta.Steel.EpochMap.repr c ->
    b: Zeta.Steel.EpochMap.borrows v ->
    r: Steel.ST.Reference.ref Zeta.Steel.EpochMap.high_water_mark ->
    _: Zeta.Steel.EpochMap.high_water_mark
  -> Steel.Effect.Common.vprop
Zeta.Steel.EpochMap.repr Zeta.Steel.EpochMap.borrows Steel.ST.Reference.ref Zeta.Steel.EpochMap.high_water_mark Steel.Effect.Common.star Steel.ST.Reference.pts_to Steel.FractionalPermission.full_perm Steel.ST.Util.pure Zeta.Steel.EpochMap.high_epoch_id_prop Steel.Effect.Common.vprop
let high_epoch_id_pred
      (#v #c: Type0)
      (default_value: c)
      (m: repr c)
      (b: borrows v)
      (r: R.ref high_water_mark)
    :  high_water_mark -> vprop =
  
fun e -> (R.pts_to r full_perm e) `star` (pure (high_epoch_id_prop default_value m b e))