val lemma_non_eac_init_addb
      (#app #n: _)
      (epmax: epoch)
      (itsl:
          neac_before_epoch app n epmax
            { let fi = eac_failure itsl in
              GB.aems_equal_upto epmax itsl /\ fi.es = EACInit /\ AddB? fi.le })
    : GTot (hash_collision app)
val lemma_non_eac_init_addb
      (#app #n: _)
      (epmax: epoch)
      (itsl:
          neac_before_epoch app n epmax
            { let fi = eac_failure itsl in
              GB.aems_equal_upto epmax itsl /\ fi.es = EACInit /\ AddB? fi.le })
    : GTot (hash_collision app)
let lemma_non_eac_init_addb
  (#app #n:_)
  (epmax: epoch)
  (itsl: neac_before_epoch app n epmax
    {let fi = eac_failure itsl in
     GB.aems_equal_upto epmax itsl /\
     fi.es = EACInit /\
     AddB? fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let be = blum_add_elem itsl i in
    let ep = be.t.e in
    let itsli = prefix itsl i in

    // since fi.es is EACInit, there cannot be a prior entry for fi.bk
    //assert(eac_state_of_key fi.bk itsli = EACInit);
    eac_state_init_implies_no_key_refs fi.bk itsli;
    //assert(~ (has_some_ref_to_key fi.bk itsli));

    if evict_set ep itsl `contains` be then (
      (* if evict set contains be, then the index of be should be prior to i *)
      let j = evict_elem_idx itsl be in
      lemma_evict_before_add itsl i;
      assert(j < i);

      (* this implies a prior reference to fi.bk which is a contradiction *)
      FStar.Classical.exists_intro (fun i -> refs_key (I.index itsli i) fi.bk) j;
      hash_collision_contra app
    )
    else (
      not_eq (add_set ep itsl) (evict_set ep itsl) be;
      hash_collision_contra app
    )
module Zeta.High.Verifier.EAC

open Zeta.BinTree
open Zeta.Interleave
open Zeta.App
open Zeta.Key
open Zeta.GenKey
open Zeta.Merkle
open Zeta.Record
open Zeta.Time
open Zeta.MultiSet
open Zeta.MultiSetHashDomain
open Zeta.GenericVerifier
open Zeta.Generic.Blum
open Zeta.EAC
open Zeta.High.Verifier
open Zeta.High.Thread
open Zeta.High.Interleave
open Zeta.High.Merkle
open Zeta.High.Blum

module S = FStar.Seq
module I = Zeta.Interleave
module T = Zeta.Generic.Thread
module G = Zeta.Generic.Global
module GI=Zeta.Generic.Interleave
module GB = Zeta.Generic.Blum
module GTL=Zeta.Generic.TSLog
module HI=Zeta.High.Interleave
module HM = Zeta.High.Merkle
module HTL=Zeta.High.TSLog
module HV = Zeta.High.Verifier
module EAC = Zeta.EAC

noeq
type failure_info (app:app_params) (n:nat) = {
  bi: nat;
  bk: base_key;
  es: eac_state app bk;
  le: vlog_entry app;
  lee: ee:vlog_entry_ext app { to_vlog_entry ee = le /\ eac_add ee es = EACFail };
  vs_pre: v:vtls_t app {v.valid};
  vs_post: v:vtls_t app {v.valid /\ v == verify_step le vs_pre};
}

let eac_failure (#app #n:_) (il: neac_log app n)
  : GTot (failure_info app n)
  = let bi = eac_boundary il in
    let bk = eac_fail_key il in
    let es = eac_state_of_key_pre bk il bi in
    let le = index il bi in
    let lee = mk_vlog_entry_ext il bi in
    let vs_pre = cur_thread_state_pre il bi in
    let vs_post = cur_thread_state_post il bi in
    lemma_cur_thread_state_extend il bi;
    eac_state_transition bk il bi;
    { bi; bk; es; le; lee; vs_pre; vs_post }

let lemma_non_eac_appfn_non_refs
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     not (fi.le `refs_key` fi.bk) /\
     RunApp? fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    ext_app_records_is_stored_val itsl i;
    hash_collision_contra app

let lemma_non_eac_init_appfn
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     (fi.es = EACInit || EAC.is_eac_state_evicted fi.es)  /\
     RunApp? fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let itsli = prefix itsl i in
    let itsli' = prefix itsl (i+1) in
    let tid = src itsl i in
    let RunApp f p ss = fi. le in

    if fi.le `refs_key` fi.bk then (
      // parameter index of key fi.bk
      let pi = S.index_mem fi.bk ss in

      // k is the verifier store prior to processing ...
      let vs_pre = thread_state_pre tid itsl i in
      runapp_implies_store_contains fi.le vs_pre fi.bk;
      let st_pre = thread_store tid itsli in
      assert(store_contains st_pre fi.bk);
      FStar.Classical.exists_intro (fun tid -> store_contains (thread_store tid itsli) fi.bk) tid;
      lemma_instore fi.bk itsli;
      runapp_refs_only_leafkeys itsl i fi.bk;
      hash_collision_contra app
    )
    else lemma_non_eac_appfn_non_refs itsl

let lemma_non_eac_instore_appfn
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     EACInStore? fi.es /\
     fi.le `refs_key` fi.bk /\
     RunApp? fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let itsli = prefix itsl i in
    let itsli' = prefix itsl (i+1) in
    let tid = src itsl i in
    let App (RunApp f p ss) rs = fi.lee in
    let EACInStore _ gk ev = fi.es in

    if not (fi.le `refs_key` fi.bk) then
      lemma_non_eac_appfn_non_refs itsl
    else (
      // parameter index of key fi.bk
      let pi = S.index_mem fi.bk ss in
      let vs_pre = cur_thread_state_pre itsl i in
      let st_pre = thread_store_pre tid itsl i in
      runapp_implies_store_contains fi.le vs_pre fi.bk;
      ext_app_records_is_stored_val itsl i;

      let ak,av = S.index rs pi in
      assert(AppK ak = stored_key st_pre fi.bk);
      assert(AppV av = HV.stored_value st_pre fi.bk);
      //stored_key_is_correct fi.bk itsli;
      key_in_unique_store fi.bk itsli tid (stored_tid fi.bk itsli);
      assert(AppK ak = gk);

      eac_app_state_value_is_stored_value itsli gk;
      assert(AppV av = ev);

      hash_collision_contra app
    )
/
Zeta.Time.fsti.checked Zeta.Record.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.Interleave.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.High.TSLog.fsti.checked Zeta.High.Thread.fsti.checked Zeta.High.Merkle.fsti.checked Zeta.High.Interleave.fsti.checked Zeta.High.Blum.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.TSLog.fsti.checked Zeta.Generic.Thread.fsti.checked Zeta.Generic.Interleave.fsti.checked Zeta.Generic.Global.fsti.checked Zeta.Generic.Blum.fsti.checked Zeta.EAC.fsti.checked Zeta.BinTree.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Zeta.High.Verifier.EAC.fst

    epmax: Zeta.Time.epoch ->
    itsl:
      Zeta.High.TSLog.neac_before_epoch app n epmax
        { let fi = Zeta.High.Verifier.EAC.eac_failure itsl in
          Zeta.Generic.Blum.aems_equal_upto epmax itsl /\ Mkfailure_info?.es fi = Zeta.EAC.EACInit /\
          AddB? (Mkfailure_info?.le fi) }
  -> Prims.GTot (Zeta.HashCollision.hash_collision app)
Zeta.App.app_params Prims.pos Zeta.Time.epoch Zeta.High.TSLog.neac_before_epoch Prims.l_and Zeta.Generic.Blum.aems_equal_upto Zeta.High.Verifier.high_verifier_spec Prims.b2t Prims.op_Equality Zeta.EAC.eac_state Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bk Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__es Zeta.EAC.EACInit Zeta.GenericVerifier.uu___is_AddB Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__le Zeta.High.Verifier.EAC.failure_info Zeta.High.Verifier.EAC.eac_failure Zeta.MultiSet.contains Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.MultiSetHashDomain.ms_hashfn_dom_cmp Zeta.Generic.Blum.evict_set Zeta.HashCollision.hash_collision_contra Prims.unit FStar.Classical.exists_intro Zeta.SeqAux.seq_index Zeta.Interleave.elem_src Zeta.GenericVerifier.verifier_log_entry Zeta.High.Verifier.refs_key Zeta.Interleave.index Prims._assert Prims.op_LessThan Zeta.Generic.Blum.lemma_evict_before_add Zeta.Generic.Interleave.seq_index Zeta.Generic.Interleave.is_blum_evict Zeta.Generic.Interleave.blum_evict_elem Zeta.Generic.Blum.evict_elem_idx Prims.bool Zeta.MultiSet.not_eq Zeta.Generic.Blum.add_set Zeta.HashCollision.hash_collision Zeta.High.Interleave.eac_state_init_implies_no_key_refs Zeta.Interleave.interleaving Zeta.Interleave.prefix Zeta.Time.__proj__Mktimestamp__item__e Zeta.MultiSetHashDomain.__proj__MHDom__item__t Zeta.Generic.Interleave.blum_add_elem Prims.nat Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bi
let lemma_non_eac_init_addb
      (#app #n: _)
      (epmax: epoch)
      (itsl:
          neac_before_epoch app n epmax
            { let fi = eac_failure itsl in
              GB.aems_equal_upto epmax itsl /\ fi.es = EACInit /\ AddB? fi.le })
    : GTot (hash_collision app) =
  
let fi = eac_failure itsl in
let i = fi.bi in
let be = blum_add_elem itsl i in
let ep = be.t.e in
let itsli = prefix itsl i in
eac_state_init_implies_no_key_refs fi.bk itsli;
if (evict_set ep itsl) `contains` be
then
  (let j = evict_elem_idx itsl be in
    lemma_evict_before_add itsl i;
    assert (j < i);
    FStar.Classical.exists_intro (fun i -> refs_key (I.index itsli i) fi.bk) j;
    hash_collision_contra app)
else
  (not_eq (add_set ep itsl) (evict_set ep itsl) be;
    hash_collision_contra app)