val induction_props : ils: Zeta.Intermediate.Interleave.verifiable_log vcfg -> Prims.GTot Prims.logical
let induction_props #vcfg (ils: verifiable_log vcfg) =
  let ilk = to_logk ils in
  spec_rel ils /\
  is_eac ilk
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"

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)

#pop-options

(*
 * A bunch of properties we use in the induction step:
 *    (a) the intermediate verifiers all satisfy the store invariant
 *    (b) the intermediate and spec level verifiers states correspond to one-another (related)
 *    (c) the spec level log is time sorted (b and c imply that the spec log has type its_log)
 *    (d) the spec level log is evict-add-consistent
 * TODO: rename this
 *)
#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
ils: Zeta.Intermediate.Interleave.verifiable_log vcfg -> Prims.GTot Prims.logical
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Interleave.verifiable_log Prims.l_and Zeta.Intermediate.Interleave.spec_rel Prims.b2t Zeta.High.Interleave.is_eac Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__thread_count Zeta.High.Interleave.ilog Zeta.Intermediate.Interleave.to_logk Prims.logical
let induction_props #vcfg (ils: verifiable_log vcfg) =
  
let ilk = to_logk ils in
spec_rel ils /\ is_eac ilk