Turn a computation state into a variable table.
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.
(defun cstate-to-vars (cstate) (declare (xargs :guard (cstatep cstate))) (let ((__function__ 'cstate-to-vars)) (declare (ignorable __function__)) (omap::keys (cstate->local cstate))))
(defthm identifier-setp-of-cstate-to-vars (b* ((varset (cstate-to-vars cstate))) (identifier-setp varset)) :rule-classes :rewrite)
(defthm cstate-to-vars-fold-def (equal (omap::keys (cstate->local cstate)) (cstate-to-vars cstate)))
(defthm cstate-to-vars-of-cstate-fix-cstate (equal (cstate-to-vars (cstate-fix cstate)) (cstate-to-vars 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)