val slot_state_map : vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
let slot_state_map vcfg = slot_id vcfg -> slot_state
module Zeta.Intermediate.SlotKeyRel

open Zeta.Key
open Zeta.Intermediate.VerifierConfig

(**
 * The definitions in this file capture the relationship between slots and keys.
 * A slot is a smaller domain of values that are temporarily associated with keys.
 *)

type slot_state = 
  | Free: slot_state 
  | Assoc: k:base_key -> slot_state
/
Zeta.Key.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.SlotKeyRel.fsti
vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.VerifierConfig.slot_id Zeta.Intermediate.SlotKeyRel.slot_state
let slot_state_map vcfg =
  
slot_id vcfg -> slot_state