val 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)
val 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 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
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 }
/
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
          Prims.op_Negation (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 Prims.op_Negation Zeta.High.Verifier.refs_key Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__le Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bk Zeta.GenericVerifier.uu___is_RunApp Zeta.High.Verifier.high_verifier_spec Zeta.High.Verifier.EAC.failure_info Zeta.High.Verifier.EAC.eac_failure Zeta.HashCollision.hash_collision_contra Prims.unit Zeta.High.Interleave.ext_app_records_is_stored_val Prims.nat Zeta.High.Verifier.EAC.__proj__Mkfailure_info__item__bi Zeta.HashCollision.hash_collision
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