val empty_all_processed_entries:Ghost.erased all_processed_entries
val empty_all_processed_entries:Ghost.erased all_processed_entries
let empty_all_processed_entries : Ghost.erased all_processed_entries =
  Seq.init #(tid & log) (U32.v n_threads) (fun i -> U16.uint_to_t i, Seq.empty)
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
module SA = Zeta.SeqAux
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

inline_for_extraction
let max_epoch_lag = 32ul
let all_hashes_size : n:U32.t{U32.v n > 0} = max_epoch_lag
let tid_bitmaps_size : n:U32.t{U32.v n > 0} = max_epoch_lag
/
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.Loops.Util.fsti.checked Steel.ST.GhostReference.fsti.checked Steel.ST.CancellableSpinLock.fsti.checked Steel.ST.Array.Util.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.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PartialMap.fsti.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.Steel.AggregateEpochHashes.fst
FStar.Ghost.erased Zeta.Steel.AggregateEpochHashes.all_processed_entries
FStar.Ghost.hide Zeta.Steel.AggregateEpochHashes.all_processed_entries FStar.Seq.Base.init FStar.Pervasives.Native.tuple2 Zeta.Steel.ApplicationTypes.tid Zeta.Steel.AggregateEpochHashes.log FStar.UInt32.v Zeta.Steel.ApplicationTypes.n_threads Prims.nat Prims.b2t Prims.op_LessThan FStar.Pervasives.Native.Mktuple2 FStar.UInt16.uint_to_t FStar.Seq.Base.empty Zeta.Steel.LogEntry.Types.log_entry
let empty_all_processed_entries:Ghost.erased all_processed_entries =
  
Seq.init #(tid & log) (U32.v n_threads) (fun i -> U16.uint_to_t i, Seq.empty)