val 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)]
val 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 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)
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 *)
/
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 #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ gk gv) k k' =
              _
            in
            let il' = Zeta.Generic.Interleave.prefix il i in
            Zeta.BinTree.is_proper_desc k k' /\
            (let v' = Zeta.High.Merkle.eac_merkle_value k' il' in
              let c = Zeta.BinTree.desc_dir k k' in
              let dh' = Zeta.Merkle.desc_hash v' c in
              (match dh' with
                | Zeta.Merkle.Empty -> gv = Zeta.Record.init_value gk
                | Zeta.Merkle.Desc k2 h2 b2 ->
                  k2 = k /\ h2 = Zeta.HashFunction.hashfn gv /\ b2 = false \/
                  Zeta.BinTree.is_proper_desc k2 k /\ gv = Zeta.Record.init_value gk)
              <:
              Prims.logical))
          <:
          Type0)) [SMTPat (Zeta.Interleave.index il i)]
Zeta.App.app_params Prims.pos 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 Zeta.High.Interleave.eac_value_is_stored_value_int Zeta.Interleave.src Prims.unit Zeta.Generic.Interleave.lemma_cur_thread_state_extend Zeta.Generic.Interleave.verifiable_log Prims.op_Equality Prims.nat Zeta.Generic.Interleave.length Prims.l_True Prims.squash Zeta.GenKey.key Zeta.Record.value Zeta.BinTree.is_proper_desc Zeta.Record.init_value Zeta.Key.base_key Zeta.Hash.hash_value Prims.bool Prims.l_or Zeta.BinTree.bin_tree_node Prims.op_LessThanOrEqual Zeta.BinTree.depth Zeta.Key.key_size Zeta.HashFunction.hashfn Prims.logical Zeta.Merkle.desc_hash_t Zeta.Merkle.desc_hash Zeta.BinTree.bin_tree_dir Prims.op_AmpAmp Zeta.BinTree.is_desc Zeta.BinTree.child Prims.op_Negation Zeta.BinTree.sibling Zeta.BinTree.desc_dir Zeta.Merkle.value Zeta.High.Merkle.eac_merkle_value Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
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)