val full_perm : t: Zeta.Steel.EpochMap.tbl vp -> default_value: c -> m: Zeta.Steel.EpochMap.repr c
  -> Steel.Effect.Common.vprop
let full_perm (#v:Type)
              (#c:Type)
              (#vp:M.epoch_id -> v -> c -> vprop)
              (t:tbl vp)
              (default_value: c)              
              ([@@@smt_fallback] m:repr c)
  = perm t default_value m empty_borrows
module Zeta.Steel.EpochMap
open Steel.ST.Util
open Zeta.Steel.Util
module M = Zeta.Steel.ThreadStateModel
module G = FStar.Ghost
module Set = FStar.Set
module Map = FStar.Map
module U32 = FStar.UInt32

val tbl (#v:Type0)
        (#c:Type0) 
        (vp:M.epoch_id -> v -> c -> vprop)
    : Type0

let repr (a:Type)
  : Type0
  = m:Map.t M.epoch_id a {
      Map.domain m `Set.equal` Set.complement Set.empty
    }

let borrows (a:Type)
  : Type0
  = FStar.PartialMap.t M.epoch_id a

let empty_borrows #a
  : borrows a
  = PartialMap.empty M.epoch_id a

(*
  One representation for this is a pair containing an
    1. an EHT
    2. a high-water-mark, a concrete epoch_id ref

  with an invariant stating that for all 
  
    epoch_id greater than the high-water-mark
    the value of the map associated with that epoch id
    is the default_value

  Additionally, if an epoch `i` is in the borrows set, 
  then `i` is less than or equal to the high water mark
*)
val perm (#v:Type)
         (#c:Type)
         (#vp:M.epoch_id -> v -> c -> vprop)
         (t:tbl vp)
         (default_value: c)
         ([@@@smt_fallback] m:repr c)
         ([@@@smt_fallback] b:borrows v)
  : vprop
/
Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Steel.ST.Util.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.PartialMap.fsti.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.EpochMap.fsti
t: Zeta.Steel.EpochMap.tbl vp -> default_value: c -> m: Zeta.Steel.EpochMap.repr c
  -> Steel.Effect.Common.vprop
Zeta.Steel.ThreadStateModel.epoch_id Steel.Effect.Common.vprop Zeta.Steel.EpochMap.tbl Zeta.Steel.EpochMap.repr Zeta.Steel.EpochMap.perm Zeta.Steel.EpochMap.empty_borrows
let full_perm
      (#v #c: Type)
      (#vp: (M.epoch_id -> v -> c -> vprop))
      (t: tbl vp)
      (default_value: c)
      ([@@@ smt_fallback]m: repr c)
     =
  
perm t default_value m empty_borrows