val all_epoch_completed : ep: Zeta.Steel.ThreadStateModel.epoch_id ->
    tsms: FStar.Seq.Base.seq Zeta.Steel.ThreadStateModel.thread_state_model
  -> Prims.logical
let all_epoch_completed (ep: epoch_id) (tsms: Seq.seq thread_state_model)
  = forall (i:Zeta.SeqAux.seq_index tsms). AH.is_epoch_verified (Seq.index tsms i) ep
module Zeta.Steel.GlobalRel

open FStar.Classical
open Zeta.MultiSet.SSeq
module GT = Zeta.Generic.Thread
module TSM = Zeta.Steel.ThreadStateModel
module HA = Zeta.Steel.HashAccumulator
module MS = Zeta.MultiSet
module ThreadRel = Zeta.Steel.ThreadRel

let to_ilog_idx (logs: verifiable_logs) (i: nat{i < n_threads_v})
  : GTot (l:i_log {GT.verifiable (i,l)})
  = let t = U16.uint_to_t i in
    let tl = index logs t in
    let tsm = to_tsm tl in
    let (_,l) = to_ilog tsm in
    l

let to_ilog (logs: verifiable_logs)
  : GTot (i_logs: i_verifiable_logs {Seq.length i_logs = n_threads_v})
  = Seq.init_ghost n_threads_v (fun i -> to_ilog_idx logs i)

let all_app_fcrs_rel (ep: epoch_id) (logs: verifiable_logs)
  : Lemma (ensures (let s_fcrs = all_app_fcrs ep logs in
                    let i_logs = to_ilog logs in
                    let i_ep = lift_epoch ep in
                    let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in
                    s_fcrs = i_fcrs))
  = let s_fcrs = all_app_fcrs ep logs in
    let i_logs = to_ilog logs in
    let i_ep = lift_epoch ep in
    let i_fcrs = GG.app_fcrs_within_ep i_ep i_logs in

    let aux (i:_)
      : Lemma (ensures (Seq.index s_fcrs i == Seq.index i_fcrs i))
      = let t = U16.uint_to_t i in
        let tl = index logs t in
        assert(app_fcrs ep tl == Seq.index s_fcrs i);
        spec_rel_implies_same_fcrs ep tl;
        ()
    in
    forall_intro aux;
    assert(Seq.equal s_fcrs i_fcrs);
    ()

let aggregate_add_hash (logs: all_logs) (ep: epoch_id)
  : GTot hash_value_t
  = let aeh = AH.aggregate_all_threads_epoch_hashes ep (as_tid_logs logs) in
    aeh.hadd

let aggregate_evict_hash (logs: all_logs) (ep: epoch_id)
  : GTot hash_value_t
  = let aeh = AH.aggregate_all_threads_epoch_hashes ep (as_tid_logs logs) in
    aeh.hevict
  
let certified_epoch_aggregate_hashes_equal (logs: all_logs) (ep: epoch_id {AH.epoch_is_certified (as_tid_logs logs) ep})
  : Lemma (ensures (aggregate_add_hash logs ep == aggregate_evict_hash logs ep))
  = ()

let all_valid_tsms = tsms: Seq.seq thread_state_model
    { forall i. ThreadRel.valid (Seq.index tsms i) }
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRel.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.SSeq.fsti.checked Zeta.SeqAux.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.MultiSet.SSeq.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Generic.Thread.fsti.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
Zeta.Steel.GlobalRel.fst

    ep: Zeta.Steel.ThreadStateModel.epoch_id ->
    tsms: FStar.Seq.Base.seq Zeta.Steel.ThreadStateModel.thread_state_model
  -> Prims.logical
Zeta.Steel.ThreadStateModel.epoch_id FStar.Seq.Base.seq Zeta.Steel.ThreadStateModel.thread_state_model Prims.l_Forall Zeta.SeqAux.seq_index Prims.b2t Zeta.Steel.AggregateEpochHashes.is_epoch_verified FStar.Seq.Base.index Prims.logical
let all_epoch_completed (ep: epoch_id) (tsms: Seq.seq thread_state_model) =
  
forall (i: Zeta.SeqAux.seq_index tsms). AH.is_epoch_verified (Seq.index tsms i) ep