val is_epoch_verified : tsm: Zeta.Steel.ThreadStateModel.thread_state_model -> eid: Zeta.Steel.ThreadStateModel.epoch_id
  -> Prims.GTot Prims.bool
let is_epoch_verified (tsm:M.thread_state_model) (eid:M.epoch_id) =
  not tsm.failed &&
  not (M.epoch_greater_than_last_verified_epoch tsm.last_verified_epoch eid)
module Zeta.Steel.AggregateEpochHashes

open FStar.Ghost
open Steel.ST.Util
module A = Steel.ST.Array
module R = Steel.ST.Reference
module G = Steel.ST.GhostReference
module Lock = Steel.ST.CancellableSpinLock
open Zeta.Steel.ApplicationTypes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
open Zeta.Steel.FormatsManual
module EpochMap = Zeta.Steel.EpochMap
module T = Zeta.Steel.FormatsManual
module M = Zeta.Steel.ThreadStateModel
module HA = Zeta.Steel.HashAccumulator
open Zeta.Steel.Util
module MR = Steel.ST.MonotonicReference
module TLM = Zeta.Steel.ThreadLogMap
open Zeta.Steel.EpochHashes

#push-options "--ide_id_info_off"

let tid_bitmap = Seq.lseq bool (U32.v n_threads)
let epoch_hashes_repr = EpochMap.repr M.epoch_hash
let epoch_bitmaps_repr = EpochMap.repr tid_bitmap

let all_epoch_hashes = EpochMap.tbl epoch_hash_perm

let epoch_tid_bitmaps =
  EpochMap.tbl #(larray bool n_threads)
               #tid_bitmap
               (fun i -> array_pts_to)
/
Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadLogMap.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.EpochMap.fsti.checked Zeta.Steel.EpochHashes.fst.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.SeqAux.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.MonotonicReference.fsti.checked Steel.ST.GhostReference.fsti.checked Steel.ST.CancellableSpinLock.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
Zeta.Steel.AggregateEpochHashes.fsti
tsm: Zeta.Steel.ThreadStateModel.thread_state_model -> eid: Zeta.Steel.ThreadStateModel.epoch_id
  -> Prims.GTot Prims.bool
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ThreadStateModel.epoch_id Prims.op_AmpAmp Prims.op_Negation Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Zeta.Steel.ThreadStateModel.epoch_greater_than_last_verified_epoch Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_verified_epoch Prims.bool
let is_epoch_verified (tsm: M.thread_state_model) (eid: M.epoch_id) =
  
not tsm.failed && not (M.epoch_greater_than_last_verified_epoch tsm.last_verified_epoch eid)