val runapp_doesnot_change_store_keys (#app #n:_) (k:base_key)
  (il: verifiable_log app n) (i: seq_index il {is_appfn il i})
  : Lemma (ensures (let t = src il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    store_contains st_post k = store_contains st_pre k))
val runapp_doesnot_change_store_keys (#app #n:_) (k:base_key)
  (il: verifiable_log app n) (i: seq_index il {is_appfn il i})
  : Lemma (ensures (let t = src il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    store_contains st_post k = store_contains st_pre k))
let runapp_doesnot_change_store_keys (#app #n:_) (k:base_key)
  (il: verifiable_log app n) (i: seq_index il {is_appfn il i})
  : Lemma (ensures (let t = src il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    store_contains st_post k = store_contains st_pre k))
  = runapp_doesnot_change_store_keys_extended k il i
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"

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
        | _ -> ()

#pop-options

let not_refs_implies_store_containment_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 `refs_key` ki) ==>
                    store_contains st_pre ki = store_contains st_post 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
      match e with
      | RunApp _ _ _ ->
          runapp_doesnot_change_slot_emptiness e vs_pre ki
      | _ ->
        ()

#restart-solver

#push-options "--z3rlimit_factor 3"

let not_refs_implies_store_key_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 `refs_key` ki) ==>
                    store_contains st_pre ki ==>
                    store_contains st_post ki /\
                    stored_key st_pre ki = stored_key st_post ki /\
                    add_method_of st_pre ki = add_method_of st_post 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;
    not_refs_implies_store_containment_unchanged ki ti il i;

    if t <> ti then lemma_non_cur_thread_state_extend ti il i
    else
      match e with
      | RunApp _ _ _ -> runapp_doesnot_change_slot_key ki e vs_pre;
                        runapp_doesnot_change_store_addmethod ki e vs_pre
      | _ -> ()

#pop-options

let runapp_doesnot_change_store_keys_extended (#app #n:_) (k:base_key)
  (il: verifiable_log app n) (i: seq_index il {is_appfn il i})
  : Lemma (ensures (let t = I.src il i in
                    let st_pre = thread_store_pre t il i in
                    let st_post = thread_store_post t il i in
                    store_contains st_post k = store_contains st_pre k /\
                    (store_contains st_pre k ==>
                    (stored_key st_pre k = stored_key st_post k /\
                     add_method_of st_pre k = add_method_of st_post k))))
  = let e = index il i in
    let t = src il i in
    let vs_pre = thread_state_pre t il i in
    lemma_cur_thread_state_extend il i;
    runapp_doesnot_change_slot_emptiness e vs_pre k;
    runapp_doesnot_change_slot_key k e vs_pre;
    runapp_doesnot_change_store_addmethod k e vs_pre
/
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 ->
    il: Zeta.High.Interleave.verifiable_log app n ->
    i: Zeta.Generic.Interleave.seq_index il {Zeta.Generic.Interleave.is_appfn il i}
  -> FStar.Pervasives.Lemma
    (ensures
      (let t = Zeta.Interleave.src 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
        Zeta.High.Verifier.store_contains st_post k = Zeta.High.Verifier.store_contains st_pre k))
Zeta.App.app_params Prims.nat Zeta.GenericVerifier.base_key Zeta.High.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Zeta.High.Verifier.high_verifier_spec Prims.b2t Zeta.Generic.Interleave.is_appfn Zeta.High.Interleave.runapp_doesnot_change_store_keys_extended Prims.unit Prims.l_True Prims.squash Prims.op_Equality Prims.bool Zeta.High.Verifier.store_contains Zeta.High.Verifier.store_t Zeta.High.Interleave.thread_store_post Zeta.High.Interleave.thread_store_pre Prims.op_LessThan Zeta.Interleave.src Zeta.GenericVerifier.verifier_log_entry Prims.Nil FStar.Pervasives.pattern
let runapp_doesnot_change_store_keys
      (#app #n: _)
      (k: base_key)
      (il: verifiable_log app n)
      (i: seq_index il {is_appfn il i})
    : Lemma
    (ensures
      (let t = src il i in
        let st_pre = thread_store_pre t il i in
        let st_post = thread_store_post t il i in
        store_contains st_post k = store_contains st_pre k)) =
  
runapp_doesnot_change_store_keys_extended k il i