val nevict_vlog_entry : app: Zeta.App.app_params -> Type0
let nevict_vlog_entry (app: app_params) = e:(vlog_entry app) {not (is_evict 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}
/
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
app: Zeta.App.app_params -> Type0
Zeta.App.app_params Zeta.High.Verifier.vlog_entry Prims.b2t Prims.op_Negation Zeta.GenericVerifier.is_evict Zeta.High.Verifier.high_verifier_spec
let nevict_vlog_entry (app: app_params) =
  
e: (vlog_entry app){not (is_evict e)}