val to_logk_entry (#vcfg: _) (il: verifiable_log vcfg) (i: seq_index il)
    : GTot (logK_entry vcfg.app)
val to_logk_entry (#vcfg: _) (il: verifiable_log vcfg) (i: seq_index il)
    : GTot (logK_entry vcfg.app)
let to_logk_entry (#vcfg:_) (il: verifiable_log vcfg) (i: seq_index il)
  : GTot (logK_entry vcfg.app)
  = let gl = to_glog il in
    let ti = i2s_map il i in
    IG.to_logk_entry gl ti
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

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

let thread_store_post (#vcfg:_) (tid: nat{tid < vcfg.thread_count}) (il: verifiable_log vcfg) (i: seq_index il)
  = let vs = thread_state_post tid il i in
    vs.st

val lemma_slot_is_merkle_points_to (#vcfg:_) (il: verifiable_log vcfg) (i: seq_index il):
  Lemma (ensures (slot_points_to_is_merkle_points_to (thread_store_pre (src il i) il i)))
        [SMTPat (prefix il i)]
/
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
il: Zeta.Intermediate.Interleave.verifiable_log vcfg -> i: Zeta.Generic.Interleave.seq_index il
  -> Prims.GTot (Zeta.Intermediate.Logs.logK_entry (VConfig?.app vcfg))
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__thread_count Zeta.Intermediate.Global.to_logk_entry Zeta.SSeq.sseq_index Zeta.GenericVerifier.verifier_log_entry Zeta.Interleave.s_seq Prims.l_and Prims.b2t Prims.op_Equality Zeta.Interleave.index Zeta.SSeq.indexss Prims.nat FStar.Pervasives.Native.fst Zeta.Interleave.src Zeta.Interleave.i2s_map Zeta.Generic.Global.verifiable_log Zeta.Generic.Interleave.to_glog Zeta.Intermediate.Logs.logK_entry Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app
let to_logk_entry (#vcfg: _) (il: verifiable_log vcfg) (i: seq_index il)
    : GTot (logK_entry vcfg.app) =
  
let gl = to_glog il in
let ti = i2s_map il i in
IG.to_logk_entry gl ti