val is_assoc_with (#vcfg: _) (ssm: slot_state_map vcfg) (s: slot_id vcfg) (k: base_key) : bool
val is_assoc_with (#vcfg: _) (ssm: slot_state_map vcfg) (s: slot_id vcfg) (k: base_key) : bool
let is_assoc_with #vcfg (ssm:slot_state_map vcfg) (s:slot_id vcfg) (k:base_key): bool =
  is_assoc ssm s && assoc_key ssm s = k
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

let is_assoc (#vcfg:_) (ssm:slot_state_map vcfg) (s:slot_id vcfg): bool =
  not (is_free ssm s)

let assoc_key (#vcfg:_) (ssm:slot_state_map vcfg) (s:slot_id vcfg{is_assoc ssm s}): base_key =
  Assoc?.k (ssm s)
/
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 ->
    k: Zeta.Key.base_key
  -> Prims.bool
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.SlotKeyRel.slot_state_map Zeta.Intermediate.VerifierConfig.slot_id Zeta.Key.base_key Prims.op_AmpAmp Zeta.Intermediate.SlotKeyRel.is_assoc Prims.op_Equality Zeta.Intermediate.SlotKeyRel.assoc_key Prims.bool
let is_assoc_with #vcfg (ssm: slot_state_map vcfg) (s: slot_id vcfg) (k: base_key) : bool =
  
is_assoc ssm s && assoc_key ssm s = k