# Cstate-to-vars

Turn a computation state into a variable table.

- Signature
(cstate-to-vars cstate) → varset

- Arguments
`cstate` — Guard (cstatep cstate).
- Returns
`varset` — Type (identifier-setp varset).

A variable table is the static counterpart of
the local state of a computation state in the dynamic execution.
The variable table consists of the keys of the omap.

We prove a theorem to fold the body of this function
into the function call.
This is the opposite of unfolding the definition.
We use this rule in the main static soundness theorem.
This rule is not very satisfactory;
we will look into avoiding it in some way.

### Definitions and Theorems

**Function: **cstate-to-vars

(defun cstate-to-vars (cstate)
(declare (xargs :guard (cstatep cstate)))
(let ((__function__ 'cstate-to-vars))
(declare (ignorable __function__))
(omap::keys (cstate->local cstate))))

**Theorem: **identifier-setp-of-cstate-to-vars

(defthm identifier-setp-of-cstate-to-vars
(b* ((varset (cstate-to-vars cstate)))
(identifier-setp varset))
:rule-classes :rewrite)

**Theorem: **cstate-to-vars-fold-def

(defthm cstate-to-vars-fold-def
(equal (omap::keys (cstate->local cstate))
(cstate-to-vars cstate)))

**Theorem: **cstate-to-vars-of-cstate-fix-cstate

(defthm cstate-to-vars-of-cstate-fix-cstate
(equal (cstate-to-vars (cstate-fix cstate))
(cstate-to-vars cstate)))

**Theorem: **cstate-to-vars-cstate-equiv-congruence-on-cstate

(defthm cstate-to-vars-cstate-equiv-congruence-on-cstate
(implies (cstate-equiv cstate cstate-equiv)
(equal (cstate-to-vars cstate)
(cstate-to-vars cstate-equiv)))
:rule-classes :congruence)