val to_vlog_entry (#app: _) (ee: vlog_entry_ext app) : vlog_entry app
val to_vlog_entry (#app: _) (ee: vlog_entry_ext app) : vlog_entry app
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
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
/
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 -> Zeta.High.Verifier.vlog_entry app
Zeta.App.app_params Zeta.EAC.vlog_entry_ext Zeta.High.Verifier.vlog_entry Prims.b2t Zeta.GenericVerifier.is_merkle_evict Zeta.High.Verifier.high_verifier_spec Zeta.Record.value Zeta.GenericVerifier.is_blum_evict Zeta.GenericVerifier.thread_id Prims.op_AmpAmp Zeta.GenericVerifier.is_internal Prims.op_Negation Zeta.GenericVerifier.is_evict Prims.l_and Zeta.GenericVerifier.is_appfn Zeta.SeqAux.distinct_elems Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Zeta.GenericVerifier.__proj__RunApp__item__rs Zeta.App.appfn_rs_t Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.GenericVerifier.__proj__RunApp__item__f Prims.op_Equality Prims.nat FStar.Seq.Base.length Zeta.App.app_record Zeta.App.__proj__Mkapp_params__item__adm
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