val addm_es_props
      (#app #n: _)
      (il: verifiable_log app n)
      (i: seq_index il {AddM? (index il i) /\ is_eac (prefix il i)})
    : Lemma
      (ensures
        (let AddM _ k k' = index il i in
          let il' = prefix il i in
          let es' = eac_state_of_key_pre k' il i in
          ancestor_es_prop k' es')) [SMTPat (index il i)]
val addm_es_props
      (#app #n: _)
      (il: verifiable_log app n)
      (i: seq_index il {AddM? (index il i) /\ is_eac (prefix il i)})
    : Lemma
      (ensures
        (let AddM _ k k' = index il i in
          let il' = prefix il i in
          let es' = eac_state_of_key_pre k' il i in
          ancestor_es_prop k' es')) [SMTPat (index il i)]
let addm_es_props
  (#app #n:_)
  (il: verifiable_log app n )
  (i: seq_index il{AddM? (index il i) /\ is_eac (prefix il i)})
  : Lemma (ensures (let AddM _ k k' = index il i in
                    let il' = prefix il i in
                    let es' = eac_state_of_key_pre k' il i in
                    ancestor_es_prop k' es'))
          [SMTPat (index il i)]
  = let il' = prefix il i in
    let AddM _ _ k' = index il i in
    lemma_cur_thread_state_extend il i;
    let es' = eac_state_of_key_pre k' il i in
    store_contains_implies k' il' (src il i);
    if k' = Root then
      eac_state_of_root_init 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

(* TODO: Migrate to interleave? *)
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)
    )
/
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

    il: Zeta.High.Interleave.verifiable_log app n ->
    i:
      Zeta.Generic.Interleave.seq_index il
        { AddM? (Zeta.Interleave.index il i) /\
          Zeta.High.Interleave.is_eac (Zeta.Generic.Interleave.prefix il i) }
  -> FStar.Pervasives.Lemma
      (ensures
        (let _ = Zeta.Interleave.index il i in
          (let Zeta.GenericVerifier.AddM #_ _ _ k' = _ in
            let il' = Zeta.Generic.Interleave.prefix il i in
            let es' = Zeta.High.Interleave.eac_state_of_key_pre k' il i in
            Zeta.High.Merkle.ancestor_es_prop k' es')
          <:
          Type0)) [SMTPat (Zeta.Interleave.index 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.l_and Prims.b2t Zeta.GenericVerifier.uu___is_AddM Zeta.Interleave.index Zeta.GenericVerifier.verifier_log_entry Zeta.High.Interleave.is_eac Zeta.Generic.Interleave.prefix Zeta.Record.record Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Prims.op_Equality Zeta.BinTree.bin_tree_node Zeta.BinTree.Root Zeta.High.Interleave.eac_state_of_root_init Prims.bool Prims.unit Zeta.High.Merkle.store_contains_implies Zeta.Interleave.src Zeta.EAC.eac_state Zeta.High.Interleave.eac_state_of_key_pre Zeta.Generic.Interleave.lemma_cur_thread_state_extend Zeta.Generic.Interleave.verifiable_log Zeta.Generic.Interleave.length Prims.l_True Prims.squash Zeta.High.Merkle.ancestor_es_prop Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let addm_es_props
      (#app #n: _)
      (il: verifiable_log app n)
      (i: seq_index il {AddM? (index il i) /\ is_eac (prefix il i)})
    : Lemma
      (ensures
        (let AddM _ k k' = index il i in
          let il' = prefix il i in
          let es' = eac_state_of_key_pre k' il i in
          ancestor_es_prop k' es')) [SMTPat (index il i)] =
  
let il' = prefix il i in
let AddM _ _ k' = index il i in
lemma_cur_thread_state_extend il i;
let es' = eac_state_of_key_pre k' il i in
store_contains_implies k' il' (src il i);
if k' = Root then eac_state_of_root_init il'