val not_refs_implies_store_unchanged  (#app #n:_) (k:base_key) (t:nat{t < n})
  (il: verifiable_log app n) (i:seq_index il)
  : Lemma (ensures (let e = I.index il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    not (e `exp_refs_key` k) ==>
                    store_contains st_pre k ==>
                    (store_contains st_post k /\
                     stored_key st_post k == stored_key st_pre k /\
                     stored_value st_post k == stored_value st_pre k)))
val not_refs_implies_store_unchanged  (#app #n:_) (k:base_key) (t:nat{t < n})
  (il: verifiable_log app n) (i:seq_index il)
  : Lemma (ensures (let e = I.index il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    not (e `exp_refs_key` k) ==>
                    store_contains st_pre k ==>
                    (store_contains st_post k /\
                     stored_key st_post k == stored_key st_pre k /\
                     stored_value st_post k == stored_value st_pre k)))
let not_refs_implies_store_unchanged  (#app #n:_) (ki:base_key) (ti:nat{ti < n})
  (il: verifiable_log app n) (i:seq_index il)
  : Lemma (ensures (let e = index il i in
                    let st_pre = thread_store_pre ti il i in
                    let st_post = thread_store_post ti il i in
                    not (e `exp_refs_key` ki) ==>
                    store_contains st_pre ki ==>
                    (store_contains st_post ki /\
                     stored_key st_post ki == stored_key st_pre ki /\
                     stored_value st_post ki == stored_value st_pre ki)))
  = let e = index il i in
    let t = src il i in
    let st_pre = thread_store_pre ti il i in
    let vs_pre = thread_state_pre ti il i in
    lemma_cur_thread_state_extend il i;

    if t <> ti then lemma_non_cur_thread_state_extend ti il i
    else
      if not (e `exp_refs_key` ki) && store_contains st_pre ki then
        match e with
        | RunApp _ _ _ ->
          runapp_doesnot_change_nonref_slots e vs_pre ki
        | _ -> ()
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"

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

#push-options "--z3rlimit_factor 3"
/
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

    k: Zeta.GenericVerifier.base_key ->
    t: Prims.nat{t < n} ->
    il: Zeta.High.Interleave.verifiable_log app n ->
    i: Zeta.Generic.Interleave.seq_index il
  -> FStar.Pervasives.Lemma
    (ensures
      (let e = Zeta.Interleave.index il i in
        let st_pre = Zeta.High.Interleave.thread_store_pre t il i in
        let st_post = Zeta.High.Interleave.thread_store_post t il i in
        Prims.op_Negation (Zeta.High.Verifier.exp_refs_key e k) ==>
        Zeta.High.Verifier.store_contains st_pre k ==>
        Zeta.High.Verifier.store_contains st_post k /\
        Zeta.High.Verifier.stored_key st_post k == Zeta.High.Verifier.stored_key st_pre k /\
        Zeta.High.Verifier.stored_value st_post k == Zeta.High.Verifier.stored_value st_pre k))
Zeta.App.app_params Prims.int Zeta.GenericVerifier.base_key Prims.nat Prims.b2t Prims.op_LessThan Zeta.High.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Zeta.High.Verifier.high_verifier_spec Prims.op_disEquality Prims.l_or Zeta.Generic.Interleave.lemma_non_cur_thread_state_extend Prims.bool Prims.op_AmpAmp Prims.op_Negation Zeta.High.Verifier.exp_refs_key Zeta.High.Verifier.store_contains 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.runapp_doesnot_change_nonref_slots Zeta.GenericVerifier.verifier_log_entry Prims.unit Zeta.Generic.Interleave.lemma_cur_thread_state_extend Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__vtls_t Zeta.Generic.Interleave.thread_state_pre Zeta.High.Verifier.store_t Zeta.High.Interleave.thread_store_pre Zeta.Interleave.src Zeta.Interleave.index Prims.l_True Prims.squash Prims.l_imp Prims.l_and Prims.eq2 Zeta.GenKey.key Zeta.High.Verifier.stored_key Zeta.Record.value Zeta.High.Verifier.stored_value Zeta.High.Interleave.thread_store_post Prims.Nil FStar.Pervasives.pattern
let not_refs_implies_store_unchanged
      (#app #n: _)
      (ki: base_key)
      (ti: nat{ti < n})
      (il: verifiable_log app n)
      (i: seq_index il)
    : Lemma
    (ensures
      (let e = index il i in
        let st_pre = thread_store_pre ti il i in
        let st_post = thread_store_post ti il i in
        not (e `exp_refs_key` ki) ==>
        store_contains st_pre ki ==>
        (store_contains st_post ki /\ stored_key st_post ki == stored_key st_pre ki /\
          stored_value st_post ki == stored_value st_pre ki))) =
  
let e = index il i in
let t = src il i in
let st_pre = thread_store_pre ti il i in
let vs_pre = thread_state_pre ti il i in
lemma_cur_thread_state_extend il i;
if t <> ti
then lemma_non_cur_thread_state_extend ti il i
else
  if not (e `exp_refs_key` ki) && store_contains st_pre ki
  then
    match e with
    | RunApp _ _ _ -> runapp_doesnot_change_nonref_slots e vs_pre ki
    | _ -> ()