val to_ilog_idx (logs: verifiable_logs) (i: nat{i < n_threads_v})
    : GTot (l: i_log{GT.verifiable (i, l)})
val to_ilog_idx (logs: verifiable_logs) (i: nat{i < n_threads_v})
    : GTot (l: i_log{GT.verifiable (i, l)})
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
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
/
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 -> i: Prims.nat{i < Zeta.Steel.GlobalRel.n_threads_v}
  -> Prims.GTot (l: Zeta.Steel.Rel.i_log{Zeta.Generic.Thread.verifiable (i, l)})
Zeta.Steel.GlobalRel.verifiable_logs Prims.nat Prims.b2t Prims.op_LessThan Zeta.Steel.GlobalRel.n_threads_v Zeta.GenericVerifier.thread_id Zeta.GenericVerifier.verifier_log Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg Zeta.Steel.Rel.i_log Zeta.Generic.Thread.verifiable FStar.Pervasives.Native.Mktuple2 Zeta.Steel.ThreadRel.i_verifiable_log Zeta.Steel.ThreadRel.to_ilog Zeta.Steel.ThreadRel.valid_tsm Zeta.Steel.ApplicationTypes.tid Zeta.Steel.ThreadStateModel.log Prims.l_and Prims.eq2 FStar.Seq.Base.seq Zeta.Steel.LogEntry.Types.log_entry Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__processed_entries Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__thread_id Zeta.Steel.Thread.to_tsm Zeta.Steel.Thread.verifiable_log Zeta.Steel.GlobalRel.index FStar.UInt16.t FStar.UInt16.uint_to_t
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