val lemma_non_eac_evicted_blum_addb
      (#app #n: _)
      (epmax: epoch)
      (itsl:
          neac_before_epoch app n epmax
            { let fi = eac_failure itsl in
              GB.aems_equal_upto epmax itsl /\ EACEvictedBlum? fi.es /\ AddB? fi.le })
    : GTot (hash_collision app)
val lemma_non_eac_evicted_blum_addb
      (#app #n: _)
      (epmax: epoch)
      (itsl:
          neac_before_epoch app n epmax
            { let fi = eac_failure itsl in
              GB.aems_equal_upto epmax itsl /\ EACEvictedBlum? fi.es /\ AddB? fi.le })
    : GTot (hash_collision app)
let lemma_non_eac_evicted_blum_addb
  (#app #n:_)
  (epmax: epoch)
  (itsl: neac_before_epoch app n epmax
    {let fi = eac_failure itsl in
     GB.aems_equal_upto epmax itsl /\
     EACEvictedBlum? fi.es /\
     AddB? fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let be = eac_evictedb_addb_diff_elem itsl in
    let ep = be.t.e in
    //assert(be.t.e <= epmax);
    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
    )

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
    )

#push-options "--z3rlimit_factor 3"

let lemma_non_eac_init_addm
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     fi.es = EACInit /\
     AddM? fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let AddM (gk,v) k k' = index itsl i in
    let itsli = prefix itsl i in
    let itsli' = prefix itsl (i+1) in
    let tid = src itsl i in

    assert(eac_add fi.lee fi.es = EACFail);
    assert(v <> init_value gk);

    lemma_addm_ancestor_is_proving itsli';
    assert(k' = proving_ancestor itsli k);

    (* k' is in the verifier thread tid's cache before processing entry i *)
    let st_pre = thread_store_pre tid itsl i in
    assert(store_contains st_pre k');

    let gk' = IntK #app k' in
    eac_value_is_stored_value itsli gk' tid;
    let mv' = eac_merkle_value k' itsli in
    let d = desc_dir k k' in
    let dh' = desc_hash mv' d in

    lemma_proving_ancestor_initial itsli k;

    match dh' with
    | Empty -> hash_collision_contra app
    | Desc k2 _ _ ->
      lemma_desc_reflexive k;
      hash_collision_contra app

#pop-options

let lemma_non_eac_init_evict
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     fi.es = EACInit /\
     is_evict fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let k  = evict_slot fi.le in
    let itsli = prefix itsl i in
    let itsli' = prefix itsl (i+1) in
    let tid = src itsl i in

    // k is the verifier store prior to processing ...
    let st_pre = thread_store tid itsli in
    assert(store_contains st_pre k);

    let aux ()
      : Lemma (ensures (k <> Root))
      = root_never_evicted itsl i
    in
    aux();

    FStar.Classical.exists_intro (fun tid -> store_contains (thread_store tid itsli) k) tid;
    lemma_instore k itsli;
    hash_collision_contra app

let lemma_non_eac_instore_addb
  (#app #n:_)
  (epmax: epoch)
  (itsl: neac_before_epoch app n epmax
    {let fi = eac_failure itsl in
     GB.aems_equal_upto epmax itsl /\
     EACInStore? fi.es /\ AddB? fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in

    let be' = eac_instore_addb_diff_elem itsl i in
    let ep = be'.t.e in
    not_eq (add_set ep itsl) (evict_set ep itsl) be';
    hash_collision_contra app


let lemma_non_eac_instore_addm
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     EACInStore? fi.es /\
     AddM? 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 AddM (gk,_) k k' = fi.le in
    let addm = EACInStore?.m fi.es in

    let tid_stored = stored_tid fi.bk itsli in

    (* if store already contains k, adding should cause verification failure *)
    if tid = tid_stored then
      hash_collision_contra app
    else (

      (* k' is the proving ancestor of k *)
      lemma_addm_ancestor_is_proving itsli';

      if addm = BAdd then (

        (* this implies that the "blum bit" is set to false in k' *)
        lemma_proving_ancestor_blum_bit itsli k;

        (* this leads to a verification failure *)
        eac_value_is_stored_value itsli (IntK k') tid;

        hash_collision_contra app
      )
      else (
        (* k' is in the store of tid_stored, since k is in tid_stored *)
        lemma_store_contains_proving_ancestor itsli tid_stored k;

        (* which gives a contradiction since k' has to be in a unique store *)
        key_in_unique_store k' itsli tid tid_stored;

        hash_collision_contra app
      )
    )

let lemma_non_eac_instore_evict
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     EACInStore? fi.es /\
     is_evict fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let itsli = prefix itsl i in
    let tid = src itsl i in
    let k  =  evict_slot fi.le in
    let EACInStore _ gk _ = fi.es in
    //let EvictMerkle _ v' = fi.lee in

    //let st_pre = thread_store tid itsli in
    //assert(store_contains st_pre k);
    //let gks = stored_key st_pre k in
    //let vk = HV.stored_value st_pre k in
    ext_evict_val_is_stored_val itsl i;
    //assert(v' = vk);

    //assert(AppV? v && v' <> v);
    eac_add_method_is_stored_addm itsli k;
    key_in_unique_store k itsli tid (stored_tid k itsli);
    eac_app_state_value_is_stored_value itsli gk;

    hash_collision_contra app

let lemma_non_eac_evicted_merkle_addm
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     EACEvictedMerkle? fi.es /\
     AddM? 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 AddM (gk,v) k k' = fi.le in
    let EACEvictedMerkle gk_e v_e = fi.es in

    (* k' is the proving ancestor of k *)
    lemma_addm_ancestor_is_proving itsli';
    // assert(k' = proving_ancestor itsli k);

    (* the stored value of k' points to k *)
    lemma_proving_ancestor_points_to_self itsli k;
    eac_value_is_stored_value itsli (IntK k') tid;


    assert(gk <> gk_e || v <> v_e);
    assert(to_base_key gk = to_base_key gk_e);
    if gk <> gk_e then
      let AppK k1 = gk in
      let AppK k2 = gk_e in
      KeyCollision k1 k2
    else (
      (* invariant - the proving ancestors stores the hash of evicted value v_e *)
      lemma_proving_ancestor_has_hash itsli gk;
      eac_value_is_evicted_value itsli gk;
      ValueCollision v v_e
    )

let lemma_non_eac_evicted_merkle_addb
  (#app #n:_)
  (epmax: epoch)
  (itsl: neac_before_epoch app n epmax
    {let fi = eac_failure itsl in
     GB.aems_equal_upto epmax itsl /\
     EACEvictedMerkle? fi.es /\
     is_blum_add fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let be' = eac_evictedm_addb_diff_elem itsl i in
    let ep = be'.t.e in
    not_eq (add_set ep itsl) (evict_set ep itsl) be';
    hash_collision_contra app

let lemma_non_eac_evicted_evict
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     EAC.is_eac_state_evicted fi.es /\
     is_evict fi.le})
  : GTot (hash_collision app)
  = let fi = eac_failure itsl in
    let i = fi.bi in
    let itsli = prefix itsl i in
    let tid = src itsl i in
    (* the following lemma says fi.bk does not exist in any store *)
    lemma_instore fi.bk itsli;
    assert(~ (exists_in_some_store fi.bk itsli));

    (* for verification to succeed fi.bk needs to be in store tid, a contradictio *)
    FStar.Classical.exists_intro (fun tid -> store_contains (thread_store tid itsli) fi.bk) tid;
    hash_collision_contra app

let lemma_non_eac_evicted_blum_addm
  (#app #n:_)
  (itsl: neac_log app n
    {let fi = eac_failure itsl in
     EACEvictedBlum? fi.es /\
     AddM? 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 AddM (gk,_) k k' = fi.le in

    (* k' is the proving ancestor of k *)
    lemma_addm_ancestor_is_proving itsli';
    assert(k' = proving_ancestor itsli k);

    lemma_proving_ancestor_points_to_self itsli k;
    eac_value_is_stored_value itsli (IntK k') tid;
    lemma_proving_ancestor_blum_bit itsli k;
    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 /\ EACEvictedBlum? (Mkfailure_info?.es fi) /\
          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 Zeta.EAC.uu___is_EACEvictedBlum Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bk Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__es 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.HashCollision.hash_collision_contra Prims.unit Zeta.MultiSet.not_eq Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.MultiSetHashDomain.ms_hashfn_dom_cmp Zeta.Generic.Blum.add_set Zeta.Generic.Blum.evict_set Zeta.Time.__proj__Mktimestamp__item__e Zeta.MultiSetHashDomain.__proj__MHDom__item__t Prims.op_GreaterThan Zeta.MultiSet.mem Prims.op_Equality Zeta.Generic.Interleave.blum_add_elem Zeta.High.Interleave.eac_boundary Zeta.High.Blum.eac_evictedb_addb_diff_elem Prims.nat Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bi Zeta.HashCollision.hash_collision
let lemma_non_eac_evicted_blum_addb
      (#app #n: _)
      (epmax: epoch)
      (itsl:
          neac_before_epoch app n epmax
            { let fi = eac_failure itsl in
              GB.aems_equal_upto epmax itsl /\ EACEvictedBlum? fi.es /\ AddB? fi.le })
    : GTot (hash_collision app) =
  
let fi = eac_failure itsl in
let i = fi.bi in
let be = eac_evictedb_addb_diff_elem itsl in
let ep = be.t.e in
not_eq (add_set ep itsl) (evict_set ep itsl) be;
hash_collision_contra app