		Search-engine friendly clone of the ACL2 documentation.

Execution32

Step32

Single-step execution.

Signature
(step32 stat) → new-stat
Arguments: stat — Guard (state32p stat).
Returns: new-stat — Type (state32p new-stat).

We make no change if the error flag is set. Otherwise, we read the program counter, we read the 32-bit of the instruction from there (which is always little endian [ISA:1.5.1]), we decode it, and, if we obtain an instruction, we run the semantic function of the instruction; if decoding fails, we set the error flag instead.

Definitions and Theorems

Function: step32

(defun step32 (stat)
  (declare (xargs :guard (state32p stat)))
  (let ((__function__ 'step32))
    (declare (ignorable __function__))
    (b* (((when (error32p stat))
          (state32-fix stat))
         (pc (read32-pc stat))
         (enc (read32-mem-ubyte32-lendian pc stat))
         (instr? (decode enc t))
         ((unless instr?) (error32 stat)))
      (exec32-instr instr? pc stat))))

Theorem: state32p-of-step32

(defthm state32p-of-step32
  (b* ((new-stat (step32 stat)))
    (state32p new-stat))
  :rule-classes :rewrite)

Theorem: step32-of-state32-fix-stat

(defthm step32-of-state32-fix-stat
  (equal (step32 (state32-fix stat))
         (step32 stat)))

Theorem: step32-state32-equiv-congruence-on-stat

(defthm step32-state32-equiv-congruence-on-stat
  (implies (state32-equiv stat stat-equiv)
           (equal (step32 stat)
                  (step32 stat-equiv)))
  :rule-classes :congruence)