val 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))
val 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 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
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"
/
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 Zeta.Generic.Blum.add_seq ep il == FStar.Seq.Base.empty)
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.Time.epoch Zeta.Generic.Interleave.verifiable_log Prims.b2t Prims.op_Equality Prims.int Zeta.Generic.Interleave.length FStar.Seq.Base.lemma_empty Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app FStar.Seq.Base.seq Zeta.Generic.Blum.add_seq Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Seq.Base.empty Prims.Nil FStar.Pervasives.pattern
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