		Search-engine friendly clone of the ACL2 documentation.

Execution-executable

Stepx

Executable single-step execution function.

This is obtained from step via apt::simplify, passing decode-is-decodex to propagate it. The result is the same as step, but with a call of decodex instead of decode. The generated theorem that unconditionally rewrites step to stepx is step-to-stepx.

We manually propagate the fixing and state validity preservation theorems that accompany step to stepx.

Definitions and Theorems

Function: stepx

(defun stepx (stat feat)
  (declare (xargs :guard (and (statp stat)
                              (featp feat)
                              (stat-validp stat feat))))
  (b* (((when (errorp stat feat))
        (stat-fix stat))
       (pc (read-pc stat feat))
       (enc? (read-instruction pc stat feat))
       ((unless enc?) (error stat feat))
       (instr? (decodex enc? feat))
       ((unless instr?) (error stat feat)))
    (exec-instr instr? pc stat feat)))

Theorem: step-is-stepx

(defthm step-is-stepx
  (equal (step stat feat)
         (stepx stat feat)))

Theorem: stepx-of-stat-fix-stat

(defthm stepx-of-stat-fix-stat
  (equal (stepx (stat-fix stat) feat)
         (stepx stat feat)))

Theorem: stepx-stat-equiv-congruence-on-stat

(defthm stepx-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (stepx stat feat)
                  (stepx stat-equiv feat)))
  :rule-classes :congruence)

Theorem: stepx-of-feat-fix-feat

(defthm stepx-of-feat-fix-feat
  (equal (stepx stat (feat-fix feat))
         (stepx stat feat)))

Theorem: stepx-feat-equiv-congruence-on-feat

(defthm stepx-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (stepx stat feat)
                  (stepx stat feat-equiv)))
  :rule-classes :congruence)

Theorem: stat-validp-of-stepx

(defthm stat-validp-of-stepx
  (implies (stat-validp stat feat)
           (stat-validp (stepx stat feat) feat)))