val lemma_eac_boundary_inv (#app: _) (#n: pos) (il: HI.verifiable_log app n) (i: seq_index il)
    : Lemma
      (requires
        (let _il = prefix il i in
          let il_ = prefix il (i + 1) in
          is_eac _il /\ not (is_eac il_))) (ensures (eac_boundary il = i)) [SMTPat (prefix il i)]
val lemma_eac_boundary_inv (#app: _) (#n: pos) (il: HI.verifiable_log app n) (i: seq_index il)
    : Lemma
      (requires
        (let _il = prefix il i in
          let il_ = prefix il (i + 1) in
          is_eac _il /\ not (is_eac il_))) (ensures (eac_boundary il = i)) [SMTPat (prefix il i)]
let lemma_eac_boundary_inv (#app:_) (#n:pos) (il: HI.verifiable_log app n) (i: seq_index il)
  : Lemma (requires (let _il = prefix il i in
                     let il_ = prefix il (i+1) in
                     is_eac _il /\ not (is_eac il_)))
          (ensures (eac_boundary il = i))
          [SMTPat (prefix il i)]
  = let _il = prefix il i in
    let il_ = prefix il (i+1) in
    let i' = eac_boundary il in
    if i' < i then
      lemma_eac_implies_prefix_eac _il (i'+1)
    else if i < i' then
      lemma_eac_implies_prefix_eac (prefix il i') (i+1)
module Zeta.Intermediate.Correctness

open FStar.Classical
open Zeta.BinTree
open Zeta.MultiSet
open Zeta.SeqIdx
open Zeta.App
open Zeta.AppSimulate
open Zeta.MultiSetHashDomain
open Zeta.Key
open Zeta.GenKey
open Zeta.Record
open Zeta.Time
open Zeta.HashCollision
open Zeta.Generic.Global
open Zeta.Generic.Blum
open Zeta.Intermediate.Global
open Zeta.Interleave
open Zeta.Generic.Interleave
open Zeta.Generic.Blum
open Zeta.Generic.TSLog
open Zeta.EAC
open Zeta.High.Interleave
open Zeta.High.Blum
open Zeta.High.Merkle
open Zeta.High.Verifier.EAC
open Zeta.Intermediate.VerifierConfig
open Zeta.Intermediate.Store
open Zeta.Intermediate.Verifier
open Zeta.Intermediate.StateRel
open Zeta.Intermediate.Interleave
open Zeta.Intermediate.TSLog
open Zeta.Intermediate.Blum

module S = FStar.Seq
module SA = Zeta.SeqAux
module GV = Zeta.GenericVerifier
module GG = Zeta.Generic.Global
module HI = Zeta.High.Interleave
module HV = Zeta.High.Verifier
module HM = Zeta.High.Merkle
module EAC = Zeta.EAC
module M = Zeta.Merkle
module FE = FStar.FunctionalExtensionality

#push-options "--fuel 0 --ifuel 1 --query_stats"
/
Zeta.Time.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.TSLog.fsti.checked Zeta.Intermediate.Store.fsti.checked Zeta.Intermediate.StateRel.fsti.checked Zeta.Intermediate.Interleave.fsti.checked Zeta.Intermediate.Global.fsti.checked Zeta.Intermediate.Blum.fsti.checked Zeta.Interleave.fsti.checked Zeta.High.Verifier.EAC.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.High.SeqConsistent.fsti.checked Zeta.High.Merkle.fsti.checked Zeta.High.Interleave.fsti.checked Zeta.High.Blum.fsti.checked Zeta.HashCollision.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.TSLog.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.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.Correctness.fst
il: Zeta.High.Interleave.verifiable_log app n -> i: Zeta.Generic.Interleave.seq_index il
  -> FStar.Pervasives.Lemma
      (requires
        (let _il = Zeta.Generic.Interleave.prefix il i in
          let il_ = Zeta.Generic.Interleave.prefix il (i + 1) in
          Zeta.High.Interleave.is_eac _il /\ Prims.op_Negation (Zeta.High.Interleave.is_eac il_)))
      (ensures Zeta.High.Interleave.eac_boundary il = i)
      [SMTPat (Zeta.Generic.Interleave.prefix il i)]
Zeta.App.app_params Prims.pos Zeta.High.Interleave.verifiable_log Zeta.Generic.Interleave.seq_index Zeta.High.Verifier.high_verifier_spec Prims.op_LessThan Zeta.High.Interleave.lemma_eac_implies_prefix_eac Prims.op_Addition Prims.bool Zeta.Generic.Interleave.prefix Prims.unit Prims.l_and Prims.b2t Zeta.High.Interleave.is_eac Zeta.SeqAux.prefix Zeta.Interleave.elem_src Zeta.GenericVerifier.verifier_log_entry Prims.l_not Zeta.High.Interleave.eac_boundary Zeta.Generic.Interleave.verifiable_log Prims.op_Equality Prims.nat Zeta.Generic.Interleave.length Prims.op_Negation Prims.squash Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let lemma_eac_boundary_inv (#app: _) (#n: pos) (il: HI.verifiable_log app n) (i: seq_index il)
    : Lemma
      (requires
        (let _il = prefix il i in
          let il_ = prefix il (i + 1) in
          is_eac _il /\ not (is_eac il_))) (ensures (eac_boundary il = i)) [SMTPat (prefix il i)] =
  
let _il = prefix il i in
let il_ = prefix il (i + 1) in
let i' = eac_boundary il in
if i' < i
then lemma_eac_implies_prefix_eac _il (i' + 1)
else if i < i' then lemma_eac_implies_prefix_eac (prefix il i') (i + 1)