val blum_evict_elem_props
  (#app #n:_)
  (il: verifiable_log app n)
  (i: seq_index il {is_blum_evict il i})
  : Lemma (ensures (let e = I.index il i in
                    let MSD.MHDom (gk,vk) t_e tid_e = blum_evict_elem il i in
                    let tid = I.src il i in
                    let st_pre = thread_store_pre tid il i in
                    let k = V.evict_slot e in
                    k = to_base_key gk /\
                    store_contains st_pre k /\
                    gk = stored_key st_pre k /\
                    vk = stored_value st_pre k /\
                    t_e = V.blum_evict_timestamp e /\
                    tid_e = tid))
          [SMTPat (blum_evict_elem il i)]
val blum_evict_elem_props
  (#app #n:_)
  (il: verifiable_log app n)
  (i: seq_index il {is_blum_evict il i})
  : Lemma (ensures (let e = I.index il i in
                    let MSD.MHDom (gk,vk) t_e tid_e = blum_evict_elem il i in
                    let tid = I.src il i in
                    let st_pre = thread_store_pre tid il i in
                    let k = V.evict_slot e in
                    k = to_base_key gk /\
                    store_contains st_pre k /\
                    gk = stored_key st_pre k /\
                    vk = stored_value st_pre k /\
                    t_e = V.blum_evict_timestamp e /\
                    tid_e = tid))
          [SMTPat (blum_evict_elem il i)]
let blum_evict_elem_props
  (#app #n:_)
  (il: verifiable_log app n)
  (i: seq_index il {is_blum_evict il i})
  : Lemma (ensures (let e = I.index il i in
                    let MSD.MHDom (gk,vk) t_e tid_e = blum_evict_elem il i in
                    let tid = I.src il i in
                    let st_pre = thread_store_pre tid il i in
                    let k = V.evict_slot e in
                    k = to_base_key gk /\
                    store_contains st_pre k /\
                    gk = stored_key st_pre k /\
                    vk = stored_value st_pre k /\
                    t_e = V.blum_evict_timestamp e /\
                    tid_e = tid))
  = let e = index il i in
    let be = blum_evict_elem il i in
    lemma_cur_thread_state_extend 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

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
/
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.Generic.Interleave.seq_index il {Zeta.Generic.Interleave.is_blum_evict il i}
  -> FStar.Pervasives.Lemma
      (ensures
        (let e = Zeta.Interleave.index il i in
          let _ = Zeta.Generic.Interleave.blum_evict_elem il i in
          (let
            Zeta.MultiSetHashDomain.MHDom
              #_
              (FStar.Pervasives.Native.Mktuple2 #_ #_ gk vk)
              t_e
              tid_e =
              _
            in
            let tid = Zeta.Interleave.src il i in
            let st_pre = Zeta.High.Interleave.thread_store_pre tid il i in
            let k = Zeta.GenericVerifier.evict_slot e in
            k = Zeta.GenKey.to_base_key gk /\ Zeta.High.Verifier.store_contains st_pre k /\
            gk = Zeta.High.Verifier.stored_key st_pre k /\
            vk = Zeta.High.Verifier.stored_value st_pre k /\
            t_e = Zeta.GenericVerifier.blum_evict_timestamp e /\ tid_e = tid)
          <:
          Type0)) [SMTPat (Zeta.Generic.Interleave.blum_evict_elem il i)]
Zeta.App.app_params Prims.nat Zeta.High.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Zeta.High.Verifier.high_verifier_spec Prims.b2t Zeta.Generic.Interleave.is_blum_evict Zeta.Generic.Interleave.lemma_cur_thread_state_extend Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Generic.Interleave.blum_evict_elem Zeta.GenericVerifier.verifier_log_entry Zeta.Interleave.index Prims.unit Prims.l_True Prims.squash Zeta.GenKey.key Zeta.Record.value Zeta.Time.timestamp Zeta.Thread.thread_id Prims.l_and Prims.op_Equality Zeta.BinTree.bin_tree_node Prims.l_or Prims.op_LessThanOrEqual Zeta.BinTree.depth Zeta.Key.key_size Zeta.GenKey.to_base_key Zeta.High.Verifier.store_contains Zeta.High.Verifier.stored_key Zeta.High.Verifier.stored_value Zeta.GenericVerifier.blum_evict_timestamp Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Zeta.GenericVerifier.evict_slot Zeta.High.Verifier.store_t Zeta.High.Interleave.thread_store_pre Prims.op_LessThan Zeta.Interleave.src Prims.Nil FStar.Pervasives.pattern
let blum_evict_elem_props
      (#app #n: _)
      (il: verifiable_log app n)
      (i: seq_index il {is_blum_evict il i})
    : Lemma
    (ensures
      (let e = I.index il i in
        let MSD.MHDom (gk, vk) t_e tid_e = blum_evict_elem il i in
        let tid = I.src il i in
        let st_pre = thread_store_pre tid il i in
        let k = V.evict_slot e in
        k = to_base_key gk /\ store_contains st_pre k /\ gk = stored_key st_pre k /\
        vk = stored_value st_pre k /\ t_e = V.blum_evict_timestamp e /\ tid_e = tid)) =
  
let e = index il i in
let be = blum_evict_elem il i in
lemma_cur_thread_state_extend il i