val blum_evict_elem_src
      (#vspec #n: _)
      (il: verifiable_log vspec n)
      (i: seq_index il {is_blum_evict il i})
    : GTot (elem_src (ms_hashfn_dom vspec.app) n)
val blum_evict_elem_src
      (#vspec #n: _)
      (il: verifiable_log vspec n)
      (i: seq_index il {is_blum_evict il i})
    : GTot (elem_src (ms_hashfn_dom vspec.app) n)
let blum_evict_elem_src (#vspec #n:_) (il: verifiable_log vspec n) (i: seq_index il{is_blum_evict il i})
  : GTot (elem_src (ms_hashfn_dom vspec.app) n)
  = let e = blum_evict_elem il i in
    let s = src il i in
    { e; 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"

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)
    )

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)

#pop-options

let is_blum_evict_epoch_ifn (#vspec #n:_) (ep: epoch)
  : GTot (IF.idxfn_t (gen_seq vspec n) bool)
  = hoist_ghost2 (is_blum_evict_epoch #vspec #n ep)

let is_blum_evict_ifn (#vspec #n:_)
  : IF.idxfn_t (gen_seq vspec n) bool
  = is_blum_evict #vspec #n

let blum_evict_elem_ifn (#vspec #n:_)
  : GTot (IF.cond_idxfn_t (ms_hashfn_dom vspec.app) (is_blum_evict_ifn #vspec #n))
  = hoist_ghost2 (blum_evict_elem #vspec #n)
/
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

    il: Zeta.Generic.Interleave.verifiable_log vspec n ->
    i: Zeta.Generic.Interleave.seq_index il {Zeta.Generic.Interleave.is_blum_evict il i}
  -> Prims.GTot
    (Zeta.Interleave.elem_src (Zeta.MultiSetHashDomain.ms_hashfn_dom (Mkverifier_spec_base?.app vspec
              ))
        n)
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.Generic.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Prims.b2t Zeta.Generic.Interleave.is_blum_evict Zeta.Interleave.Mkelem_src Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Prims.op_LessThan Zeta.Interleave.src Zeta.GenericVerifier.verifier_log_entry Zeta.Generic.Interleave.blum_evict_elem Zeta.Interleave.elem_src
let blum_evict_elem_src
      (#vspec #n: _)
      (il: verifiable_log vspec n)
      (i: seq_index il {is_blum_evict il i})
    : GTot (elem_src (ms_hashfn_dom vspec.app) n) =
  
let e = blum_evict_elem il i in
let s = src il i in
{ e = e; s = s }