		Search-engine friendly clone of the ACL2 documentation.

States64

Inc64-pc

Increment the program counter.

Signature
(inc64-pc stat) → new-stat
Arguments: stat — Guard (state64p stat).
Returns: new-stat — Type (state64p 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 encodings in the C extension [ISA:26].

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

Definitions and Theorems

Function: inc64-pc

(defun inc64-pc (stat)
  (declare (xargs :guard (state64p stat)))
  (let ((__function__ 'inc64-pc))
    (declare (ignorable __function__))
    (write64-pc (+ (read64-pc stat) 4)
                stat)))

Theorem: state64p-of-inc64-pc

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

Theorem: inc64-pc-of-state64-fix-stat

(defthm inc64-pc-of-state64-fix-stat
  (equal (inc64-pc (state64-fix stat))
         (inc64-pc stat)))

Theorem: inc64-pc-state64-equiv-congruence-on-stat

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