val evict_elems_distinct
      (#vspec #n: _)
      (ep: epoch)
      (il: verifiable_log vspec n)
      (i1 i2: SA.seq_index (evict_seq ep il))
    : Lemma
    (ensures
      (let es = evict_seq ep il in
        i1 <> i2 ==> S.index es i1 <> S.index es i2))
val evict_elems_distinct
      (#vspec #n: _)
      (ep: epoch)
      (il: verifiable_log vspec n)
      (i1 i2: SA.seq_index (evict_seq ep il))
    : Lemma
    (ensures
      (let es = evict_seq ep il in
        i1 <> i2 ==> S.index es i1 <> S.index es i2))
let evict_elems_distinct (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  (i1 i2: SA.seq_index (evict_seq ep il))
  : Lemma (ensures (let es = evict_seq ep il in
                    i1 <> i2 ==> S.index es i1 <> S.index es i2))
  = let evil = evict_il ep il in
    let gl = to_glog il in
    let t1 = src evil i1 in
    let tl1 = G.index gl t1 in
    let _,j1 = i2s_map evil i1 in
    let t2 = src evil i2 in
    let tl2 = G.index gl t2 in
    let _,j2 = i2s_map evil i2 in
    evict_seq_identical_thread ep il t1;
    evict_seq_identical_thread ep il t2;

    if i1 <> i2 then (
      if t1 <> t2 then (
        T.evict_elem_tid ep tl1 j1;
        T.evict_elem_tid ep tl2 j2
      )
      else (
        i2s_map_monotonic evil i1 i2;
        assert(j1 <> j2);
        T.evict_elem_unique ep tl1 j1 j2
      )
    )
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)

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 }

let blum_evict_elem_src_ifn (#vspec #n:_)
  : GTot (IF.cond_idxfn_t (elem_src (ms_hashfn_dom vspec.app) n) (is_blum_evict_ifn #vspec #n))
  = hoist_ghost2 (blum_evict_elem_src #vspec #n)

let evict_il (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : GTot (interleaving (ms_hashfn_dom vspec.app) n)
  = let fm = IF.to_fm (is_blum_evict_epoch_ifn #vspec #n ep) (blum_evict_elem_src_ifn #vspec #n) in
    IF.filter_map fm il

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

let evict_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 es' = evict_seq ep il' in
                    let es = evict_seq ep il in
                    if is_blum_evict_epoch ep il (n - 1) then
                      es == SA.append1 es' (blum_evict_elem il (n - 1))
                    else
                      es == es'))
  = let fm = IF.to_fm (is_blum_evict_epoch_ifn #vspec #n ep) (blum_evict_elem_src_ifn #vspec #n) in
    let i = length il - 1 in
    let il' = prefix il i in
    let ail' = evict_il ep il' in
    IF.lemma_filter_map_snoc fm il;
    if is_blum_evict_epoch ep il i then (
      IF.lemma_filter_map_snoc fm il;
      lemma_iseq_append1 ail' (blum_evict_elem_src il i)
    )

let evict_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 es = evict_set ep il in
                    let es' = evict_set ep il' in
                    if is_blum_evict_epoch ep il i then
                      es == add_elem es' (blum_evict_elem il i)
                    else es == es'))
  = let i = length il - 1 in
    let il' = prefix il i in
    evict_seq_snoc ep il;
    if is_blum_evict_epoch ep il i then
      seq2mset_add_elem #_ #(ms_hashfn_dom_cmp vspec.app) (evict_seq ep il') (blum_evict_elem il i)

let t_add_seq_il (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat {t < n})
  = let a_il = add_il ep il in
    let a_ss = s_seq a_il in
    S.index a_ss t

let t_add_seq_gl (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t: nat{t < n})
  = let gl = s_seq il in
    let tl = G.index gl t in
    T.add_seq ep tl

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

let t_add_i2g (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  (i:SA.seq_index (t_add_seq_il ep il t))
  : j:SA.seq_index (t_add_seq_gl ep il t){S.index (t_add_seq_il ep il t) i = S.index (t_add_seq_gl ep il t) j}
  = let ta_il = t_add_seq_il ep il t in
    let ta_gl = t_add_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    let a_il = add_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    (* index in the add seq sequence *)
    let i1 = s2i_map a_il (t,i) in
    assert(i2s_map a_il i1 = (t,i));
    assert(src a_il i1 = t);

    (* index in the interleaved sequence il *)
    let i2 = IF.filter_map_invmap fm il i1 in
    assert(blum_add_elem il i2 = S.index ta_il i);
    assert(src il i2 = t);

    (* index in the original log of the t'th thread *)
    let _,i3 = i2s_map il i2 in
    assert(T.blum_add_elem tl i3 = blum_add_elem il i2);

    (* map i3 to the add seq - the index with ta_gl *)
    T.add_seq_map tl i3

let t_add_i2g_mono (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  : Lemma (ensures (monotonic_prop (t_add_i2g ep il t)))
          [SMTPat (t_add_i2g ep il t)]
  = let ta_il = t_add_seq_il ep il t in
    let ta_gl = t_add_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    let a_il = add_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    let f = t_add_i2g ep il t in

    let aux (i j: SA.seq_index ta_il)
      : Lemma (ensures (i < j ==> f i < f j))
      = if i < j then (
          let i1 = s2i_map a_il (t,i) in
          let j1 = s2i_map a_il (t,j) in
          s2i_map_monotonic a_il (t,i) (t,j);
          assert(i1 < j1);

          let i2 = IF.filter_map_invmap fm il i1 in
          let j2 = IF.filter_map_invmap fm il j1 in
          IF.filter_map_invmap_monotonic fm il i1 j1;
          assert(i2 < j2);

          let _,i3 = i2s_map il i2 in
          let _,j3 = i2s_map il j2 in
          i2s_map_monotonic il i2 j2;
          assert(i3 < j3);

          T.add_seq_map_monotonic tl i3 j3
        )
    in
    forall_intro_2 aux

let t_add_g2i (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  (j:SA.seq_index (t_add_seq_gl ep il t))
  : i:SA.seq_index (t_add_seq_il ep il t){S.index (t_add_seq_il ep il t) i = S.index (t_add_seq_gl ep il t) j}
  = let ta_il = t_add_seq_il ep il t in
    let ta_gl = t_add_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    let a_il = add_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    let j1 = T.add_seq_invmap ep tl j in
    let j2 = s2i_map il (t,j1) in
    assert(is_blum_add il j2);
    assert(blum_add_elem il j2 = T.blum_add_elem tl j1);
    let j3 = IF.filter_map_map fm il j2 in
    let _,j4 = i2s_map a_il j3 in
    j4

let t_add_g2i_mono (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  : Lemma (ensures (monotonic_prop (t_add_g2i ep il t)))
  = let ta_il = t_add_seq_il ep il t in
    let ta_gl = t_add_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    let a_il = add_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    let f = t_add_g2i ep il t in
    let aux (i j: SA.seq_index ta_gl)
      : Lemma (ensures (i < j ==> f i < f j))
      = if i < j then (
          let i1 = T.add_seq_invmap ep tl i in
          let j1 = T.add_seq_invmap ep tl j in
          T.add_seq_invmap_monotonic ep tl i j;
          assert(i1 < j1);

          let i2 = s2i_map il (t,i1) in
          let j2 = s2i_map il (t,j1) in
          s2i_map_monotonic il (t,i1) (t,j1);
          assert(i2 < j2);

          let i3 = IF.filter_map_map fm il i2 in
          let j3 = IF.filter_map_map fm il j2 in
          IF.lemma_filter_map_map_monotonic fm il i2 j2;
          assert(i3 < j3);

          i2s_map_monotonic a_il i3 j3
        )
    in
    forall_intro_2 aux

#pop-options

#push-options "--z3rlimit_factor 3"

let add_seq_identical_thread (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t: nat{t < n})
  : Lemma (ensures (t_add_seq_il ep il t == t_add_seq_gl ep il t))
   = monotonic_bijection_implies_equal
      (t_add_seq_il ep il t)
      (t_add_seq_gl ep il t)
      (t_add_i2g ep il t)
      (t_add_g2i ep il t)

#pop-options

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

let add_sseq_identical (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : Lemma (ensures (s_seq (add_il ep il) == G.add_sseq ep (to_glog il)))
  = let a_il = add_il ep il in
    let a_ss1 = s_seq a_il in
    let gl = to_glog il in
    let a_ss2 = G.add_sseq ep gl in

    let aux (t:_)
      : Lemma (ensures (S.index a_ss1 t == S.index a_ss2 t))
      = add_seq_identical_thread ep il t
    in
    forall_intro aux;
    assert(S.equal a_ss1 a_ss2)

let add_set_identical (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : Lemma (ensures (add_set ep il == G.add_set ep (to_glog il)))
  = add_sseq_identical ep il;
    Zeta.MultiSet.SSeq.lemma_interleaving_multiset #_ #(ms_hashfn_dom_cmp vspec.app) (add_il ep il)

#pop-options

let t_evict_seq_il (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat {t < n})
  = let a_il = evict_il ep il in
    let a_ss = s_seq a_il in
    S.index a_ss t

let t_evict_seq_gl (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t: nat{t < n})
  = let gl = s_seq il in
    let tl = G.index gl t in
    T.evict_seq ep tl

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

let t_evict_i2g (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  (i:SA.seq_index (t_evict_seq_il ep il t))
  : GTot (j:SA.seq_index (t_evict_seq_gl ep il t){S.index (t_evict_seq_il ep il t) i = S.index (t_evict_seq_gl ep il t) j})
  = let ta_il = t_evict_seq_il ep il t in
    let ta_gl = t_evict_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_evict_epoch_ifn #vspec #n ep) (blum_evict_elem_src_ifn #vspec #n) in
    let a_il = evict_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    (* index in the evict seq sequence *)
    let i1 = s2i_map a_il (t,i) in
    assert(i2s_map a_il i1 = (t,i));
    assert(src a_il i1 = t);

    (* index in the interleaved sequence il *)
    let i2 = IF.filter_map_invmap fm il i1 in
    assert(blum_evict_elem il i2 = S.index ta_il i);
    assert(src il i2 = t);

    (* index in the original log of the t'th thread *)
    let _,i3 = i2s_map il i2 in
    assert(T.blum_evict_elem tl i3 = blum_evict_elem il i2);

    (* map i3 to the evict seq - the index with ta_gl *)
    T.evict_seq_map tl i3

let t_evict_i2g_mono (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  : Lemma (ensures (monotonic_prop (hoist_ghost (t_evict_i2g ep il t))))
          [SMTPat (t_evict_i2g ep il t)]
  = let ta_il = t_evict_seq_il ep il t in
    let ta_gl = t_evict_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_evict_epoch_ifn #vspec #n ep) (blum_evict_elem_src_ifn #vspec #n) in
    let a_il = evict_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    let f = t_evict_i2g ep il t in

    let aux (i j: SA.seq_index ta_il)
      : Lemma (ensures (i < j ==> f i < f j))
      = if i < j then (
          let i1 = s2i_map a_il (t,i) in
          let j1 = s2i_map a_il (t,j) in
          s2i_map_monotonic a_il (t,i) (t,j);
          assert(i1 < j1);

          let i2 = IF.filter_map_invmap fm il i1 in
          let j2 = IF.filter_map_invmap fm il j1 in
          IF.filter_map_invmap_monotonic fm il i1 j1;
          assert(i2 < j2);

          let _,i3 = i2s_map il i2 in
          let _,j3 = i2s_map il j2 in
          i2s_map_monotonic il i2 j2;
          assert(i3 < j3);

          T.evict_seq_map_monotonic tl i3 j3
        )
    in
    forall_intro_2 aux

let t_evict_g2i (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  (j:SA.seq_index (t_evict_seq_gl ep il t))
  : GTot (i:SA.seq_index (t_evict_seq_il ep il t){S.index (t_evict_seq_il ep il t) i = S.index (t_evict_seq_gl ep il t) j})
  = let ta_il = t_evict_seq_il ep il t in
    let ta_gl = t_evict_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_evict_epoch_ifn #vspec #n ep) (blum_evict_elem_src_ifn #vspec #n) in
    let a_il = evict_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    let j1 = T.evict_seq_invmap ep tl j in
    let j2 = s2i_map il (t,j1) in
    assert(is_blum_evict il j2);
    assert(blum_evict_elem il j2 = T.blum_evict_elem tl j1);
    let j3 = IF.filter_map_map fm il j2 in
    let _,j4 = i2s_map a_il j3 in
    j4

let t_evict_g2i_mono (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t:nat{t < n})
  : Lemma (ensures (monotonic_prop (hoist_ghost (t_evict_g2i ep il t))))
  = let ta_il = t_evict_seq_il ep il t in
    let ta_gl = t_evict_seq_gl ep il t in
    let fm = IF.to_fm (is_blum_evict_epoch_ifn #vspec #n ep) (blum_evict_elem_src_ifn #vspec #n) in
    let a_il = evict_il ep il in
    let gl = to_glog il in
    let tl = G.index gl t in

    let f = t_evict_g2i ep il t in
    let aux (i j: SA.seq_index ta_gl)
      : Lemma (ensures (i < j ==> f i < f j))
      = if i < j then (
          let i1 = T.evict_seq_invmap ep tl i in
          let j1 = T.evict_seq_invmap ep tl j in
          T.evict_seq_invmap_monotonic ep tl i j;
          assert(i1 < j1);

          let i2 = s2i_map il (t,i1) in
          let j2 = s2i_map il (t,j1) in
          s2i_map_monotonic il (t,i1) (t,j1);
          assert(i2 < j2);

          let i3 = IF.filter_map_map fm il i2 in
          let j3 = IF.filter_map_map fm il j2 in
          IF.lemma_filter_map_map_monotonic fm il i2 j2;
          assert(i3 < j3);

          i2s_map_monotonic a_il i3 j3
        )
    in
    forall_intro_2 aux

#pop-options

#push-options "--z3rlimit_factor 3 --split_queries always --query_stats"

let evict_seq_identical_thread (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n) (t: nat{t < n})
  : Lemma (ensures (t_evict_seq_il ep il t == t_evict_seq_gl ep il t))
   = monotonic_bijection_implies_equal
      (t_evict_seq_il ep il t)
      (t_evict_seq_gl ep il t)
      (hoist_ghost (t_evict_i2g ep il t))
      (hoist_ghost (t_evict_g2i ep il t))

#pop-options

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

let evict_sseq_identical (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : Lemma (ensures (s_seq (evict_il ep il) == G.evict_sseq ep (to_glog il)))
  = let a_il = evict_il ep il in
    let a_ss1 = s_seq a_il in
    let gl = to_glog il in
    let a_ss2 = G.evict_sseq ep gl in

    let aux (t:_)
      : Lemma (ensures (S.index a_ss1 t == S.index a_ss2 t))
      = evict_seq_identical_thread ep il t
    in
    forall_intro aux;
    assert(S.equal a_ss1 a_ss2)

let evict_set_identical (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : Lemma (ensures (evict_set ep il == G.evict_set ep (to_glog il)))
  = evict_sseq_identical ep il;
    Zeta.MultiSet.SSeq.lemma_interleaving_multiset #_ #(ms_hashfn_dom_cmp vspec.app) (evict_il ep il)

#pop-options

let lemma_add_evict_ep_i2g (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : Lemma (requires (add_set ep il == evict_set ep il))
          (ensures (let gl = to_glog il in
                    G.add_set ep gl == G.evict_set ep gl))
  = add_set_identical ep il;
    evict_set_identical ep il

let lemma_add_evict_ep_g2i (#vspec #n:_) (ep: epoch) (il: verifiable_log vspec n)
  : Lemma (requires (let gl = to_glog il in
                     G.add_set ep gl == G.evict_set ep gl))
          (ensures (add_set ep il == evict_set ep il))
  = add_set_identical ep il;
    evict_set_identical ep il

let lemma_add_evict_set_dir1 (#vspec #n:_) (epmax: epoch) (il: verifiable_log vspec n)
  : Lemma (requires (aems_equal_upto epmax il))
          (ensures (G.aems_equal_upto epmax (to_glog il)))
  = let gl = to_glog il in
    let aux (ep:epoch)
      : Lemma (ensures (ep <= epmax ==> G.add_set ep gl == G.evict_set ep gl))
      = if ep <= epmax then
          lemma_add_evict_ep_i2g ep il
    in
    forall_intro aux

let lemma_add_evict_set_dir2 (#vspec #n:_) (epmax: epoch) (il: verifiable_log vspec n)
  : Lemma (requires (G.aems_equal_upto epmax (to_glog il)))
          (ensures (aems_equal_upto epmax il))

  = let gl = to_glog il in
    let aux (ep:epoch)
      : Lemma (ensures (ep <= epmax ==> add_set ep il == evict_set ep il))
      = if ep <= epmax then
          lemma_add_evict_ep_g2i ep il
    in
    forall_intro aux

let lemma_add_evict_set_identical_glog (#vspec #n:_) (epmax: epoch) (il: verifiable_log vspec n)
  : Lemma (ensures (aems_equal_upto epmax il <==> G.aems_equal_upto epmax (to_glog il)))
  = introduce aems_equal_upto epmax il ==> G.aems_equal_upto epmax (to_glog il)
    with _. lemma_add_evict_set_dir1 epmax il;
    introduce G.aems_equal_upto epmax (to_glog il) ==> aems_equal_upto epmax il
    with _. lemma_add_evict_set_dir2 epmax il

let add_set_contains_each_add_elem (#vspec #n:_) (il: verifiable_log vspec n) (i: seq_index il{is_blum_add il i})
  : Lemma (ensures (let be = blum_add_elem il i in
                    let ep = be.t.e in
                    add_set ep il `contains` be))
  = let be = blum_add_elem il i in
    let ep = be.t.e in
    let ail = add_il ep il in
    let asq = i_seq ail in
    let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    let j = IF.filter_map_map fm il i in

    index_prop ail j;
    assert(S.index asq j = be);
    mset_contains_seq_element #_ #(ms_hashfn_dom_cmp vspec.app) asq j

let some_add_elem_idx
  (#vspec #n:_)
  (il: verifiable_log vspec n)
  (be: ms_hashfn_dom vspec.app {let ep = be.t.e in
                                add_set ep il `contains` be})
  : i: seq_index il {is_blum_add il i /\ be = blum_add_elem il i}
  = let ep = be.t.e in
    let fm = IF.to_fm (is_blum_add_epoch_ifn #vspec #n ep) (blum_add_elem_src_ifn #vspec #n) in
    let ail = add_il ep il in
    let asq = i_seq ail in
    let j = index_of_mselem #_ #(ms_hashfn_dom_cmp vspec.app) asq be in
    let i = IF.filter_map_invmap fm il j in
    index_prop ail j;
    i

let evict_set_contains_each_evict_elem (#vspec #n:_) (il: verifiable_log vspec n) (i: seq_index il{is_blum_evict il i})
  : Lemma (ensures (let be = blum_evict_elem il i in
                    let ep = be.t.e in
                    evict_set ep il `contains` be))
  = let be = blum_evict_elem il i in
    let ep = be.t.e in
    let eil = evict_il ep il in
    let es = i_seq eil in
    let fm = IF.to_fm (is_blum_evict_epoch_ifn #vspec #n ep) (blum_evict_elem_src_ifn #vspec #n) in
    let j = IF.filter_map_map fm il i in
    index_prop eil j;
    mset_contains_seq_element #_ #(ms_hashfn_dom_cmp vspec.app) es j

let rec index_mem_2 (#a:eqtype) (s: S.seq a) (x: a {S.count x s >= 2})
  : Tot (ij:(SA.seq_index s * SA.seq_index s)
         {let i,j = ij in
          i <> j /\ S.index s i = x /\ S.index s j = x})
    (decreases S.length s)
  = assert(S.length s > 0);
    if S.head s = x then
      (0, 1 + (S.index_mem  x (S.tail s)))
    else
      let i,j = index_mem_2 (S.tail s) x in
      (i + 1, j + 1)

#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 ->
    i1: Zeta.SeqAux.seq_index (Zeta.Generic.Blum.evict_seq ep il) ->
    i2: Zeta.SeqAux.seq_index (Zeta.Generic.Blum.evict_seq ep il)
  -> FStar.Pervasives.Lemma
    (ensures
      (let es = Zeta.Generic.Blum.evict_seq ep il in
        i1 <> i2 ==> FStar.Seq.Base.index es i1 <> FStar.Seq.Base.index es i2))
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.Time.epoch Zeta.Generic.Interleave.verifiable_log Zeta.SeqAux.seq_index Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Generic.Blum.evict_seq Prims.op_disEquality Prims.l_or Prims.b2t Prims.op_LessThan Zeta.Generic.Thread.evict_elem_tid Prims.unit Prims.bool Zeta.Generic.Thread.evict_elem_unique Prims._assert Zeta.Interleave.i2s_map_monotonic Zeta.Generic.Blum.evict_seq_identical_thread Zeta.SSeq.sseq_index Zeta.Interleave.s_seq Prims.l_and Prims.op_Equality Zeta.Interleave.index Zeta.SSeq.indexss FStar.Pervasives.Native.fst Zeta.Interleave.src Zeta.Interleave.i2s_map Zeta.Generic.Thread.verifiable_log Zeta.Generic.Global.index Zeta.Generic.Global.verifiable_log Zeta.Generic.Interleave.to_glog Zeta.Interleave.interleaving Zeta.Generic.Blum.evict_il Prims.l_True Prims.squash Prims.l_imp FStar.Seq.Base.index FStar.Seq.Base.seq Prims.Nil FStar.Pervasives.pattern
let evict_elems_distinct
      (#vspec #n: _)
      (ep: epoch)
      (il: verifiable_log vspec n)
      (i1 i2: SA.seq_index (evict_seq ep il))
    : Lemma
    (ensures
      (let es = evict_seq ep il in
        i1 <> i2 ==> S.index es i1 <> S.index es i2)) =
  
let evil = evict_il ep il in
let gl = to_glog il in
let t1 = src evil i1 in
let tl1 = G.index gl t1 in
let _, j1 = i2s_map evil i1 in
let t2 = src evil i2 in
let tl2 = G.index gl t2 in
let _, j2 = i2s_map evil i2 in
evict_seq_identical_thread ep il t1;
evict_seq_identical_thread ep il t2;
if i1 <> i2
then
  (if t1 <> t2
    then
      (T.evict_elem_tid ep tl1 j1;
        T.evict_elem_tid ep tl2 j2)
    else
      (i2s_map_monotonic evil i1 i2;
        assert (j1 <> j2);
        T.evict_elem_unique ep tl1 j1 j2))