val slot_state_trans_closure (#vcfg: _) (s: slot_id vcfg) (l: logS vcfg) (sst_init: slot_state)
    : Tot (option slot_state) (decreases (length l))
val slot_state_trans_closure (#vcfg: _) (s: slot_id vcfg) (l: logS vcfg) (sst_init: slot_state)
    : Tot (option slot_state) (decreases (length l))
let rec slot_state_trans_closure #vcfg (s:slot_id vcfg) (l:logS vcfg) (sst_init: slot_state)
  : Tot (option slot_state) (decreases (length l)) =
  let n = length l in
  if n = 0 then Some (sst_init)
  else
    let l' = hprefix l in
    let e = telem l in
    let osst' = slot_state_trans_closure s l' sst_init in
    if None? osst' then None
    else if not (has_distinct_slots e) then None
    else
      slot_state_trans e s (Some?.v osst')
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
 *)
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

let to_key (#vcfg:_) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg) {all_slots_assoc ssm ss}) (i: seq_index ss)
  : base_key
  = let s = index ss i in
    assert(is_assoc ssm s);
    assoc_key ssm s

let to_key_seq (#vcfg:_) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg){all_slots_assoc ssm ss})
  : seq base_key
  = init (length ss) (to_key ssm ss)

let to_logk_entry #vcfg (ssm: slot_state_map vcfg) (e: logS_entry vcfg{valid_logS_entry ssm e})
  : logK_entry vcfg.app
  = let open Zeta.GenericVerifier in
    let vspec = HV.high_verifier_spec vcfg.app in
    match e with
    | AddM (gk,gv) s s' -> AddM (gk,gv) (to_base_key gk)  (assoc_key ssm s')
    | AddB (gk,gv) s t j -> AddB (gk,gv) (to_base_key gk) t j
    | EvictM s s' -> EvictM (assoc_key ssm s) (assoc_key ssm s')
    | EvictB s t -> EvictB (assoc_key ssm s) t
    | EvictBM s s' t -> EvictBM (assoc_key ssm s) (assoc_key ssm s') t
    | VerifyEpoch -> VerifyEpoch
    | NextEpoch -> NextEpoch
    | RunApp f p ss -> let ks: seq (vspec.slot_t) = to_key_seq ssm ss in
                       let f: appfn_id vspec.app = f in
                       RunApp f p ks

(*
 * define a state machine over slot_states; to allow for "failures" where the log
 * uses slot states in an inconsistent manner (e.g., evict a slot without adding to it)
 * we make the transition function return option slot_state, with None being failure.
 *)
let slot_state_trans #vcfg (e:logS_entry vcfg) (s:slot_id vcfg) (sst: slot_state): option slot_state =
  let open Zeta.GenericVerifier in
  match e with
  | AddM (gk,_) s1 s2 ->
    let k = to_base_key gk in
    if s = s1 then
      if Free? sst then Some (Assoc k)
      else None
    else if s = s2 then
      if Assoc? sst then Some sst
      else None
    else Some sst
  | AddB (gk,_) s1  _ _ ->
    let k = to_base_key gk in
    if s = s1 then
      if Free? sst then Some (Assoc k)
      else None
    else Some sst
  | EvictM s1 s2 ->
    if s = s1 then
      if Assoc? sst then Some Free
      else None
    else if s = s2 then
      if Assoc? sst then Some sst
      else None
    else Some sst
  | EvictB s1 _ ->
    if s = s1 then
      if Assoc? sst then Some Free
      else None
    else Some sst
  | EvictBM s1 s2 _ ->
    if s = s1 then
      if Assoc? sst then Some Free
      else None
    else if s = s2 then
      if Assoc? sst then Some sst
      else None
    else Some sst
  | RunApp _ _ ss ->
    if mem s ss then
      if Assoc? sst then Some sst else None
    else Some sst
  | NextEpoch
  | VerifyEpoch -> Some sst

let has_distinct_slots #vcfg (e: logS_entry vcfg): bool =
  let open Zeta.GenericVerifier in
  match e with
  | AddM _ s s' -> s <> s'
  | EvictM s s' -> s <> s'
  | EvictBM s s' _ -> s <> s'
  | _ -> true
/
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

    s: Zeta.Intermediate.VerifierConfig.slot_id vcfg ->
    l: Zeta.Intermediate.Logs.logS vcfg ->
    sst_init: Zeta.Intermediate.SlotKeyRel.slot_state
  -> Prims.Tot (FStar.Pervasives.Native.option Zeta.Intermediate.SlotKeyRel.slot_state)
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.VerifierConfig.slot_id Zeta.Intermediate.Logs.logS Zeta.Intermediate.SlotKeyRel.slot_state Prims.op_Equality Prims.int FStar.Pervasives.Native.Some Prims.bool FStar.Pervasives.Native.uu___is_None FStar.Pervasives.Native.None Prims.op_Negation Zeta.Intermediate.Logs.has_distinct_slots Zeta.Intermediate.Logs.slot_state_trans FStar.Pervasives.Native.__proj__Some__item__v FStar.Pervasives.Native.option Zeta.Intermediate.Logs.slot_state_trans_closure Zeta.Intermediate.Verifier.logS_entry Zeta.SeqAux.telem FStar.Seq.Base.seq Zeta.SeqAux.hprefix Prims.nat FStar.Seq.Base.length
let rec slot_state_trans_closure #vcfg (s: slot_id vcfg) (l: logS vcfg) (sst_init: slot_state)
    : Tot (option slot_state) (decreases (length l)) =
  
let n = length l in
if n = 0
then Some (sst_init)
else
  let l' = hprefix l in
  let e = telem l in
  let osst' = slot_state_trans_closure s l' sst_init in
  if None? osst'
  then None
  else if not (has_distinct_slots e) then None else slot_state_trans e s (Some?.v osst')