val is_assoc (#vcfg: _) (ssm: slot_state_map vcfg) (s: slot_id vcfg) : bool
val is_assoc (#vcfg: _) (ssm: slot_state_map vcfg) (s: slot_id vcfg) : bool
let is_assoc (#vcfg:_) (ssm:slot_state_map vcfg) (s:slot_id vcfg): bool =
  not (is_free ssm s)
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

(* mapping from a slot to its state *)
let slot_state_map vcfg = slot_id vcfg -> slot_state 

let is_free (#vcfg:_) (ssm:slot_state_map vcfg) (s: slot_id vcfg): bool = 
  ssm s = Free
/
Zeta.Key.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.SlotKeyRel.fsti

    ssm: Zeta.Intermediate.SlotKeyRel.slot_state_map vcfg ->
    s: Zeta.Intermediate.VerifierConfig.slot_id vcfg
  -> Prims.bool
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.SlotKeyRel.slot_state_map Zeta.Intermediate.VerifierConfig.slot_id Prims.op_Negation Zeta.Intermediate.SlotKeyRel.is_free Prims.bool
let is_assoc (#vcfg: _) (ssm: slot_state_map vcfg) (s: slot_id vcfg) : bool =
  
not (is_free ssm s)