val aggregate_all_threads_epoch_hashes_emp: Prims.unit
  -> Lemma
    (forall (e: M.epoch_id).
        aggregate_all_threads_epoch_hashes e empty_all_processed_entries == M.init_epoch_hash)
val aggregate_all_threads_epoch_hashes_emp: Prims.unit
  -> Lemma
    (forall (e: M.epoch_id).
        aggregate_all_threads_epoch_hashes e empty_all_processed_entries == M.init_epoch_hash)
let aggregate_all_threads_epoch_hashes_emp ()
  : Lemma (forall (e:M.epoch_id).
             aggregate_all_threads_epoch_hashes e empty_all_processed_entries ==
             M.init_epoch_hash)
  = assert (forall tid. Map.equal (thread_contrib_of_log (U16.uint_to_t tid) (snd (Seq.index empty_all_processed_entries tid)))
                             (Map.const M.init_epoch_hash));
    let all_init = (Seq.create (U32.v n_threads) (Map.const M.init_epoch_hash)) in
    assert (Seq.equal (all_threads_epoch_hashes_of_logs empty_all_processed_entries)
                      all_init);
    introduce forall (e:M.epoch_id).
                aggregate_all_threads_epoch_hashes e empty_all_processed_entries ==
                M.init_epoch_hash
    with (
      calc (==) {
        aggregate_all_threads_epoch_hashes e empty_all_processed_entries;
       (==) {}
        aggregate_epoch_hashes_seq (Zeta.SeqAux.map (fun (s:epoch_hashes_repr) -> Map.sel s e) all_init);
       (==) { aggregate_epoch_hashes_seq_unit (Zeta.SeqAux.map (fun (s:epoch_hashes_repr) -> Map.sel s e) all_init) }
        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)

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;
      }
    )
/
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
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      forall (e: Zeta.Steel.ThreadStateModel.epoch_id).
        Zeta.Steel.AggregateEpochHashes.aggregate_all_threads_epoch_hashes e
          (FStar.Ghost.reveal Zeta.Steel.AggregateEpochHashes.empty_all_processed_entries) ==
        Zeta.Steel.ThreadStateModel.init_epoch_hash)
Prims.unit FStar.Classical.Sugar.forall_intro Zeta.Steel.ThreadStateModel.epoch_id Prims.eq2 Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.AggregateEpochHashes.aggregate_all_threads_epoch_hashes FStar.Ghost.reveal Zeta.Steel.AggregateEpochHashes.all_processed_entries Zeta.Steel.AggregateEpochHashes.empty_all_processed_entries Zeta.Steel.ThreadStateModel.init_epoch_hash FStar.Calc.calc_finish Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hashes_seq Zeta.SeqAux.map Zeta.Steel.AggregateEpochHashes.epoch_hashes_repr FStar.Map.sel FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hashes_seq_unit Prims._assert FStar.Seq.Base.equal Zeta.Steel.AggregateEpochHashes.all_threads_epoch_hashes_of_logs FStar.Seq.Base.seq FStar.Seq.Base.create FStar.UInt32.v Zeta.Steel.ApplicationTypes.n_threads FStar.Map.const Prims.l_Forall Prims.int Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThan FStar.Seq.Base.length FStar.Pervasives.Native.tuple2 Zeta.Steel.ApplicationTypes.tid Zeta.Steel.AggregateEpochHashes.log FStar.UInt.size FStar.UInt16.n FStar.Map.equal Zeta.Steel.AggregateEpochHashes.thread_contrib_of_log FStar.UInt16.uint_to_t FStar.Pervasives.Native.snd FStar.Seq.Base.index Prims.l_True FStar.Pervasives.pattern
let aggregate_all_threads_epoch_hashes_emp ()
    : Lemma
    (forall (e: M.epoch_id).
        aggregate_all_threads_epoch_hashes e empty_all_processed_entries == M.init_epoch_hash) =
  
assert (forall tid.
      Map.equal (thread_contrib_of_log (U16.uint_to_t tid)
            (snd (Seq.index empty_all_processed_entries tid)))
        (Map.const M.init_epoch_hash));
let all_init = (Seq.create (U32.v n_threads) (Map.const M.init_epoch_hash)) in
assert (Seq.equal (all_threads_epoch_hashes_of_logs empty_all_processed_entries) all_init);
introduce forall (e: M.epoch_id) . aggregate_all_threads_epoch_hashes e empty_all_processed_entries ==
M.init_epoch_hash
with (calc ( == ) {
    aggregate_all_threads_epoch_hashes e empty_all_processed_entries;
    ( == ) { () }
    aggregate_epoch_hashes_seq (Zeta.SeqAux.map (fun (s: epoch_hashes_repr) -> Map.sel s e) all_init
      );
    ( == ) { aggregate_epoch_hashes_seq_unit (Zeta.SeqAux.map (fun (s: epoch_hashes_repr) ->
              Map.sel s e)
          all_init) }
    M.init_epoch_hash;
  })