val as_tid_logs : logs: Zeta.Steel.ThreadStateModel.all_logs
  -> t:
    FStar.Seq.Base.seq (Zeta.Steel.ApplicationTypes.tid * Zeta.Steel.ThreadStateModel.log)
      { FStar.Seq.Base.length logs == FStar.Seq.Base.length t /\
        (forall (i: Zeta.SeqAux.seq_index logs).
            FStar.Seq.Base.index t i == (FStar.UInt16.uint_to_t i, FStar.Seq.Base.index logs i)) }
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))
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
/
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
logs: Zeta.Steel.ThreadStateModel.all_logs
  -> t:
    FStar.Seq.Base.seq (Zeta.Steel.ApplicationTypes.tid * Zeta.Steel.ThreadStateModel.log)
      { FStar.Seq.Base.length logs == FStar.Seq.Base.length t /\
        (forall (i: Zeta.SeqAux.seq_index logs).
            FStar.Seq.Base.index t i == (FStar.UInt16.uint_to_t i, FStar.Seq.Base.index logs i)) }
Zeta.Steel.ThreadStateModel.all_logs Zeta.SeqAux.mapi Zeta.Steel.ThreadStateModel.log FStar.Pervasives.Native.tuple2 Zeta.Steel.ApplicationTypes.tid Zeta.SeqAux.seq_index FStar.Pervasives.Native.Mktuple2 FStar.UInt16.uint_to_t FStar.Seq.Base.index FStar.Seq.Base.seq Prims.l_and Prims.eq2 Prims.nat FStar.Seq.Base.length Prims.l_Forall
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))