val add_set_snoc (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let a_s = add_set ep il in
                    let as' = add_set ep il' in
                    if is_blum_add_epoch ep il i then
                      a_s == add_elem as' (blum_add_elem il i)
                    else a_s == as'))
val add_set_snoc (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let a_s = add_set ep il in
                    let as' = add_set ep il' in
                    if is_blum_add_epoch ep il i then
                      a_s == add_elem as' (blum_add_elem il i)
                    else a_s == as'))
let add_set_snoc (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n {length il > 0})
  : Lemma (ensures (let i = length il - 1 in
                    let il' = prefix il i in
                    let a_s = add_set ep il in
                    let as' = add_set ep il' in
                    if is_blum_add_epoch ep il i then
                      a_s == add_elem as' (blum_add_elem il i)
                    else a_s == as'))
  = let i = length il - 1 in
    let il' = prefix il i in
    add_seq_snoc ep il;
    if is_blum_add_epoch ep il i then
      seq2mset_add_elem #_ #(ms_hashfn_dom_cmp vspec.app) (add_seq ep il') (blum_add_elem il i)
module Zeta.Generic.Blum

open Zeta.Ghost
open Zeta.SMap
open FStar.Classical

module IF = Zeta.IdxFn
module T = Zeta.Generic.Thread

let gen_seq (vspec:verifier_spec) (n:_) = {
  IF.a = I.elem_src (verifier_log_entry vspec) n;
  IF.phi = verifiable;
  IF.phi_commutes_with_prefix = (fun il i -> lemma_prefix_verifiable n il i);
}

let is_blum_add_epoch_ifn (#vspec #n:_) (ep: epoch)
  : IF.idxfn_t (gen_seq vspec n) bool
  = is_blum_add_epoch #vspec #n ep

let is_blum_add_ifn (#vspec #n:_)
  : IF.idxfn_t (gen_seq vspec n) bool
  = is_blum_add #vspec #n

let blum_add_elem_ifn (#vspec #n:_)
  : IF.cond_idxfn_t (ms_hashfn_dom vspec.app) (is_blum_add_ifn #vspec #n)
  = blum_add_elem #vspec #n

let blum_add_elem_src (#vspec #n:_) (il: verifiable_log vspec n) (i: seq_index il{is_blum_add il i})
  : elem_src (ms_hashfn_dom vspec.app) n
  = let e = blum_add_elem il i in
    let s = src il i in
    {e ; s}

let blum_add_elem_src_ifn (#vspec #n:_)
  : IF.cond_idxfn_t (elem_src (ms_hashfn_dom vspec.app) n) (is_blum_add_ifn #vspec #n)
  = blum_add_elem_src #vspec #n

let add_il (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : interleaving (ms_hashfn_dom vspec.app) n
  = let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    IF.filter_map fm il

#push-options "--fuel 0 --ifuel 1 --query_stats"

let add_seq_empty
  (#vspec: verifier_spec)
  (#n:_)
  (ep: epoch)
  (il: verifiable_log vspec n {length il = 0})
  : Lemma (ensures (add_seq ep il == S.empty))
  = let a_s = add_seq ep il in
    S.lemma_empty a_s

let add_seq_snoc
  (#vspec: verifier_spec)
  (#n:_)
  (ep: epoch)
  (il: verifiable_log vspec n {length il > 0})
  : Lemma (ensures (let n = length il in
                    let il' = prefix il (n- 1 ) in
                    let as' = add_seq ep il' in
                    let a_s = add_seq ep il in
                    if is_blum_add_epoch ep il (n - 1) then
                      a_s == SA.append1 as' (blum_add_elem il (n - 1))
                    else
                      a_s == as'))
  = let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    let i = length il - 1 in
    let il' = prefix il i in
    let ail' = add_il ep il' in
    IF.lemma_filter_map_snoc fm il;
    if is_blum_add_epoch ep il i then (
      IF.lemma_filter_map_snoc fm il;
      lemma_iseq_append1 ail' (blum_add_elem_src il i)
    )
/
Zeta.SMap.fsti.checked Zeta.MultiSet.SSeq.fsti.checked Zeta.IdxFn.fsti.checked Zeta.Ghost.fsti.checked Zeta.Generic.Thread.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Generic.Blum.fst

    ep: Zeta.Time.epoch ->
    il: Zeta.Generic.Interleave.verifiable_log vspec 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 a_s = Zeta.Generic.Blum.add_set ep il in
        let as' = Zeta.Generic.Blum.add_set ep il' in
        (match Zeta.Generic.Blum.is_blum_add_epoch ep il i with
          | true -> a_s == Zeta.MultiSet.add_elem as' (Zeta.Generic.Interleave.blum_add_elem il i)
          | _ -> a_s == as')
        <:
        Type0))
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.Time.epoch Zeta.Generic.Interleave.verifiable_log Prims.b2t Prims.op_GreaterThan Zeta.Generic.Interleave.length Zeta.Generic.Blum.is_blum_add_epoch Zeta.MultiSet.seq2mset_add_elem Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.MultiSetHashDomain.ms_hashfn_dom_cmp Zeta.Generic.Blum.add_seq Zeta.Generic.Interleave.blum_add_elem Prims.bool Prims.unit Zeta.Generic.Blum.add_seq_snoc Prims.op_Equality Zeta.Generic.Interleave.prefix Prims.int Prims.op_Subtraction Prims.l_True Prims.squash Prims.eq2 Zeta.MultiSet.mset Zeta.MultiSet.add_elem Zeta.MultiSetHashDomain.mset_ms_hashfn_dom Zeta.Generic.Blum.add_set Prims.Nil FStar.Pervasives.pattern
let add_set_snoc (#vspec #n: _) (ep: epoch) (il: verifiable_log vspec n {length il > 0})
    : Lemma
    (ensures
      (let i = length il - 1 in
        let il' = prefix il i in
        let a_s = add_set ep il in
        let as' = add_set ep il' in
        if is_blum_add_epoch ep il i then a_s == add_elem as' (blum_add_elem il i) else a_s == as')) =
  
let i = length il - 1 in
let il' = prefix il i in
add_seq_snoc ep il;
if is_blum_add_epoch ep il i
then seq2mset_add_elem #_ #(ms_hashfn_dom_cmp vspec.app) (add_seq ep il') (blum_add_elem il i)