val all_slots_assoc : ssm: Zeta.Intermediate.SlotKeyRel.slot_state_map vcfg ->
    ss: FStar.Seq.Base.seq (Zeta.Intermediate.VerifierConfig.slot_id vcfg)
  -> Prims.logical
let all_slots_assoc (#vcfg:_) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg))
  = forall i. (is_assoc ssm (index ss i))
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)
/
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 ->
    ss: FStar.Seq.Base.seq (Zeta.Intermediate.VerifierConfig.slot_id vcfg)
  -> Prims.logical
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.SlotKeyRel.slot_state_map FStar.Seq.Base.seq Zeta.Intermediate.VerifierConfig.slot_id Prims.l_Forall Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Zeta.Intermediate.SlotKeyRel.is_assoc FStar.Seq.Base.index Prims.logical
let all_slots_assoc (#vcfg: _) (ssm: slot_state_map vcfg) (ss: seq (slot_id vcfg)) =
  
forall i. (is_assoc ssm (index ss i))