val eac_failure (#app #n: _) (il: neac_log app n) : GTot (failure_info app n)
val eac_failure (#app #n: _) (il: neac_log app n) : GTot (failure_info app n)
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 }
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};
}
/
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
il: Zeta.High.Interleave.neac_log app n -> Prims.GTot (Zeta.High.Verifier.EAC.failure_info app n)
Zeta.App.app_params Prims.pos Zeta.High.Interleave.neac_log Zeta.High.Verifier.EAC.Mkfailure_info Prims.unit Zeta.High.Interleave.eac_state_transition Zeta.Generic.Interleave.lemma_cur_thread_state_extend Zeta.High.Verifier.high_verifier_spec Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__vtls_t Zeta.Generic.Interleave.cur_thread_state_post Zeta.Generic.Interleave.cur_thread_state_pre Zeta.EAC.vlog_entry_ext Zeta.High.Interleave.mk_vlog_entry_ext Zeta.GenericVerifier.verifier_log_entry Zeta.Interleave.index Zeta.EAC.eac_state Zeta.High.Interleave.eac_state_of_key_pre Zeta.GenericVerifier.base_key Prims.l_and Prims.b2t Prims.op_Equality Zeta.High.Interleave.eac_state_of_key_post Zeta.High.Interleave.eac_boundary Zeta.EAC.EACFail Prims.op_disEquality Zeta.High.Verifier.refs_key Zeta.High.Interleave.eac_fail_key Zeta.Generic.Interleave.seq_index Zeta.High.Interleave.is_eac Zeta.SeqAux.prefix Zeta.Interleave.elem_src Prims.l_not Prims.op_Addition Zeta.High.Verifier.EAC.failure_info
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 = bi; bk = bk; es = es; le = le; lee = lee; vs_pre = vs_pre; vs_post = vs_post }