val valid_logS_entry (#vcfg: _) (ssm: slot_state_map vcfg) (e: logS_entry vcfg) : bool
val valid_logS_entry (#vcfg: _) (ssm: slot_state_map vcfg) (e: logS_entry vcfg) : bool
let valid_logS_entry #vcfg (ssm: slot_state_map vcfg) (e: logS_entry vcfg): bool =
  let open Zeta.GenericVerifier in
  match e with
  | AddM r s s' ->
    is_free ssm s && is_assoc ssm s'
  | AddB r s  _ _ ->
    is_free ssm s
  | EvictM s s' ->
    is_assoc ssm s && is_assoc ssm s'
  | EvictB s _ ->
    is_assoc ssm s
  | EvictBM s s' _ ->
    is_assoc ssm s && is_assoc ssm s'
  | RunApp _ _ ss ->
    all_slots_assoc_comp ssm ss
  | VerifyEpoch
  | NextEpoch -> true
module Zeta.Intermediate.Logs

open FStar.Seq
open Zeta.SeqAux
open Zeta.Key
open Zeta.App
open Zeta.GenKey
open Zeta.Intermediate.VerifierConfig
open Zeta.Intermediate.SlotKeyRel
open Zeta.Intermediate.Verifier

module GV = Zeta.GenericVerifier
module HV = Zeta.High.Verifier


(* Definitions of different styles of verifier logs.
   - logK : contains only key references
   - logS: contains slot references
   - logL: contains slot references & low-level data structures (TODO) *)


let logK_entry = HV.vlog_entry

let logS vcfg = seq (logS_entry vcfg)

let logK vcfg = seq (logK_entry vcfg.app)

(* all slots in a seq associated with a key *)
let all_slots_assoc (#vcfg:_) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg))
  = forall i. (is_assoc ssm (index ss i))

val all_slots_assoc_comp (#vcfg:_) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg))
  : b:bool{b <==> all_slots_assoc ssm ss}

(*
 * Given a slot -> key mapping, we define a boolean whether a log entry is valid.
 * This definition checks if the slots are used correctly:
 * (a) We add to a slot only if it is free
 * (b) We evict from a slot only if it is associated with a key
 * (c) We reference a slot in Get/Put and as an ancestor in Add/Evict only if it is associated with a key
/
Zeta.SeqAux.fsti.checked Zeta.Key.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.SlotKeyRel.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.Logs.fsti

    ssm: Zeta.Intermediate.SlotKeyRel.slot_state_map vcfg ->
    e: Zeta.Intermediate.Verifier.logS_entry vcfg
  -> Prims.bool
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.SlotKeyRel.slot_state_map Zeta.Intermediate.Verifier.logS_entry Zeta.Record.record Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Intermediate.Verifier.int_verifier_spec Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__slot_t Prims.op_AmpAmp Zeta.Intermediate.SlotKeyRel.is_free Zeta.Intermediate.SlotKeyRel.is_assoc Zeta.Time.timestamp Zeta.GenericVerifier.thread_id Zeta.App.appfn_id Zeta.App.appfn_arg FStar.Seq.Base.seq Zeta.Intermediate.Logs.all_slots_assoc_comp Prims.bool
let valid_logS_entry #vcfg (ssm: slot_state_map vcfg) (e: logS_entry vcfg) : bool =
  
let open Zeta.GenericVerifier in
match e with
| AddM r s s' -> is_free ssm s && is_assoc ssm s'
| AddB r s _ _ -> is_free ssm s
| EvictM s s' -> is_assoc ssm s && is_assoc ssm s'
| EvictB s _ -> is_assoc ssm s
| EvictBM s s' _ -> is_assoc ssm s && is_assoc ssm s'
| RunApp _ _ ss -> all_slots_assoc_comp ssm ss
| VerifyEpoch | NextEpoch -> true