val n_threads_v : FStar.UInt.uint_t FStar.UInt32.n
let n_threads_v = U32.v n_threads
module Zeta.Steel.GlobalRel

open Zeta.App
open Zeta.AppSimulate
open Zeta.Steel.ApplicationTypes
open Zeta.Steel.ThreadStateModel
open Zeta.Steel.MultiSetHash
open Zeta.Steel.Rel
open Zeta.Steel.ThreadRel
open Zeta.Steel.Thread

module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module GG = Zeta.Generic.Global
module HA = Zeta.Steel.HashAccumulator
module StT = Zeta.Steel.Thread
module AH = Zeta.Steel.AggregateEpochHashes

let index_ (logs: all_logs)  (t: tid)
  : tlog
  = let tv = U16.v t in
    (t, Seq.index logs tv)

let verifiable (logs: all_logs)
  = forall (t: tid). StT.verifiable (index_ logs t)

let verifiable_logs = l: all_logs {verifiable l}

let index (logs: verifiable_logs) (t: tid)
  : StT.verifiable_log
  = index_ logs t

let as_tid_logs (logs:all_logs)
  = Zeta.SeqAux.mapi #_ #(tid & log)
                     logs
                     (fun (i:Zeta.SeqAux.seq_index logs) -> (FStar.UInt16.uint_to_t i, Seq.index logs i))

(* all verifier threads succeed and have certified upto epmax *)
let verifiable_and_certified (logs: all_logs) (epmax: epoch_id)
  = verifiable logs /\
    (forall (eid: epoch_id). (U32.v eid <= U32.v epmax) ==> AH.epoch_is_certified (as_tid_logs logs) eid)
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRel.fsti.checked Zeta.Steel.Thread.fsti.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.MultiSetHash.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.AggregateEpochHashes.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Intermediate.Global.fsti.checked Zeta.Generic.Global.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.GlobalRel.fsti
FStar.UInt.uint_t FStar.UInt32.n
FStar.UInt32.v Zeta.Steel.ApplicationTypes.n_threads
let n_threads_v =
  
U32.v n_threads