val eac_add_app (#app #ks: _) (ee: vlog_entry_ext app {App? ee}) (s: eac_state app ks)
    : eac_state app ks
val eac_add_app (#app #ks: _) (ee: vlog_entry_ext app {App? ee}) (s: eac_state app ks)
    : eac_state app ks
let eac_add_app #app #ks (ee: vlog_entry_ext app {App? ee}) (s: eac_state app ks)
  : eac_state app ks
  = let e = to_vlog_entry ee in
    let App (RunApp f p refkeys) rs = ee in
    let fn = appfn f in
    let rc,_,ws = fn p rs in

    (* any app failure leads to eac failure *)
    if rc = Fn_failure then EACFail
    (* propagate state if e does not ref the key we are tracking *)
    else if not (e `refs_key` ks) then s
    else
      match s with
      | EACInStore m gk v ->
        let idx = index_mem ks refkeys in
        let (gk',v') = index rs idx in
        if AppV v' <> v then EACFail
        else if AppK gk' <> gk then EACFail
        else
          let v = AppV (index ws idx) in
          EACInStore m gk v
      | _ -> EACFail
module Zeta.EAC

open FStar.Seq
open Zeta.SeqMachine
open Zeta.Time
open Zeta.Key
open Zeta.App
open Zeta.AppSimulate
open Zeta.GenKey
open Zeta.Record
open Zeta.GenericVerifier
open Zeta.High.Verifier

let evict_vlog_entry (app: app_params) = e:(vlog_entry app) {is_evict e}

let nevict_vlog_entry (app: app_params) = e:(vlog_entry app) {not (is_evict e)}

type vlog_entry_ext (app: app_params) =
  | NEvict: e:vlog_entry app{is_internal e && not (is_evict e)} -> vlog_entry_ext app
  | EvictMerkle: e:vlog_entry app{is_merkle_evict e} -> v:value app -> vlog_entry_ext app
  | EvictBlum: e:vlog_entry app{is_blum_evict e} -> v:value app -> tid:thread_id -> vlog_entry_ext app
  | App: e:vlog_entry app{is_appfn e /\ Zeta.SeqAux.distinct_elems (RunApp?.rs e)} ->
         rs: appfn_rs_t (RunApp?.f e) { length rs = length (RunApp?.rs e) }   -> vlog_entry_ext app

let vlog_ext (app: app_params) = seq (vlog_entry_ext app)

type eac_state (app: app_params) (k: base_key) =
  | EACFail: eac_state app k
  | EACInit: eac_state app k
  | EACInStore: m:add_method -> gk:key app {to_base_key gk = k} -> v:value_t gk -> eac_state app k
  | EACEvictedMerkle: gk:key app {to_base_key gk = k} -> v:value_t gk -> eac_state app k
  | EACEvictedBlum: gk: key app{to_base_key gk = k} -> v:value_t gk -> t:timestamp -> j:thread_id -> eac_state app k

let is_eac_state_evicted #app #k (s: eac_state app k): bool =
  match s with
  | EACEvictedMerkle _ _ -> true
  | EACEvictedBlum _ _ _ _ -> true
  | _ -> false

let is_eac_state_instore #app #k (s: eac_state app k): bool =
  match s with
  | EACInStore _ _ _ -> true
  | _ -> false

let is_eac_state_active #app #k (s: eac_state app k)
  = s <> EACInit && s <> EACFail

let gen_key_inferrable #app #k (s: eac_state app k)
  = is_merkle_key k ||
    is_eac_state_active s

let to_gen_key #app #k (s: eac_state app k{gen_key_inferrable s})
  = if is_merkle_key k then IntK k
    else
    match s with
    | EACInStore _ gk _ -> gk
    | EACEvictedMerkle gk _ -> gk
    | EACEvictedBlum gk _ _ _ -> gk

let to_vlog_entry #app (ee:vlog_entry_ext app): vlog_entry app =
  match ee with
  | EvictMerkle e _ -> e
  | EvictBlum e _ _ -> e
  | NEvict e -> e
  | App e _ -> e
/
Zeta.Time.fsti.checked Zeta.SeqMachine.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.Key.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.EAC.fsti
ee: Zeta.EAC.vlog_entry_ext app {App? ee} -> s: Zeta.EAC.eac_state app ks
  -> Zeta.EAC.eac_state app ks
Zeta.App.app_params Zeta.GenericVerifier.base_key Zeta.EAC.vlog_entry_ext Prims.b2t Zeta.EAC.uu___is_App Zeta.EAC.eac_state Zeta.App.appfn_id Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.High.Verifier.high_verifier_spec Zeta.App.appfn_arg FStar.Seq.Base.seq Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Zeta.App.appfn_rs_t Zeta.GenericVerifier.__proj__RunApp__item__f Zeta.GenericVerifier.RunApp Prims.op_Equality Prims.nat FStar.Seq.Base.length Zeta.App.app_record Zeta.App.__proj__Mkapp_params__item__adm Zeta.GenericVerifier.__proj__RunApp__item__rs Zeta.App.fn_return_code Zeta.App.interp_code Zeta.App.__proj__Mkfn_sig__item__fres_t FStar.Map.sel Zeta.App.fn_id Zeta.App.fn_sig Zeta.App.__proj__Mkapp_params__item__tbl Zeta.App.app_value_nullable Prims.eq2 Zeta.App.__proj__Mkfn_sig__item__arity Zeta.App.Fn_failure Zeta.EAC.EACFail Prims.bool Prims.op_Negation Zeta.High.Verifier.refs_key Zeta.High.Verifier.add_method Zeta.GenKey.key Zeta.Key.base_key Zeta.GenKey.to_base_key Zeta.Record.value_t Zeta.App.app_key Prims.op_disEquality Zeta.Record.value Zeta.Record.AppV Zeta.GenKey.AppK Zeta.EAC.EACInStore FStar.Seq.Base.index FStar.Seq.Properties.index_mem FStar.Pervasives.Native.tuple3 Zeta.App.app_fn_t Zeta.App.__proj__Mkfn_sig__item__farg_t Zeta.App.appfn Zeta.High.Verifier.vlog_entry Zeta.EAC.to_vlog_entry
let eac_add_app #app #ks (ee: vlog_entry_ext app {App? ee}) (s: eac_state app ks) : eac_state app ks =
  
let e = to_vlog_entry ee in
let App (RunApp f p refkeys) rs = ee in
let fn = appfn f in
let rc, _, ws = fn p rs in
if rc = Fn_failure
then EACFail
else
  if not (e `refs_key` ks)
  then s
  else
    match s with
    | EACInStore m gk v ->
      let idx = index_mem ks refkeys in
      let gk', v' = index rs idx in
      if AppV v' <> v
      then EACFail
      else
        if AppK gk' <> gk
        then EACFail
        else
          let v = AppV (index ws idx) in
          EACInStore m gk v
    | _ -> EACFail