val thread_store_pre : tid: Prims.nat{tid < VConfig?.thread_count vcfg} ->
    il: Zeta.Intermediate.Interleave.verifiable_log vcfg ->
    i: Zeta.Generic.Interleave.seq_index il
  -> Prims.GTot (Zeta.Intermediate.Store.vstore vcfg)
let thread_store_pre (#vcfg:_) (tid: nat{tid < vcfg.thread_count}) (il: verifiable_log vcfg) (i: seq_index il)
  = let vs = thread_state_pre tid il i in
    vs.st
module Zeta.Intermediate.Interleave

open FStar.Seq
open Zeta.SeqAux
open Zeta.Interleave
open Zeta.Time
open Zeta.Intermediate.VerifierConfig
open Zeta.Intermediate.Store
open Zeta.Intermediate.Verifier
open Zeta.Intermediate.Logs
open Zeta.Intermediate.StateRel
open Zeta.Generic.Interleave

module I = Zeta.Interleave
module SA = Zeta.SeqAux
module GG = Zeta.Generic.Global
module GI = Zeta.Generic.Interleave
module HI = Zeta.High.Interleave
module IV = Zeta.Intermediate.Verifier
module IG = Zeta.Intermediate.Global

let ilog (vcfg: verifier_config) =
  Zeta.Generic.Interleave.ilog (int_verifier_spec vcfg) (vcfg.thread_count)

let verifiable_log (vcfg: verifier_config)
  = il: ilog vcfg {verifiable il}

let thread_store (#vcfg:_) (tid:nat{tid < vcfg.thread_count}) (il: verifiable_log vcfg)
  = let vs = thread_state tid il in
    vs.st
/
Zeta.Time.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.Intermediate.StateRel.fsti.checked Zeta.Intermediate.Logs.fsti.checked Zeta.Intermediate.Global.fsti.checked Zeta.Interleave.fsti.checked Zeta.High.Interleave.fsti.checked Zeta.Generic.Interleave.fsti.checked Zeta.Generic.Global.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.Interleave.fsti

    tid: Prims.nat{tid < VConfig?.thread_count vcfg} ->
    il: Zeta.Intermediate.Interleave.verifiable_log vcfg ->
    i: Zeta.Generic.Interleave.seq_index il
  -> Prims.GTot (Zeta.Intermediate.Store.vstore vcfg)
Zeta.Intermediate.VerifierConfig.verifier_config Prims.nat Prims.b2t Prims.op_LessThan Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__thread_count Zeta.Intermediate.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__st Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__vtls_t Zeta.Generic.Interleave.thread_state_pre Zeta.Intermediate.Store.vstore
let thread_store_pre
      (#vcfg: _)
      (tid: nat{tid < vcfg.thread_count})
      (il: verifiable_log vcfg)
      (i: seq_index il)
     =
  
let vs = thread_state_pre tid il i in
vs.st