		Search-engine friendly clone of the ACL2 documentation.

Linear-memory-in-app-view

Canonical-address-p

Recognizer of a canonical address

Signature
(canonical-address-p lin-addr) → *

In 64-bit mode, a linear address is considered to be in canonical form if address bits 63 through to the most-significant implemented bit by the microarchitecture (represented by the constant *max-linear-address-size* in these books) are set to either all ones or all zeros.

Definitions and Theorems

Function: canonical-address-p$inline

(defun canonical-address-p$inline (lin-addr)
       (declare (xargs :guard t))
       (mbe :logic (signed-byte-p 48 lin-addr)
            :exec (and (integerp lin-addr)
                       (<= -140737488355328 lin-addr)
                       (< lin-addr 140737488355328))))

Theorem: canonical-address-p-and-logext-48

(defthm canonical-address-p-and-logext-48
        (implies (canonical-address-p a)
                 (equal (logext 48 a) a)))

Theorem: canonical-address-p-of-logext-48

(defthm canonical-address-p-of-logext-48
        (canonical-address-p (logext 48 a)))