		Search-engine friendly clone of the ACL2 documentation.

States32

Inc32-pc

Increment the program counter.

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

The increment is by 4, which is motivated by the fact that, at least in the normal encoding, instructions take 32 bits each. We may generalize this function, or add an alternative one, if and when we extend our model to support compressed encodingsin the C extension [ISA:26].

We read the program counter, we add 4, and we write the result. Recall that write32-pc wraps around if needed [ISA:1.4].

Definitions and Theorems

Function: inc32-pc

(defun inc32-pc (stat)
  (declare (xargs :guard (state32p stat)))
  (let ((__function__ 'inc32-pc))
    (declare (ignorable __function__))
    (write32-pc (+ (read32-pc stat) 4)
                stat)))

Theorem: state32p-of-inc32-pc

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

Theorem: inc32-pc-of-state32-fix-stat

(defthm inc32-pc-of-state32-fix-stat
  (equal (inc32-pc (state32-fix stat))
         (inc32-pc stat)))

Theorem: inc32-pc-state32-equiv-congruence-on-stat

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