val eac_state_of_key (#app #n:_) (k: base_key) (il: verifiable_log app n)
  : GTot (eac_state app k)
val eac_state_of_key (#app #n:_) (k: base_key) (il: verifiable_log app n)
  : GTot (eac_state app k)
let eac_state_of_key (#app #n:_) (k: base_key) (il: verifiable_log app n)
  = EAC.eac_state_of_key k (vlog_ext_of_il_log il)
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

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

let mk_vlog_entry_ext #app #n (il: verifiable_log app n) (i: seq_index il)
  = let vle = I.index il i in
    let open Zeta.GenericVerifier in
    let open Zeta.High.Verifier in
    let vs = cur_thread_state_pre il i in
    let tid = src il i in
    lemma_cur_thread_state_extend il i;

    match vle with
    | EvictM k k' ->
      let v = stored_value vs.st k in
      EvictMerkle vle v
    | EvictB k ts ->
      let v = stored_value vs.st k in
      EvictBlum vle v tid
    | EvictBM k _ ts ->
      let v = stored_value vs.st k in
      EvictBlum vle v tid
    | RunApp f p ss ->
      let rs = reads vs ss in
      App vle rs
    | v -> NEvict v

let vlog_entry_ext_prop (#app #n:_) (il: verifiable_log app n) (i: seq_index il)
  : Lemma (ensures (let ee = mk_vlog_entry_ext il i in
                    let e = I.index il i in
                    e = to_vlog_entry ee))
  = ()

let mk_vlog_entry_ext_pp (#app #n:_) (il: verifiable_log app n) (j:nat{j <= length il}) (i:nat{i < j})
  : Lemma (ensures (let il' = prefix il j in
                    mk_vlog_entry_ext il i = mk_vlog_entry_ext il' i))
  = ()

let vlog_ext_of_il_log (#app: app_params) (#n:nat) (il: verifiable_log app n)
  = S.init (length il) (hoist_ghost (mk_vlog_entry_ext il))

let vlog_ext_prefix_property (#app #n:_) (il: verifiable_log app n) (j:nat{j <= length il})
  : Lemma (ensures (let il' = prefix il j in
                    let le'1 = vlog_ext_of_il_log il' in
                    let le = vlog_ext_of_il_log il in
                    let le'2 = SA.prefix le j in
                    le'1 = le'2))
          [SMTPat (vlog_ext_of_il_log (prefix il j))]
  = let il' = prefix il j in
    let le1 = vlog_ext_of_il_log il' in
    let le = vlog_ext_of_il_log il in
    let le2 = SA.prefix le j in
    assert(S.length le1 = S.length le2);
    let aux (i: SA.seq_index le1)
      : Lemma (ensures (S.index le1 i = S.index le2 i))
      = ()
    in
    introduce forall i. (S.index le1 i = S.index le2 i) with aux i;
    assert(equal le1 le2)

let is_eac #app #n (il: verifiable_log app n)
  = is_eac_log (vlog_ext_of_il_log il)

let lemma_eac_empty #app #n (il: verifiable_log app n{S.length il = 0})
  : Lemma (ensures (is_eac il))
  = let le = vlog_ext_of_il_log il in
    eac_empty_log le
/
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
  -> Prims.GTot (Zeta.EAC.eac_state app k)
Zeta.App.app_params Prims.nat Zeta.GenericVerifier.base_key Zeta.High.Interleave.verifiable_log Zeta.EAC.eac_state_of_key Zeta.High.Interleave.vlog_ext_of_il_log Zeta.EAC.eac_state
let eac_state_of_key (#app #n: _) (k: base_key) (il: verifiable_log app n) =
  
EAC.eac_state_of_key k (vlog_ext_of_il_log il)