|
|
|---|
|
|
|
|---|
Increment the program counter.
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:27].
We read the program counter, we add 4, and we write the result. Recall that write32-pc wraps around if needed [ISA:1.4].
Function:
(defun inc32-pc (stat) (declare (xargs :guard (stat32p stat))) (write32-pc (+ (read32-pc stat) 4) stat))
Theorem:
(defthm stat32p-of-inc32-pc (b* ((new-stat (inc32-pc stat))) (stat32p new-stat)) :rule-classes :rewrite)
Theorem:
(defthm inc32-pc-of-stat32-fix-stat (equal (inc32-pc (stat32-fix stat)) (inc32-pc stat)))
Theorem:
(defthm inc32-pc-stat32-equiv-congruence-on-stat (implies (stat32-equiv stat stat-equiv) (equal (inc32-pc stat) (inc32-pc stat-equiv))) :rule-classes :congruence)