val lemma_blum_add_elem_props (#app:_) (tl: verifiable_log app) (i: seq_index tl {is_blum_add tl i})
  : Lemma (ensures (let open Zeta.MultiSetHashDomain in
                    let be = blum_add_elem tl i in
                    let gk,gv = be.r in
                    add_slot (index tl i) = to_base_key gk))
          [SMTPat (blum_add_elem tl i)]
val lemma_blum_add_elem_props (#app:_) (tl: verifiable_log app) (i: seq_index tl {is_blum_add tl i})
  : Lemma (ensures (let open Zeta.MultiSetHashDomain in
                    let be = blum_add_elem tl i in
                    let gk,gv = be.r in
                    add_slot (index tl i) = to_base_key gk))
          [SMTPat (blum_add_elem tl i)]
let lemma_blum_add_elem_props (#app:_) (tl: verifiable_log app) (i: seq_index tl {is_blum_add tl i})
  : Lemma (ensures (let open Zeta.MultiSetHashDomain in
                    let be = blum_add_elem tl i in
                    let gk,gv = be.r in
                    add_slot (index tl i) = to_base_key gk))
  = lemma_state_transition tl i
module Zeta.High.Thread

#push-options "--fuel 0 --ifuel 1"
/
Zeta.MultiSetHashDomain.fsti.checked Zeta.Key.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.High.Thread.fst

    tl: Zeta.High.Thread.verifiable_log app ->
    i: Zeta.Generic.Thread.seq_index tl {Zeta.Generic.Thread.is_blum_add tl i}
  -> FStar.Pervasives.Lemma
      (ensures
        (let be = Zeta.Generic.Thread.blum_add_elem tl i in
          let _ = MHDom?.r be in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ gk _ = _ in
            Zeta.GenericVerifier.add_slot (Zeta.Generic.Thread.index tl i) =
            Zeta.GenKey.to_base_key gk)
          <:
          Type0)) [SMTPat (Zeta.Generic.Thread.blum_add_elem tl i)]
Zeta.App.app_params Zeta.High.Thread.verifiable_log Zeta.Generic.Thread.seq_index Zeta.High.Verifier.high_verifier_spec Prims.b2t Zeta.Generic.Thread.is_blum_add Zeta.Generic.Thread.lemma_state_transition Prims.unit Prims.l_True Prims.squash Zeta.GenKey.key Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Record.value Prims.op_Equality Zeta.BinTree.bin_tree_node Prims.l_or Prims.op_LessThanOrEqual Zeta.BinTree.depth Zeta.Key.key_size Zeta.GenericVerifier.add_slot Zeta.Generic.Thread.index Zeta.GenKey.to_base_key Zeta.Record.record Zeta.MultiSetHashDomain.__proj__MHDom__item__r Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.Generic.Thread.blum_add_elem Prims.Nil FStar.Pervasives.pattern
let lemma_blum_add_elem_props
      (#app: _)
      (tl: verifiable_log app)
      (i: seq_index tl {is_blum_add tl i})
    : Lemma
    (ensures
      (let open Zeta.MultiSetHashDomain in
        let be = blum_add_elem tl i in
        let gk, gv = be.r in
        add_slot (index tl i) = to_base_key gk)) =
  
lemma_state_transition tl i