val slot_id : vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
let slot_id (vcfg:verifier_config) = i:nat{i < 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
/
Zeta.App.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.VerifierConfig.fsti
vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
Zeta.Intermediate.VerifierConfig.verifier_config Prims.nat Prims.b2t Prims.op_LessThan Zeta.Intermediate.VerifierConfig.store_size
let slot_id (vcfg: verifier_config) =
  
i: nat{i < store_size vcfg}