val eac_empty_log
  (#app: app_params)
  (l: vlog_ext app {length l = 0})
  : Lemma (ensures (eac l))
val eac_empty_log
  (#app: app_params)
  (l: vlog_ext app {length l = 0})
  : Lemma (ensures (eac l))
let eac_empty_log
  (#app: app_params)
  (l: vlog_ext app {length l = 0})
  : Lemma (ensures (eac l))
          [SMTPat (eac l)]
  = lemma_empty l;
    let aux (k: base_key)
        : Lemma (ensures (valid (eac_smk app k) l))
                  [SMTPat (valid (eac_smk app k) l)]
      = lemma_empty_seq_valid (eac_smk app k)
    in
    ()
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

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
/
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
l: Zeta.EAC.vlog_ext app {FStar.Seq.Base.length l = 0}
  -> FStar.Pervasives.Lemma (ensures Zeta.EAC.eac l)
Zeta.App.app_params Zeta.EAC.vlog_ext Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length Zeta.EAC.vlog_entry_ext Zeta.GenericVerifier.base_key Prims.unit Prims.l_True Prims.squash Zeta.SeqMachine.valid Zeta.EAC.eac_smk Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.bool Prims.Nil Zeta.SeqMachine.lemma_empty_seq_valid FStar.Seq.Base.lemma_empty Zeta.EAC.eac Prims.logical
let eac_empty_log (#app: app_params) (l: vlog_ext app {length l = 0})
    : Lemma (ensures (eac l)) [SMTPat (eac l)] =
  
lemma_empty l;
let aux (k: base_key) : Lemma (ensures (valid (eac_smk app k) l)) [SMTPat (valid (eac_smk app k) l)]
=
  lemma_empty_seq_valid (eac_smk app k)
in
()