val epoch_hash_perm : k: Zeta.Steel.ThreadStateModel.epoch_id ->
    v: Zeta.Steel.EpochHashes.epoch_hashes_t ->
    c: Zeta.Steel.ThreadStateModel.epoch_hash
  -> Steel.Effect.Common.vprop
let epoch_hash_perm (k:M.epoch_id)
                    (v:epoch_hashes_t)
                    (c:M.epoch_hash) =
    HA.ha_val v.hadd c.hadd `star`
    HA.ha_val v.hevict c.hevict
module Zeta.Steel.EpochHashes
open Steel.ST.Util
open Zeta.Steel.Util
module M = Zeta.Steel.ThreadStateModel
module HA = Zeta.Steel.HashAccumulator


//[@@CAbstractStruct] TODO: Restore this after krml #247
noeq
type epoch_hashes_t = {
  hadd: HA.ha;
  hevict: HA.ha;
}
/
Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.HashAccumulator.fsti.checked Steel.ST.Util.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.EpochHashes.fst

    k: Zeta.Steel.ThreadStateModel.epoch_id ->
    v: Zeta.Steel.EpochHashes.epoch_hashes_t ->
    c: Zeta.Steel.ThreadStateModel.epoch_hash
  -> Steel.Effect.Common.vprop
Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.EpochHashes.epoch_hashes_t Zeta.Steel.ThreadStateModel.epoch_hash Steel.Effect.Common.star Zeta.Steel.HashAccumulator.ha_val Zeta.Steel.EpochHashes.__proj__Mkepoch_hashes_t__item__hadd Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hadd Zeta.Steel.EpochHashes.__proj__Mkepoch_hashes_t__item__hevict Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hevict Steel.Effect.Common.vprop
let epoch_hash_perm (k: M.epoch_id) (v: epoch_hashes_t) (c: M.epoch_hash) =
  
(HA.ha_val v.hadd c.hadd) `star` (HA.ha_val v.hevict c.hevict)