val aggregate_epoch_hash_assoc (i j k: M.epoch_hash)
    : Lemma
    (aggregate_epoch_hash (aggregate_epoch_hash i j) k ==
      aggregate_epoch_hash i (aggregate_epoch_hash j k))
val aggregate_epoch_hash_assoc (i j k: M.epoch_hash)
    : Lemma
    (aggregate_epoch_hash (aggregate_epoch_hash i j) k ==
      aggregate_epoch_hash i (aggregate_epoch_hash j k))
let aggregate_epoch_hash_assoc (i j k:M.epoch_hash)
  : Lemma (aggregate_epoch_hash (aggregate_epoch_hash i j) k ==
           aggregate_epoch_hash i (aggregate_epoch_hash j k))
  = HA.aggregate_hashes_associative i.hadd j.hadd k.hadd;
    HA.aggregate_hashes_associative i.hevict j.hevict k.hevict
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)

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)

let all_threads_epoch_hashes =
  Seq.lseq epoch_hashes_repr (U32.v n_threads)

let aggregate_epoch_hash (e0 e1:M.epoch_hash)
  : M.epoch_hash
  = { hadd = HA.aggregate_hashes e0.hadd e1.hadd;
      hevict = HA.aggregate_hashes e0.hevict e1.hevict}

let aggregate_epoch_hash_unit (i:M.epoch_hash)
  : Lemma (aggregate_epoch_hash M.init_epoch_hash i == i)
          [SMTPat (aggregate_epoch_hash M.init_epoch_hash i)]
  = HA.initial_hash_unit i.hadd;
    HA.initial_hash_unit i.hevict

let aggregate_epoch_hash_comm (i j:M.epoch_hash)
  : Lemma (aggregate_epoch_hash i j == aggregate_epoch_hash j i)
  = HA.aggregate_hashes_commutative i.hadd j.hadd;
    HA.aggregate_hashes_commutative i.hevict j.hevict
/
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

    i: Zeta.Steel.ThreadStateModel.epoch_hash ->
    j: Zeta.Steel.ThreadStateModel.epoch_hash ->
    k: Zeta.Steel.ThreadStateModel.epoch_hash
  -> FStar.Pervasives.Lemma
    (ensures
      Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hash (Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hash
            i
            j)
        k ==
      Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hash i
        (Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hash j k))
Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.HashAccumulator.aggregate_hashes_associative Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hevict Prims.unit Zeta.Steel.ThreadStateModel.__proj__Mkepoch_hash__item__hadd Prims.l_True Prims.squash Prims.eq2 Zeta.Steel.AggregateEpochHashes.aggregate_epoch_hash Prims.Nil FStar.Pervasives.pattern
let aggregate_epoch_hash_assoc (i j k: M.epoch_hash)
    : Lemma
    (aggregate_epoch_hash (aggregate_epoch_hash i j) k ==
      aggregate_epoch_hash i (aggregate_epoch_hash j k)) =
  
HA.aggregate_hashes_associative i.hadd j.hadd k.hadd;
HA.aggregate_hashes_associative i.hevict j.hevict k.hevict