		Search-engine friendly clone of the ACL2 documentation.

Execution64

Step64

Single-step execution.

Signature
(step64 stat) → new-stat
Arguments: stat — Guard (state64p stat).
Returns: new-stat — Type (state64p 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: step64

(defun step64 (stat)
  (declare (xargs :guard (state64p stat)))
  (let ((__function__ 'step64))
    (declare (ignorable __function__))
    (b* (((when (error64p stat))
          (state64-fix stat))
         (pc (read64-pc stat))
         (enc (read64-mem-ubyte32-lendian pc stat))
         (instr? (decode enc t))
         ((unless instr?) (error64 stat)))
      (exec64-instr instr? pc stat))))

Theorem: state64p-of-step64

(defthm state64p-of-step64
  (b* ((new-stat (step64 stat)))
    (state64p new-stat))
  :rule-classes :rewrite)

Theorem: step64-of-state64-fix-stat

(defthm step64-of-state64-fix-stat
  (equal (step64 (state64-fix stat))
         (step64 stat)))

Theorem: step64-state64-equiv-congruence-on-stat

(defthm step64-state64-equiv-congruence-on-stat
  (implies (state64-equiv stat stat-equiv)
           (equal (step64 stat)
                  (step64 stat-equiv)))
  :rule-classes :congruence)