		Search-engine friendly clone of the ACL2 documentation.

States32

Write32-pc

Write the program counter.

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

The value is any integer, signed or unsigned, which is converted to an unsigned 32-bit integer by keeping its low 32 bits.

The fact that the value to write is any integer is handy for callers, who can just pass the integer (e.g. the exact result of an operation) and let this writer function convert the integer for the register. [ISA:1.4] says that address computations wrap round ignoring overflow, i.e. the last address in the address space is adjacent to address 0.

Definitions and Theorems

Function: write32-pc

(defun write32-pc (pc stat)
  (declare (xargs :guard (and (integerp pc) (state32p stat))))
  (let ((__function__ 'write32-pc))
    (declare (ignorable __function__))
    (change-state32 stat
                    :pc (loghead 32 pc))))

Theorem: state32p-of-write32-pc

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

Theorem: write32-pc-of-ifix-pc

(defthm write32-pc-of-ifix-pc
  (equal (write32-pc (ifix pc) stat)
         (write32-pc pc stat)))

Theorem: write32-pc-int-equiv-congruence-on-pc

(defthm write32-pc-int-equiv-congruence-on-pc
  (implies (acl2::int-equiv pc pc-equiv)
           (equal (write32-pc pc stat)
                  (write32-pc pc-equiv stat)))
  :rule-classes :congruence)

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

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

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

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