val eac_state_unchanged_snoc (#app #n: _) (bk: base_key) (il: eac_log app n {length il > 0})
    : Lemma
    (ensures
      (let i = length il - 1 in
        let il' = prefix il i in
        let es' = eac_state_of_key bk il' in
        let es = eac_state_of_key bk il in
        let e = index il i in
        es = es' ==> (e `refs_key` bk) ==> RunApp? e /\ EACInStore? es))
val eac_state_unchanged_snoc (#app #n: _) (bk: base_key) (il: eac_log app n {length il > 0})
    : Lemma
    (ensures
      (let i = length il - 1 in
        let il' = prefix il i in
        let es' = eac_state_of_key bk il' in
        let es = eac_state_of_key bk il in
        let e = index il i in
        es = es' ==> (e `refs_key` bk) ==> RunApp? e /\ EACInStore? es))
let eac_state_unchanged_snoc
  (#app #n:_)
  (bk: base_key)
  (il: eac_log app n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let es' = eac_state_of_key bk il' in
                    let es = eac_state_of_key bk il in
                    let e = index il i in
                    es = es' ==>
                    (e `refs_key` bk) ==>
                    RunApp? e /\ EACInStore? es))
  = eac_state_snoc 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

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

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'

let addm_type
  (#app:_)
  (#n:pos)
  (il: verifiable_log app n)
  (i: seq_index il{AddM? (index il i) /\ is_eac (prefix il i)})
  : GTot addm_t
  = let AddM (gk, gv) k k' = index il i in
    let il' = prefix il i in
    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 -> NewEdge
    | Desc k2 h2 b2 -> if k2 = k then NoNewEdge else CutEdge

let cutedge_desc
  (#app:_) (#n:pos)
  (il: verifiable_log app n) (i:_{is_eac (prefix il i) /\ addm_type il i = CutEdge})
  = let AddM (gk, gv) k k' = index il i in
    let il' = prefix il i in
    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
    | Desc k2 h2 b2 -> k2

let is_merkle_evict (#app:_) (e: vlog_entry app)
  = EvictM? e \/ EvictBM? e

let ancestor_slot (#app) (e:vlog_entry app {is_merkle_evict e})
  = match e with
    | EvictM _ k' -> k'
    | EvictBM _ k' _ -> k'

let evictm_props (#app #n:_) (il: eac_log app n) (i: seq_index il{is_merkle_evict (index il i)})
  : Lemma (ensures (let k = evict_slot (index il i) in
                    let k' = ancestor_slot (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
                     points_to v' c k)))
          [SMTPat (index il i)]
  = let il' = prefix il i in
    let k = evict_slot (index il i) in
    let k' = ancestor_slot (index il i) in
    lemma_cur_thread_state_extend il i;
    eac_value_is_stored_value il' (IntK k') (src il i)

let evictm_es_props (#app #n:_) (il: eac_log app n) (i:_ {EvictM? (index il i)})
  : Lemma (ensures (let EvictM k _ = index il i in
                    let es_pre = eac_state_of_key_pre k il i in
                    let es_post = eac_state_of_key_post k il i in
                    EACInStore? es_pre /\ EACEvictedMerkle? es_post))
          [SMTPat (index il i)]
  = let e = index il i in
    let EvictM k _ = e in
    let il' = prefix il i in
    let ee = mk_vlog_entry_ext il i in
    lemma_cur_thread_state_extend il i;
    store_contains_implies k il' (src il i);
    eac_state_transition k il i

let evictbm_es_props (#app #n:_) (il: eac_log app n) (i:_ {EvictBM? (index il i)})
  : Lemma (ensures (let EvictBM k _ _ = index il i in
                    let es_pre = eac_state_of_key_pre k il i in
                    let es_post = eac_state_of_key_post k il i in
                    EACInStore? es_pre /\ EACEvictedBlum? es_post))
          [SMTPat (index il i)]
  = let e = index il i in
    let EvictBM k _ _ = e in
    let il' = prefix il i in
    let ee = mk_vlog_entry_ext il i in
    lemma_cur_thread_state_extend il i;
    store_contains_implies k il' (src il i);
    eac_state_transition k il i

let merkle_evict_ancestor_props
  (#app #n:_)
  (il: eac_log app n) (i:_ {is_merkle_evict (index il i)})
  : Lemma (ensures (let k = ancestor_slot (index il i) in
                    let es_pre = eac_state_of_key_pre k il i in
                    let es_post = eac_state_of_key_post k il i in
                    es_pre = es_post /\ ancestor_es_prop k es_pre))
          [SMTPat (index il i)]
  = let k = ancestor_slot (index il i) in
    let _ = mk_vlog_entry_ext il i in
    let il' = prefix il i in
    lemma_cur_thread_state_extend il i;
    store_contains_implies k il' (src il i);
    eac_state_transition k il i;
    if k = Root then
      eac_state_of_root_init il'

let eac_ptrfn_aux (#app #n:_) (il: eac_log app n) (k:merkle_key) (c:bin_tree_dir)
  : GTot (option (base_key))
  = let v = eac_merkle_value k il in
    if M.points_to_none v c
    then None
    else Some (M.pointed_key v c)

let eac_state_transition_snoc
  (#app #n:_)
  (bk: base_key)
  (il: eac_log app n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let es' = eac_state_of_key bk il' in
                    let es = eac_state_of_key bk il in
                    let e = index il i in
                    es' <> es ==> (
                    e `refs_key` bk /\
                    (match es', es with
                    | EACInit, EACInStore m _ _ -> AddM? e /\ m = MAdd
                    | EACInStore _ _ _ , EACEvictedBlum _ _ _ _ -> V.is_blum_evict e
                    | EACInStore _ gk1 _ , EACEvictedMerkle gk2 _ -> EvictM? e /\ gk1 = gk2
                    | EACEvictedBlum _ _ _ _, EACInStore m _ _ -> AddB? e /\ m = BAdd
                    | EACEvictedMerkle _ _, EACInStore m _ _ -> AddM? e /\ m = MAdd
                    | EACInStore m1 _ _, EACInStore m2 _ _ -> RunApp? e /\ m1 = m2
                    | _ -> False))))
  = eac_state_snoc 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

    bk: Zeta.GenericVerifier.base_key ->
    il: Zeta.High.Interleave.eac_log app n {Zeta.Generic.Interleave.length il > 0}
  -> FStar.Pervasives.Lemma
    (ensures
      (let i = Zeta.Generic.Interleave.length il - 1 in
        let il' = Zeta.Generic.Interleave.prefix il i in
        let es' = Zeta.High.Interleave.eac_state_of_key bk il' in
        let es = Zeta.High.Interleave.eac_state_of_key bk il in
        let e = Zeta.Interleave.index il i in
        es = es' ==> Zeta.High.Verifier.refs_key e bk ==> RunApp? e /\ EACInStore? es))
Zeta.App.app_params Prims.pos Zeta.GenericVerifier.base_key Zeta.High.Interleave.eac_log Prims.b2t Prims.op_GreaterThan Zeta.Generic.Interleave.length Zeta.High.Verifier.high_verifier_spec Zeta.High.Interleave.eac_state_snoc Prims.unit Prims.l_True Prims.squash Prims.l_imp Prims.op_Equality Zeta.EAC.eac_state Zeta.High.Verifier.refs_key Prims.l_and Zeta.GenericVerifier.uu___is_RunApp Zeta.EAC.uu___is_EACInStore Zeta.GenericVerifier.verifier_log_entry Zeta.Interleave.index Zeta.High.Interleave.eac_state_of_key Zeta.Generic.Interleave.verifiable_log Prims.nat Zeta.Generic.Interleave.prefix Prims.int Prims.op_Subtraction Prims.Nil FStar.Pervasives.pattern
let eac_state_unchanged_snoc (#app #n: _) (bk: base_key) (il: eac_log app n {length il > 0})
    : Lemma
    (ensures
      (let i = length il - 1 in
        let il' = prefix il i in
        let es' = eac_state_of_key bk il' in
        let es = eac_state_of_key bk il in
        let e = index il i in
        es = es' ==> (e `refs_key` bk) ==> RunApp? e /\ EACInStore? es)) =
  
eac_state_snoc bk il