val aggregate_epoch_hashes_seq_unit (s: Seq.seq M.epoch_hash)
    : Lemma (requires forall i. Seq.index s i == M.init_epoch_hash)
      (ensures aggregate_epoch_hashes_seq s == M.init_epoch_hash)
      (decreases Seq.length s)
val aggregate_epoch_hashes_seq_unit (s: Seq.seq M.epoch_hash)
    : Lemma (requires forall i. Seq.index s i == M.init_epoch_hash)
      (ensures aggregate_epoch_hashes_seq s == M.init_epoch_hash)
      (decreases Seq.length s)
let rec aggregate_epoch_hashes_seq_unit (s:Seq.seq M.epoch_hash)
  : Lemma
    (requires
      forall i. Seq.index s i == M.init_epoch_hash)
    (ensures
      aggregate_epoch_hashes_seq s == M.init_epoch_hash)
    (decreases Seq.length s)
  = if Seq.length s = 0 then ()
    else (
      let prefix, last = Seq.un_snoc s in
      Seq.un_snoc_snoc prefix last;
      calc (==) {
        aggregate_epoch_hashes_seq s;
        (==) {}
        aggregate_epoch_hash last (aggregate_epoch_hashes_seq prefix);
        (==) { aggregate_epoch_hash_unit (aggregate_epoch_hashes_seq prefix) }
        aggregate_epoch_hashes_seq prefix;
        (==) { aggregate_epoch_hashes_seq_unit prefix }
        M.init_epoch_hash;
      }
    )
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

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)
/
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
s: FStar.Seq.Base.seq Zeta.Steel.ThreadStateModel.epoch_hash
  -> FStar.Pervasives.Lemma
      (requires
        forall (i: Prims.nat{i < FStar.Seq.Base.length s}).
          FStar.Seq.Base.index s i == Zeta.Steel.ThreadStateModel.init_epoch_hash)
      (ensures
        Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hashes_seq s ==
        Zeta.Steel.ThreadStateModel.init_epoch_hash)
      (decreases FStar.Seq.Base.length s)
FStar.Seq.Base.seq Zeta.Steel.ThreadStateModel.epoch_hash Prims.op_Equality Prims.int FStar.Seq.Base.length Prims.bool FStar.Calc.calc_finish Prims.eq2 Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hashes_seq Zeta.Steel.ThreadStateModel.init_epoch_hash Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hash FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hash_unit Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hashes_seq_unit FStar.Seq.Properties.un_snoc_snoc FStar.Pervasives.Native.tuple2 FStar.Seq.Properties.snoc FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd FStar.Seq.Properties.un_snoc Prims.l_Forall Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.index FStar.Pervasives.pattern
let rec aggregate_epoch_hashes_seq_unit (s: Seq.seq M.epoch_hash)
    : Lemma (requires forall i. Seq.index s i == M.init_epoch_hash)
      (ensures aggregate_epoch_hashes_seq s == M.init_epoch_hash)
      (decreases Seq.length s) =
  
if Seq.length s = 0
then ()
else
  (let prefix, last = Seq.un_snoc s in
    Seq.un_snoc_snoc prefix last;
    calc ( == ) {
      aggregate_epoch_hashes_seq s;
      ( == ) { () }
      aggregate_epoch_hash last (aggregate_epoch_hashes_seq prefix);
      ( == ) { aggregate_epoch_hash_unit (aggregate_epoch_hashes_seq prefix) }
      aggregate_epoch_hashes_seq prefix;
      ( == ) { aggregate_epoch_hashes_seq_unit prefix }
      M.init_epoch_hash;
    })