val lemma_spec_rel_implies_same_evict_elem (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il {is_blum_evict il i})
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_evict ilk i /\
                    blum_evict_elem il i = blum_evict_elem ilk i))
          [SMTPat (blum_evict_elem il i)]
val lemma_spec_rel_implies_same_evict_elem (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il {is_blum_evict il i})
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_evict ilk i /\
                    blum_evict_elem il i = blum_evict_elem ilk i))
          [SMTPat (blum_evict_elem il i)]
let lemma_spec_rel_implies_same_evict_elem (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il {is_blum_evict il i})
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_evict ilk i /\
                    blum_evict_elem il i = blum_evict_elem ilk i))
  = let _il = prefix il i in
    let t = src il i in
    let _vss:IV.vtls_t vcfg = thread_state_pre t il i in
    let _sts = _vss.st in
    let e = index il i in
    let s = GV.evict_slot e in

    lemma_cur_thread_state_extend il i;

    let ilk = to_logk il in
    let _ilk = SA.prefix ilk i in
    let _vsk: HV.vtls_t vcfg.app = thread_state_pre t ilk i in
    let _stk = _vsk.st in
    let ek = index ilk i in
    assert(is_blum_evict ilk i);
    let k = GV.evict_slot ek in

    elim_forall_vtls_rel _il t;
    lemma_ismap_correct _sts s (slot_of_key _sts k);
    elim_key_store_rel _sts _stk k
module Zeta.Intermediate.Blum

open Zeta.Intermediate.Store
open Zeta.Intermediate.StateRel
open FStar.Classical

module SA = Zeta.SeqAux
module GV = Zeta.GenericVerifier
module HV = Zeta.High.Verifier
module IV = Zeta.Intermediate.Verifier

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

let lemma_spec_rel_implies_same_add_elem (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il {is_blum_add il i})
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_add ilk i /\
                    blum_add_elem il i = blum_add_elem ilk i))
  = lemma_spec_rel_implies_prefix_spec_rel il i

#push-options "--z3rlimit_factor 3"

let lemma_spec_rel_implies_is_blum_evict_identical (#vcfg:_)
  (il: verifiable_log vcfg {spec_rel il})
  (i: seq_index il)
  : Lemma (ensures (let ilk = to_logk il in
                    is_blum_evict il i = is_blum_evict ilk i))
  = let _il = prefix il i in
    let t = src il i in
    let _vss:IV.vtls_t vcfg = thread_state_pre t il i in
    let _sts = _vss.st in
    let e = index il i in
    //let s = GV.evict_slot e in

    lemma_cur_thread_state_extend il i;

    let ilk = to_logk il in
    let _ilk = SA.prefix ilk i in
    let _vsk: HV.vtls_t vcfg.app = thread_state_pre t ilk i in
    let _stk = _vsk.st in
    let ek = index ilk i in
    ()
/
Zeta.SeqAux.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.Intermediate.StateRel.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenericVerifier.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.Blum.fst

    il: Zeta.Intermediate.Interleave.verifiable_log vcfg {Zeta.Intermediate.Interleave.spec_rel il} ->
    i: Zeta.Generic.Interleave.seq_index il {Zeta.Generic.Interleave.is_blum_evict il i}
  -> FStar.Pervasives.Lemma
      (ensures
        (let ilk = Zeta.Intermediate.Interleave.to_logk il in
          Zeta.Generic.Interleave.is_blum_evict ilk i /\
          Zeta.Generic.Interleave.blum_evict_elem il i =
          Zeta.Generic.Interleave.blum_evict_elem ilk i))
      [SMTPat (Zeta.Generic.Interleave.blum_evict_elem il i)]
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Interleave.verifiable_log Zeta.Intermediate.Interleave.spec_rel Zeta.Generic.Interleave.seq_index Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__thread_count Prims.b2t Zeta.Generic.Interleave.is_blum_evict Zeta.Intermediate.Store.elim_key_store_rel Prims.unit Zeta.Intermediate.Store.lemma_ismap_correct Zeta.Intermediate.Store.slot_of_key Zeta.Intermediate.Interleave.elim_forall_vtls_rel Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Zeta.High.Verifier.high_verifier_spec Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.GenericVerifier.evict_slot Prims._assert Zeta.GenericVerifier.verifier_log_entry Zeta.Interleave.index Zeta.High.Verifier.store_t Zeta.High.Verifier.__proj__Mkvtls_t__item__st Zeta.High.Verifier.vtls_t Zeta.Generic.Interleave.thread_state_pre FStar.Seq.Base.seq Zeta.Interleave.elem_src Prims.op_Equality Prims.nat FStar.Seq.Base.length Zeta.SeqAux.prefix Zeta.High.Interleave.ilog Zeta.Intermediate.Interleave.to_logk Zeta.Generic.Interleave.lemma_cur_thread_state_extend Zeta.Intermediate.Store.vstore Zeta.Intermediate.Verifier.__proj__Mkvtls_t__item__st Zeta.Intermediate.Verifier.vtls_t Prims.op_LessThan Zeta.Interleave.src Zeta.Generic.Interleave.verifiable_log Zeta.Generic.Interleave.length Zeta.Generic.Interleave.prefix Prims.l_True Prims.squash Prims.l_and Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Generic.Interleave.blum_evict_elem Prims.Nil FStar.Pervasives.pattern
let lemma_spec_rel_implies_same_evict_elem
      (#vcfg: _)
      (il: verifiable_log vcfg {spec_rel il})
      (i: seq_index il {is_blum_evict il i})
    : Lemma
    (ensures
      (let ilk = to_logk il in
        is_blum_evict ilk i /\ blum_evict_elem il i = blum_evict_elem ilk i)) =
  
let _il = prefix il i in
let t = src il i in
let _vss:IV.vtls_t vcfg = thread_state_pre t il i in
let _sts = _vss.st in
let e = index il i in
let s = GV.evict_slot e in
lemma_cur_thread_state_extend il i;
let ilk = to_logk il in
let _ilk = SA.prefix ilk i in
let _vsk:HV.vtls_t vcfg.app = thread_state_pre t ilk i in
let _stk = _vsk.st in
let ek = index ilk i in
assert (is_blum_evict ilk i);
let k = GV.evict_slot ek in
elim_forall_vtls_rel _il t;
lemma_ismap_correct _sts s (slot_of_key _sts k);
elim_key_store_rel _sts _stk k