val runapp_refs_only_leafkeys (#app #n:_) (il: verifiable_log app n) (i:_ {RunApp? (index il i)}) (k: base_key)
  : Lemma (ensures (let e = index il i in
                    e `refs_key` k ==> is_leaf_key k))
val runapp_refs_only_leafkeys (#app #n:_) (il: verifiable_log app n) (i:_ {RunApp? (index il i)}) (k: base_key)
  : Lemma (ensures (let e = index il i in
                    e `refs_key` k ==> is_leaf_key k))
let runapp_refs_only_leafkeys (#app #n:_) (il: verifiable_log app n) (i:_ {RunApp? (index il i)}) (k: base_key)
  : Lemma (ensures (let e = index il i in
                    e `refs_key` k ==> is_leaf_key k))
  = let e = index il i in
    lemma_cur_thread_state_extend il i;
    let RunApp f p ss = e in
    let vs_pre = thread_state_pre (src il i) il i in
    if e `refs_key` k then
      let idx = index_mem k ss in
      runapp_implies_store_contains e vs_pre k
module Zeta.High.Interleave

open FStar.Classical

open Zeta.Ghost

let root : r:Zeta.BinTree.bin_tree_node { Zeta.BinTree.depth r = 0 } = Zeta.BinTree.Root

#push-options "--fuel 0 --ifuel 1 --query_stats"
/
Zeta.SeqIdx.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.Ghost.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.High.Interleave.fst

    il: Zeta.High.Interleave.verifiable_log app n ->
    i: Zeta.SeqAux.seq_index il {RunApp? (Zeta.Interleave.index il i)} ->
    k: Zeta.GenericVerifier.base_key
  -> FStar.Pervasives.Lemma
    (ensures
      (let e = Zeta.Interleave.index il i in
        Zeta.High.Verifier.refs_key e k ==> Zeta.Key.is_leaf_key k))
Zeta.App.app_params Prims.nat Zeta.High.Interleave.verifiable_log Zeta.SeqAux.seq_index Zeta.Interleave.elem_src Zeta.GenericVerifier.verifier_log_entry Zeta.High.Verifier.high_verifier_spec Prims.b2t Zeta.GenericVerifier.uu___is_RunApp Zeta.Interleave.index Zeta.GenericVerifier.base_key Zeta.App.appfn_id Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.App.appfn_arg FStar.Seq.Base.seq Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Zeta.High.Verifier.refs_key Zeta.High.Verifier.runapp_implies_store_contains FStar.Seq.Properties.index_mem Prims.bool Prims.unit Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__vtls_t Zeta.Generic.Interleave.thread_state_pre Zeta.Interleave.src Zeta.Generic.Interleave.lemma_cur_thread_state_extend Prims.l_True Prims.squash Prims.l_imp Zeta.Key.is_leaf_key Prims.Nil FStar.Pervasives.pattern
let runapp_refs_only_leafkeys
      (#app #n: _)
      (il: verifiable_log app n)
      (i: _{RunApp? (index il i)})
      (k: base_key)
    : Lemma
    (ensures
      (let e = index il i in
        e `refs_key` k ==> is_leaf_key k)) =
  
let e = index il i in
lemma_cur_thread_state_extend il i;
let RunApp f p ss = e in
let vs_pre = thread_state_pre (src il i) il i in
if e `refs_key` k
then
  let idx = index_mem k ss in
  runapp_implies_store_contains e vs_pre k