val eac_state_transition
  (#app: app_params)
  (k: base_key)
  (l: vlog_ext app {length l > 0})
  : Lemma (ensures (let open Zeta.SeqAux in
                    let n = length l - 1 in
                    let l' = prefix l n in
                    let ee = index l n in
                    let es' = eac_state_of_key k l' in
                    let es = eac_state_of_key k l in
                    es = eac_add ee es'))
           [SMTPat (eac_state_of_key k l)]
val eac_state_transition
  (#app: app_params)
  (k: base_key)
  (l: vlog_ext app {length l > 0})
  : Lemma (ensures (let open Zeta.SeqAux in
                    let n = length l - 1 in
                    let l' = prefix l n in
                    let ee = index l n in
                    let es' = eac_state_of_key k l' in
                    let es = eac_state_of_key k l in
                    es = eac_add ee es'))
           [SMTPat (eac_state_of_key k l)]
let eac_state_transition
  (#app: app_params)
  (k: base_key)
  (l: vlog_ext app {length l > 0})
  : Lemma (ensures (let open Zeta.SeqAux in
                    let n = length l - 1 in
                    let l' = prefix l n in
                    let ee = index l n in
                    let es' = eac_state_of_key k l' in
                    let es = eac_state_of_key k l in
                    es = eac_add ee es'))
          [SMTPat (eac_state_of_key k l)]
  = let n = length l - 1 in
    let l' = prefix l n in
    let ee = index l n in
    let smk = eac_smk app k in
    lemma_hprefix_append_telem l;
    lemma_reduce_append (init_state smk) (trans_fn smk) l' ee
module Zeta.EAC

open FStar.Classical

open Zeta.SeqMachine
open Zeta.SeqAux

let empty_log_implies_init_state
  (#app: _)
  (k: base_key)
  (l: vlog_ext app{length l = 0})
  : Lemma (ensures (eac_state_of_key k l = EACInit))
  = let smk = eac_smk app k in
    lemma_empty_seq_init smk l
/
Zeta.SeqMachine.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.EAC.fst
k: Zeta.GenericVerifier.base_key -> l: Zeta.EAC.vlog_ext app {FStar.Seq.Base.length l > 0}
  -> FStar.Pervasives.Lemma
      (ensures
        (let n = FStar.Seq.Base.length l - 1 in
          let l' = Zeta.SeqAux.prefix l n in
          let ee = FStar.Seq.Base.index l n in
          let es' = Zeta.EAC.eac_state_of_key k l' in
          let es = Zeta.EAC.eac_state_of_key k l in
          es = Zeta.EAC.eac_add ee es')) [SMTPat (Zeta.EAC.eac_state_of_key k l)]
Zeta.App.app_params Zeta.GenericVerifier.base_key Zeta.EAC.vlog_ext Prims.b2t Prims.op_GreaterThan FStar.Seq.Base.length Zeta.EAC.vlog_entry_ext Zeta.SeqAux.lemma_reduce_append Zeta.SeqMachine.state_type Zeta.SeqMachine.init_state Zeta.SeqMachine.trans_fn Prims.unit Zeta.SeqAux.lemma_hprefix_append_telem Zeta.SeqMachine.seq_machine Zeta.EAC.eac_smk FStar.Seq.Base.index FStar.Seq.Base.seq Prims.op_Equality Prims.nat Zeta.SeqAux.prefix Prims.int Prims.op_Subtraction Prims.l_True Prims.squash Zeta.EAC.eac_state Zeta.EAC.eac_add Zeta.EAC.eac_state_of_key Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let eac_state_transition (#app: app_params) (k: base_key) (l: vlog_ext app {length l > 0})
    : Lemma
      (ensures
        (let open Zeta.SeqAux in
          let n = length l - 1 in
          let l' = prefix l n in
          let ee = index l n in
          let es' = eac_state_of_key k l' in
          let es = eac_state_of_key k l in
          es = eac_add ee es')) [SMTPat (eac_state_of_key k l)] =
  
let n = length l - 1 in
let l' = prefix l n in
let ee = index l n in
let smk = eac_smk app k in
lemma_hprefix_append_telem l;
lemma_reduce_append (init_state smk) (trans_fn smk) l' ee