		Search-engine friendly clone of the ACL2 documentation.

States64

Write64-pc

Write the program counter.

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

The value is any integer, signed or unsigned, which is converted to an unsigned 64-bit integer by keeping its low 64 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: write64-pc

(defun write64-pc (pc stat)
  (declare (xargs :guard (and (integerp pc) (state64p stat))))
  (let ((__function__ 'write64-pc))
    (declare (ignorable __function__))
    (change-state64 stat
                    :pc (loghead 64 pc))))

Theorem: state64p-of-write64-pc

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

Theorem: write64-pc-of-ifix-pc

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

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

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

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

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

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

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