val to_ilog (logs: verifiable_logs)
  : GTot (i_logs: i_verifiable_logs {Seq.length i_logs = n_threads_v})
val to_ilog (logs: verifiable_logs)
  : GTot (i_logs: i_verifiable_logs {Seq.length i_logs = n_threads_v})
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)
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
/
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
logs: Zeta.Steel.GlobalRel.verifiable_logs
  -> Prims.GTot
    (i_logs:
      Zeta.Steel.GlobalRel.i_verifiable_logs
        {FStar.Seq.Base.length i_logs = Zeta.Steel.GlobalRel.n_threads_v})
Zeta.Steel.GlobalRel.verifiable_logs FStar.Seq.Base.init_ghost Zeta.Steel.Rel.i_log Zeta.Steel.GlobalRel.n_threads_v Prims.nat Prims.b2t Prims.op_LessThan Zeta.Steel.GlobalRel.to_ilog_idx Zeta.Steel.GlobalRel.i_verifiable_logs Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n FStar.Seq.Base.length Zeta.GenericVerifier.verifier_log Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg
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)