val store_contains_implies (#app #n: _) (bk: base_key) (il: eac_log app n) (t: nat{t < n})
    : Lemma
    (ensures
      (let st = thread_store t il in
        store_contains st bk ==>
        bk <> Root ==> EACInStore? (eac_state_of_key bk il) /\ stored_tid bk il = t))
val store_contains_implies (#app #n: _) (bk: base_key) (il: eac_log app n) (t: nat{t < n})
    : Lemma
    (ensures
      (let st = thread_store t il in
        store_contains st bk ==>
        bk <> Root ==> EACInStore? (eac_state_of_key bk il) /\ stored_tid bk il = t))
let store_contains_implies
  (#app #n:_)
  (bk: base_key)
  (il: eac_log app n)
  (t:nat{t < n})
  : Lemma (ensures (let st = thread_store t il in
                    store_contains st bk ==>
                    bk <> Root ==>
                    EACInStore? (eac_state_of_key bk il) /\
                    stored_tid bk il = t))
  = let st = thread_store t il in
    if bk <> Root && store_contains st bk then (
      FStar.Classical.exists_intro (fun tid -> store_contains (thread_store tid il) bk) t;
      lemma_instore bk il;
      key_in_unique_store bk il t (stored_tid bk il)
    )
module Zeta.High.Merkle

module V = Zeta.GenericVerifier
module HV = Zeta.High.Verifier
module BP = Zeta.BinTreePtr
module M = Zeta.Merkle

open Zeta.Ghost

let stored_value (#app:_) = HV.stored_value #app

(* three type of edge additions due to AddM (k,_) k' *)
type addm_t=
  | NoNewEdge         (* common case: no new added; k' points k *)
  | NewEdge           (* new edge added: k' points to none along k direction *)
  | CutEdge           (* cut an existing edge: k' points to k2, is_proper_desc k2 k *)

let addm_props
  (#app:_)
  (#n:pos)
  (il: verifiable_log app n )
  (i: seq_index il{AddM? (index il i) /\ is_eac (prefix il i)})
  : Lemma (ensures (let AddM (gk, gv) k k' = index il i in
                    let il' = prefix il i in
                    is_proper_desc k k' /\
                    (let v' = eac_merkle_value k' il' in
                     let c = desc_dir k k' in
                     let dh' = desc_hash v' c in
                     match dh' with
                     | Empty -> gv = init_value gk
                     | Desc k2 h2 b2 -> (k2 = k /\ h2 = hashfn gv /\ b2 = false) \/
                                        (is_proper_desc k2 k /\ gv = init_value gk))))
          [SMTPat (index il i)]
  = let il' = prefix il i in
    let AddM _ _ k' = index il i in
    lemma_cur_thread_state_extend il i;
    eac_value_is_stored_value_int il' k' (src il i)

(* the property satisfied by all base keys used as an ancestor in addm/evictm/evictbm *)
let ancestor_es_prop (#app:_)
  (bk: base_key)
  (es: eac_state app bk)
  = bk = Root /\ es = EACInit \/
    bk <> Root /\ EACInStore? es
/
Zeta.Merkle.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.Hash.fsti.checked Zeta.Ghost.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.BinTreePtr.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Zeta.High.Merkle.fst
bk: Zeta.GenericVerifier.base_key -> il: Zeta.High.Interleave.eac_log app n -> t: Prims.nat{t < n}
  -> FStar.Pervasives.Lemma
    (ensures
      (let st = Zeta.High.Interleave.thread_store t il in
        Zeta.High.Verifier.store_contains st bk ==>
        bk <> Zeta.BinTree.Root ==>
        EACInStore? (Zeta.High.Interleave.eac_state_of_key bk il) /\
        Zeta.High.Interleave.stored_tid bk il = t))
Zeta.App.app_params Prims.pos Zeta.GenericVerifier.base_key Zeta.High.Interleave.eac_log Prims.nat Prims.b2t Prims.op_LessThan Prims.op_AmpAmp Prims.op_disEquality Zeta.BinTree.bin_tree_node Zeta.BinTree.Root Zeta.High.Verifier.store_contains Zeta.High.Interleave.key_in_unique_store Zeta.High.Interleave.stored_tid Prims.unit Zeta.High.Interleave.lemma_instore FStar.Classical.exists_intro Zeta.High.Interleave.thread_store Prims.bool Zeta.High.Verifier.store_t Prims.l_True Prims.squash Prims.l_imp Prims.l_and Zeta.EAC.uu___is_EACInStore Zeta.High.Interleave.eac_state_of_key Prims.op_Equality Prims.l_or Zeta.GenKey.key Zeta.EAC.to_gen_key Zeta.High.Verifier.stored_key Prims.Nil FStar.Pervasives.pattern
let store_contains_implies (#app #n: _) (bk: base_key) (il: eac_log app n) (t: nat{t < n})
    : Lemma
    (ensures
      (let st = thread_store t il in
        store_contains st bk ==>
        bk <> Root ==> EACInStore? (eac_state_of_key bk il) /\ stored_tid bk il = t)) =
  
let st = thread_store t il in
if bk <> Root && store_contains st bk
then
  (FStar.Classical.exists_intro (fun tid -> store_contains (thread_store tid il) bk) t;
    lemma_instore bk il;
    key_in_unique_store bk il t (stored_tid bk il))