val valid_slot (vcfg: verifier_config) (s: nat) : bool
val valid_slot (vcfg: verifier_config) (s: nat) : bool
let valid_slot (vcfg:verifier_config) (s:nat): bool =
  s < store_size vcfg
module Zeta.Intermediate.VerifierConfig

open Zeta.App

noeq
type verifier_config =
  | VConfig: store_size: pos ->
             app: app_params ->
             thread_count: pos ->
             verifier_config

let store_size (vc: verifier_config): nat =
  VConfig?.store_size vc

(* an index in store *)
let slot_id (vcfg:verifier_config) = i:nat{i < store_size vcfg}
/
Zeta.App.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.VerifierConfig.fsti
vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> s: Prims.nat -> Prims.bool
Zeta.Intermediate.VerifierConfig.verifier_config Prims.nat Prims.op_LessThan Zeta.Intermediate.VerifierConfig.store_size Prims.bool
let valid_slot (vcfg: verifier_config) (s: nat) : bool =
  
s < store_size vcfg