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

    itsl:
      Zeta.High.Interleave.neac_log app n
        { let fi = Zeta.High.Verifier.EAC.eac_failure itsl in
          EACInStore? (Mkfailure_info?.es fi) /\
          Zeta.High.Verifier.refs_key (Mkfailure_info?.le fi) (Mkfailure_info?.bk fi) /\
          RunApp? (Mkfailure_info?.le fi) }
  -> Prims.GTot (Zeta.HashCollision.hash_collision app)
Zeta.App.app_params Prims.pos Zeta.High.Interleave.neac_log Prims.l_and Prims.b2t Zeta.EAC.uu___is_EACInStore Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bk Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__es Zeta.High.Verifier.refs_key Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__le Zeta.GenericVerifier.uu___is_RunApp Zeta.High.Verifier.high_verifier_spec Zeta.High.Verifier.EAC.failure_info Zeta.High.Verifier.EAC.eac_failure Zeta.App.appfn_id Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.App.appfn_arg FStar.Seq.Base.seq Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Zeta.App.appfn_rs_t Zeta.GenericVerifier.__proj__RunApp__item__f Zeta.GenericVerifier.RunApp Prims.op_Equality Prims.nat FStar.Seq.Base.length Zeta.App.app_record Zeta.App.__proj__Mkapp_params__item__adm Zeta.GenericVerifier.__proj__RunApp__item__rs Zeta.High.Verifier.add_method Zeta.GenKey.key Zeta.Key.base_key Zeta.GenKey.to_base_key Zeta.Record.value_t Prims.op_Negation Zeta.High.Verifier.EAC.lemma_non_eac_appfn_non_refs Prims.bool Zeta.App.app_key Zeta.App.app_value_nullable Zeta.HashCollision.hash_collision_contra Prims.unit Prims._assert Zeta.Record.value Zeta.Record.AppV Zeta.High.Interleave.eac_app_state_value_is_stored_value Zeta.GenKey.AppK Zeta.High.Interleave.key_in_unique_store Zeta.High.Interleave.stored_tid Zeta.High.Verifier.stored_value Zeta.High.Verifier.stored_key Zeta.HashCollision.hash_collision FStar.Seq.Base.index Zeta.High.Interleave.ext_app_records_is_stored_val Zeta.High.Verifier.runapp_implies_store_contains Zeta.High.Verifier.store_t Zeta.High.Interleave.thread_store_pre Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__vtls_t Zeta.Generic.Interleave.cur_thread_state_pre FStar.Seq.Properties.index_mem Zeta.EAC.eac_state Zeta.EAC.vlog_entry_ext Zeta.High.Verifier.vlog_entry Zeta.EAC.to_vlog_entry Zeta.EAC.eac_add Zeta.EAC.EACFail Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__lee Prims.op_LessThan Zeta.Interleave.src Zeta.GenericVerifier.verifier_log_entry Zeta.Interleave.interleaving Zeta.Interleave.prefix Prims.op_Addition Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bi
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
  (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);
    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)