val eac_ptrfn_empty_or_points_to_desc
      (#app #n: _)
      (il: eac_log app n)
      (k: merkle_key)
      (c: bin_tree_dir)
    : Lemma (ensures (empty_or_points_to_desc il k c)) (decreases (length il))
val eac_ptrfn_empty_or_points_to_desc
      (#app #n: _)
      (il: eac_log app n)
      (k: merkle_key)
      (c: bin_tree_dir)
    : Lemma (ensures (empty_or_points_to_desc il k c)) (decreases (length il))
let rec eac_ptrfn_empty_or_points_to_desc
  (#app #n:_)
  (il: eac_log app n)
  (k: merkle_key)
  (c: bin_tree_dir)
  : Lemma (ensures (empty_or_points_to_desc il k c))
          (decreases (length il))
  = if length il = 0 then
      eac_value_init (IntK k) il
    else
      let i = length il - 1  in
      let il' = prefix il i in
      let e = index il i in
      eac_ptrfn_empty_or_points_to_desc il' k c;
      eac_value_snoc_simple (IntK k) il;
      match e with
      | AddM _ _ _ -> eac_ptrfn_empty_or_points_desc_addm_extend il k c
      | RunApp _ _ _ -> runapp_refs_only_leafkeys il i k
      | _ -> ()
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

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

#push-options "--fuel 1 --ifuel 1 --z3rlimit_factor 3 --query_stats"

let eac_value_root_snoc
  (#app #n:_)
  (il: eac_log app n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let e = index il i in
                    let il' = prefix il i in
                    let ev = eac_value (IntK Root) il in
                    let ev' = eac_value (IntK Root) il' in
                    match e with
                    | EvictBM _ k' _
                    | EvictM _ k'
                    | AddM _ _ k' -> if Root <> k' then ev = ev' else True
                    | _ -> ev = ev'))
  = let i = length il - 1 in
    let il' = prefix il i in
    let e = index il i in
    let t = src il i in
    lemma_cur_thread_state_extend il i;
    lemma_root_in_store0 il;
    lemma_root_in_store0 il';
    eac_value_is_stored_value_int il' Root 0;
    eac_value_is_stored_value_int il Root 0;
    lemma_fullprefix_equal il;

    match e with
    | AddM _ _ k'
    | EvictBM _ k' _
    | EvictM _ k' ->
      if Root <> k' then
        if t = 0 then ()
        else
          lemma_non_cur_thread_state_extend 0 il i
    | VerifyEpoch
    | NextEpoch
    | EvictB _ _
    | AddB _ _ _ _ ->
      if t = 0 then ()
      else
        lemma_non_cur_thread_state_extend 0 il i
    | RunApp _ _ _ ->
      runapp_refs_only_leafkeys il i Root;
      not_refs_implies_store_unchanged Root 0 il i

#pop-options

let not_refs_implies_eac_value_unchanged_snoc (#app #n:_)
  (gki: key app)
  (il: eac_log app n{length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let e = index il i in
                    let il' = prefix il i in
                    let ev = eac_value gki il in
                    let ev' = eac_value gki il' in
                    let ki = to_base_key gki in
                    not (e `exp_refs_key` ki) ==>
                    ev = ev'))
  = let i = length il - 1 in
    let t = src il i in
    let e = index il i in
    let il' = prefix il i in
    let ev = eac_value gki il in
    let ev' = eac_value gki il' in
    let ki = to_base_key gki in
    let es = eac_state_of_genkey gki il in
    let es' = eac_state_of_genkey gki il' in
    eac_state_snoc ki il;

    if not (e `exp_refs_key` ki) then (
      assert(es = es');
      if ki = Root then
        eac_value_root_snoc il
      else match es with
      | EACInit ->
        eac_value_init_state_is_init il gki;
        eac_value_init_state_is_init il' gki
      | EACInStore m gk v ->
        let t' = stored_tid ki il' in
        not_refs_implies_store_unchanged ki t' il i;
        eac_value_is_stored_value il gki t';
        eac_value_is_stored_value il' gki t'
      | _ ->
        eac_value_is_evicted_value il gki;
        eac_value_is_evicted_value il' gki
    )

let eac_value_snoc_simple_addb
  (#app #n:_)
  (gkf: key app)
  (il: eac_log app n {length il > 0})
  : Lemma (requires (let i = length il - 1 in
                     let il' = prefix il i in
                     let e = index il i in
                     AddB? e))
          (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let e = index il i in
                    let bkf = to_base_key gkf in
                    match e with
                    | AddB (gk,gv) k _ _ -> eac_value gkf il = eac_value gkf il'))
  = let i = length il - 1 in
    let t = src il i in
    let il' = prefix il i in
    let e = index il i in
    let ee = mk_vlog_entry_ext il i in
    let ki = to_base_key gkf in
    let es = eac_state_of_key ki il in
    let es' = eac_state_of_key ki il' in

    not_refs_implies_eac_value_unchanged_snoc gkf il;
    eac_state_snoc ki il;
    lemma_cur_thread_state_extend il i;

    match e with
    | AddB (gk,gv) k _ _ ->
      if k = ki then
        match es', es with
        | EACEvictedBlum gk' gv' _ _, EACInStore _ _ _ ->
          assert(gk' = gk /\ gv = gv');
          if gkf = gk then (
            eac_value_is_evicted_value il' gkf;
            eac_value_is_stored_value il gkf t
          )
          else (
            eac_value_init_state_is_init il gkf;
            eac_value_init_state_is_init il' gkf
          )

#push-options "--fuel 1 --ifuel 1 --z3rlimit_factor 3 --query_stats"

let eac_value_snoc_simple_evictm
  (#app #n:_)
  (gki: key app)
  (il: eac_log app n {length il > 0})
  : Lemma (requires (let i = length il - 1 in
                     let il' = prefix il i in
                     let e = index il i in
                     EvictM? e))
          (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let e = index il i in
                    let ki = to_base_key gki in
                    match e with
                    | EvictM k k' -> if k' = ki then
                                       let v' = eac_merkle_value k' il' in
                                       let es = eac_state_of_key k il' in
                                       let gk = to_gen_key es in
                                       let v = eac_value gk il' in
                                       let c = desc_dir k k' in
                                       let v' = update_value v' c k (hashfn v) false in
                                       eac_value gki il = IntV v'
                                     else
                                       eac_value gki il = eac_value gki il'))
  = let i = length il - 1 in
    let t = src il i in
    let il' = prefix il i in
    let e = index il i in
    let ee = mk_vlog_entry_ext il i in
    let ki = to_base_key gki in
    let es = eac_state_of_key ki il in
    let es' = eac_state_of_key ki il' in

    not_refs_implies_eac_value_unchanged_snoc gki il;
    eac_state_snoc ki il;
    lemma_cur_thread_state_extend il i;

    match e with
    | EvictM k k' ->
     if ki = k then (
       match es', es with
       | EACInStore _ gk _, EACEvictedMerkle _ _ ->
         if gk <> gki then (
           eac_value_init_state_is_init il gki;
           eac_value_init_state_is_init il' gki
         )
         else (
           key_in_unique_store ki il' t (stored_tid ki il');
           assert(stored_tid ki il' = t);
           eac_value_is_stored_value il' gki t;
           eac_value_is_evicted_value il gki;
           ext_evict_val_is_stored_val il i
         )
     )
     else if ki = k' then (
       eac_value_is_stored_value_int il' ki t;
       eac_value_is_stored_value_int il ki t;
       store_contains_implies k il' t;
       eac_value_is_stored_value il' (to_gen_key (eac_state_of_key k il')) t
     )

#pop-options

let eac_value_snoc_simple_evictb
  (#app #n:_)
  (gki: key app)
  (il: eac_log app n {length il > 0})
  : Lemma (requires (let i = length il - 1 in
                     let il' = prefix il i in
                     let e = index il i in
                     EvictB? e))
          (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let e = index il i in
                    let ki = to_base_key gki in
                    match e with
                    | EvictB  _ _  -> eac_value gki il = eac_value gki il'))
  = let i = length il - 1 in
    let t = src il i in
    let il' = prefix il i in
    let e = index il i in
    let ee = mk_vlog_entry_ext il i in
    let ki = to_base_key gki in
    let es = eac_state_of_key ki il in
    let es' = eac_state_of_key ki il' in

    not_refs_implies_eac_value_unchanged_snoc gki il;
    eac_state_snoc ki il;
    lemma_cur_thread_state_extend il i;

    match e with
    | EvictB k _ ->
      if k = ki then (
        match es', es with
        | EACInStore _ gk _, EACEvictedBlum _ _ _ _ ->
          if gki = gk then (
            key_in_unique_store ki il' t (stored_tid ki il');
            eac_value_is_stored_value il' gki t;
            eac_value_is_evicted_value il gki;
            ext_evict_val_is_stored_val il i
          )
          else (
            eac_value_init_state_is_init il gki;
            eac_value_init_state_is_init il' gki
          )
      )

#push-options "--z3rlimit_factor 3"

let eac_value_snoc_simple_evictbm
  (#app #n:_)
  (gki: key app)
  (il: eac_log app n {length il > 0})
  : Lemma (requires (let i = length il - 1 in
                     let il' = prefix il i in
                     let e = index il i in
                     EvictBM? e))
          (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let e = index il i in
                    let ki = to_base_key gki in
                    match e with
                    | EvictBM k k' _ -> if k' = ki then
                                       let v' = eac_merkle_value k' il' in
                                       let es = eac_state_of_key k il' in
                                       let gk = to_gen_key es in
                                       let v = eac_value gk il' in
                                       let c = desc_dir k k' in
                                       let dh' = desc_hash v' c in
                                       let Desc k2 h2 b2 = dh' in
                                       let v' = update_value v' c k h2 true in
                                       eac_value gki il = IntV v'
                                     else
                                       eac_value gki il = eac_value gki il'))
  = let i = length il - 1 in
    let t = src il i in
    let il' = prefix il i in
    let e = index il i in
    let ee = mk_vlog_entry_ext il i in
    let ki = to_base_key gki in
    let es = eac_state_of_key ki il in
    let es' = eac_state_of_key ki il' in

    not_refs_implies_eac_value_unchanged_snoc gki il;
    eac_state_snoc ki il;
    lemma_cur_thread_state_extend il i;

    match e with
    | EvictBM k k' _ ->
     if ki = k then (
       match es', es with
       | EACInStore _ gk _, EACEvictedBlum _ _ _ _ ->
         if gk <> gki then (
           eac_value_init_state_is_init il gki;
           eac_value_init_state_is_init il' gki
         )
         else (
           key_in_unique_store ki il' t (stored_tid ki il');
           assert(stored_tid ki il' = t);
           eac_value_is_stored_value il' gki t;
           eac_value_is_evicted_value il gki;
           ext_evict_val_is_stored_val il i
         )
     )
     else if ki = k' then (
       eac_value_is_stored_value_int il' ki t;
       eac_value_is_stored_value_int il ki t;
       store_contains_implies k il' t;
       eac_value_is_stored_value il' (to_gen_key (eac_state_of_key k il')) t;
        ()
     )

#pop-options

let eac_value_snoc_simple
  (#app #n:_)
  (gkf: key app)
  (il: eac_log app n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let e = index il i in
                    let bkf = to_base_key gkf in
                    match e with
                    | AddM (gk,gv) k k' -> if bkf <> k && bkf <> k' then
                                             eac_value gkf il = eac_value gkf il'
                                           else True
                    | AddB _ _ _ _ -> eac_value gkf il = eac_value gkf il'
                    | EvictM k k' -> if k' = bkf then
                                       let v' = eac_merkle_value k' il' in
                                       let es = eac_state_of_key k il' in
                                       let gk = to_gen_key es in
                                       let v = eac_value gk il' in
                                       let c = desc_dir k k' in
                                       let v' = update_value v' c k (hashfn v) false in
                                       eac_value gkf il = IntV v'
                                     else
                                       eac_value gkf il = eac_value gkf il'
                    | EvictB _ _ -> eac_value gkf il = eac_value gkf il'
                    | EvictBM k k' _ -> if k' = bkf then
                                       let v' = eac_merkle_value k' il' in
                                       let es = eac_state_of_key k il' in
                                       let gk = to_gen_key es in
                                       let v = eac_value gk il' in
                                       let c = desc_dir k k' in
                                       let dh' = desc_hash v' c in
                                       let Desc k2 h2 b2 = dh' in
                                       let v' = update_value v' c k h2 true in
                                       eac_value gkf il = IntV v'
                                     else
                                       eac_value gkf il = eac_value gkf il'
                    | VerifyEpoch -> eac_value gkf il = eac_value gkf il'
                    | NextEpoch -> eac_value gkf il = eac_value gkf il'
                    | RunApp _ _ _ -> if e `refs_key` bkf then
                                        True
                                      else
                                       eac_value gkf il = eac_value gkf il'
  ))
  = let i = length il - 1 in
    let il' = prefix il i in
    let e = index il i in
    let bkf = to_base_key gkf in
    let es = eac_state_of_key bkf il in
    let es' = eac_state_of_key bkf il' in
    eac_state_snoc bkf il;
    lemma_cur_thread_state_extend il i;
    not_refs_implies_eac_value_unchanged_snoc gkf il;

    match e with
    | AddB _ _ _ _ -> eac_value_snoc_simple_addb gkf il
    | EvictM _ _ -> eac_value_snoc_simple_evictm gkf il
    | EvictB _ _ -> eac_value_snoc_simple_evictb gkf il
    | EvictBM _ _ _ -> eac_value_snoc_simple_evictbm gkf il
    | _ -> ()


let empty_or_points_to_desc
  (#app #n:_)
  (il: eac_log app n)
  (k:merkle_key)
  (c:bin_tree_dir)
  = match eac_ptrfn_aux il k c with
    | None -> true
    | Some k2 -> is_desc k2 (child c k)


#push-options "--z3rlimit_factor 3"

let eac_ptrfn_empty_or_points_desc_addm_extend
  (#app #n:_)
  (il: eac_log app n {length il > 0})
  (ki: merkle_key)
  (c: bin_tree_dir)
  : Lemma (requires (let i = length il - 1 in
                     let e = index il i in
                     let il' = prefix il i in
                     AddM? e /\
                     empty_or_points_to_desc il' ki c))
          (ensures (empty_or_points_to_desc il ki c))
  = let i = length il - 1 in
    let e = index il i in
    let il' = prefix il i in
    let es = eac_state_of_key ki il in
    let es' = eac_state_of_key ki il' in
    let AddM (gk,gv) k k' = e in
    let t = src il i in

    eac_value_snoc_simple (IntK ki) il;
    lemma_cur_thread_state_extend il i;
    eac_state_snoc ki il;

    if ki = k then (
      match es', es with
      | EACInit, EACInStore _ _ _ ->
        store_contains_implies ki il t;
        eac_value_is_stored_value il (IntK ki) t
      | EACEvictedMerkle _ _, EACInStore _ _ _ ->
        store_contains_implies ki il t;
        eac_value_is_stored_value il (IntK ki) t;
        eac_value_is_evicted_value il' (IntK ki)
    )
    else if ki = k' then (
      store_contains_implies ki il t;
      store_contains_implies ki il' t;
      eac_value_is_stored_value il' (IntK ki) t;
      eac_value_is_stored_value il (IntK ki) t
    )

#pop-options
/
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.eac_log app n -> k: Zeta.Key.merkle_key -> c: Zeta.BinTree.bin_tree_dir
  -> FStar.Pervasives.Lemma (ensures Zeta.High.Merkle.empty_or_points_to_desc il k c)
      (decreases Zeta.Generic.Interleave.length il)
Zeta.App.app_params Prims.pos Zeta.High.Interleave.eac_log Zeta.Key.merkle_key Zeta.BinTree.bin_tree_dir Prims.op_Equality Prims.int Zeta.Generic.Interleave.length Zeta.High.Verifier.high_verifier_spec Zeta.High.Interleave.eac_value_init Zeta.GenKey.IntK Prims.bool Zeta.Record.record Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Zeta.High.Merkle.eac_ptrfn_empty_or_points_desc_addm_extend Zeta.App.appfn_id Zeta.App.appfn_arg FStar.Seq.Base.seq Zeta.High.Interleave.runapp_refs_only_leafkeys Zeta.GenericVerifier.verifier_log_entry Prims.unit Zeta.High.Merkle.eac_value_snoc_simple Zeta.High.Merkle.eac_ptrfn_empty_or_points_to_desc Zeta.Interleave.index Zeta.Generic.Interleave.verifiable_log Prims.b2t Prims.nat Zeta.Generic.Interleave.prefix Prims.op_Subtraction Prims.l_True Prims.squash Zeta.High.Merkle.empty_or_points_to_desc Prims.Nil FStar.Pervasives.pattern
let rec eac_ptrfn_empty_or_points_to_desc
      (#app #n: _)
      (il: eac_log app n)
      (k: merkle_key)
      (c: bin_tree_dir)
    : Lemma (ensures (empty_or_points_to_desc il k c)) (decreases (length il)) =
  
if length il = 0
then eac_value_init (IntK k) il
else
  let i = length il - 1 in
  let il' = prefix il i in
  let e = index il i in
  eac_ptrfn_empty_or_points_to_desc il' k c;
  eac_value_snoc_simple (IntK k) il;
  match e with
  | AddM _ _ _ -> eac_ptrfn_empty_or_points_desc_addm_extend il k c
  | RunApp _ _ _ -> runapp_refs_only_leafkeys il i k
  | _ -> ()