		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

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)