val is_merkle_evict (#vspec: _) (e: verifier_log_entry vspec) : bool
val is_merkle_evict (#vspec: _) (e: verifier_log_entry vspec) : bool
let is_merkle_evict #vspec (e:verifier_log_entry vspec): bool =
  match e with
  | EvictM _ _ -> true
  | _ -> false
module Zeta.GenericVerifier

open Zeta.Ghost
open Zeta.App
open Zeta.AppSimulate
open Zeta.Time
open Zeta.MultiSetHashDomain
open Zeta.Record

module S = FStar.Seq
module SA = Zeta.SeqAux
module MSD = Zeta.MultiSetHashDomain

(* identifier type for verifier threads *)
let thread_id = Zeta.Thread.thread_id

let base_key = Zeta.Key.base_key
let key_lt = Zeta.BinTree.lt

(* The basic "structure" of a verifier specification. We are interested in specifications that
 * satisfy additional properties as described below. *)
noeq
type verifier_spec_base = {

  (* type of the verifier thread local state *)
  vtls_t: Type0;

  (* is the verifier state valid, indicating no verification failures *)
  valid: vtls_t -> bool;

  (* generate a invalid state *)
  fail: vtls_t -> vtls: vtls_t {not (valid vtls)};

  (* clock of a verifier thread. *)
  clock: vtls:vtls_t{valid vtls} -> timestamp;

  (* last merkle added blum evicted key *)
  last_evict_key: vtls:vtls_t{valid vtls} -> base_key;

  (* thread_id of the verifier thread; thread_id can be accessed even in a failed state *)
  tid: vtls_t -> thread_id;

  (* initialize the thread local state for a particular thread id *)
  init: t:thread_id -> vtls: vtls_t { valid vtls /\ tid vtls = t };

  (* type used to identify records (e.g., keys, slots) *)
  slot_t: eqtype;

  (* application specification *)
  app: app_params;

  (* get a record from the store - this could fail and return None *)
  get: slot_t -> vtls: vtls_t {valid vtls} -> GTot (option (record app));

  (* update the record in a slot with a new value *)
  puts: vtls: vtls_t { valid vtls } ->
        ss: S.seq slot_t ->
        ws: S.seq (app_value_nullable app.adm) ->
        GTot (vtls': vtls_t { valid vtls });

  (* implementation of merkle add *)
  addm: record app -> slot_t -> slot_t -> vtls: vtls_t { valid vtls } -> GTot vtls_t;

  (* implementation of blum add *)
  addb: record app -> slot_t -> timestamp -> thread_id -> vtls: vtls_t { valid vtls } -> GTot vtls_t;

  (* implementation of merkle evict *)
  evictm: slot_t -> slot_t -> vtls: vtls_t { valid vtls } -> GTot vtls_t;

  (* implementation of blum evict *)
  evictb: slot_t -> timestamp -> vtls: vtls_t { valid vtls } -> GTot vtls_t;

  (* implementation of blum evict for records added using merkle *)
  evictbm: slot_t -> slot_t -> timestamp -> vtls: vtls_t { valid vtls } -> GTot vtls_t;

  nextepoch: vtls: vtls_t { valid vtls } -> vtls_t;

  verifyepoch: vtls: vtls_t { valid vtls } -> vtls_t;
}

let clock_evict_key (#vspec: verifier_spec_base) (vtls: vspec.vtls_t {vspec.valid vtls})
  : Zeta.TimeKey.timestamp_key
  = vspec.clock vtls, vspec.last_evict_key vtls

type verifier_log_entry (vspec: verifier_spec_base): eqtype =
  | AddM: r: record vspec.app -> s: vspec.slot_t -> s': vspec.slot_t -> verifier_log_entry vspec
  | AddB: r: record vspec.app -> s: vspec.slot_t -> t: timestamp -> tid: thread_id -> verifier_log_entry vspec
  | EvictM: s: vspec.slot_t -> s': vspec.slot_t -> verifier_log_entry vspec
  | EvictB: s: vspec.slot_t -> t: timestamp -> verifier_log_entry vspec
  | EvictBM: s: vspec.slot_t -> s': vspec.slot_t -> t: timestamp -> verifier_log_entry vspec
  | NextEpoch: verifier_log_entry vspec
  | VerifyEpoch: verifier_log_entry vspec
  | RunApp: f: appfn_id vspec.app ->
            p: appfn_arg f ->
            rs: S.seq (vspec.slot_t) ->
            verifier_log_entry vspec

let is_appfn #vspec (e: verifier_log_entry vspec)
  = RunApp? e

let param_len #vspec (e: verifier_log_entry vspec{is_appfn e})
  = let RunApp _ _ rs = e in
    S.length rs

let is_internal #vspec (e: verifier_log_entry vspec)
  = not (is_appfn e)

let is_blum_add #vspec (e: verifier_log_entry vspec) = AddB? e

let blum_add_timestamp #vspec (e: verifier_log_entry vspec {is_blum_add e})
  : timestamp
  = match e with
    | AddB _ _ t _ -> t

let is_evict #vspec (e: verifier_log_entry vspec): bool =
  match e with
  | EvictM _ _ -> true
  | EvictB _ _ -> true
  | EvictBM _ _ _ -> true
  | _ -> false

let evict_slot #vspec (e: verifier_log_entry vspec{is_evict e})
  = match e with
    | EvictM s _ -> s
    | EvictB s _ -> s
    | EvictBM s _ _ -> s

let is_blum_evict #vspec (e: verifier_log_entry vspec) =
  match e with
  | EvictB _ _ -> true
  | EvictBM _ _ _ -> true
  | _ -> false

let blum_evict_timestamp #vspec (e: verifier_log_entry vspec {is_blum_evict e})
  = match e with
    | EvictB _ t -> t
    | EvictBM _ _ t -> t
/
Zeta.TimeKey.fsti.checked Zeta.Time.fsti.checked Zeta.Thread.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.Key.fsti.checked Zeta.Ghost.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.GenericVerifier.fsti
e: Zeta.GenericVerifier.verifier_log_entry vspec -> Prims.bool
Zeta.GenericVerifier.verifier_spec_base Zeta.GenericVerifier.verifier_log_entry Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Prims.bool
let is_merkle_evict #vspec (e: verifier_log_entry vspec) : bool =
  
match e with
| EvictM _ _ -> true
| _ -> false