		Search-engine friendly clone of the ACL2 documentation.

Features

Feat->ialign

The IALIGN parameter [ISA:1.5].

Signature
(feat->ialign feat) → ialign
Arguments: feat — Guard (featp feat).
Returns: ialign — Type (posp ialign).

This is currently always 32, because we do not support the C extension [ISA:27] yet. Once we add support for the C extension, this will be 16 when the C extension is active in the features.

In any case, IALIGN always consists of a whole number of bytes.

Definitions and Theorems

Function: feat->ialign

(defun feat->ialign (feat)
  (declare (xargs :guard (featp feat)))
  (declare (ignore feat))
  (declare
       (xargs :type-prescription (and (posp (feat->ialign feat))
                                      (> (feat->ialign feat) 1))))
  (let ((__function__ 'feat->ialign))
    (declare (ignorable __function__))
    32))

Theorem: posp-of-feat->ialign

(defthm posp-of-feat->ialign
  (b* ((ialign (feat->ialign feat)))
    (posp ialign))
  :rule-classes :rewrite)

Theorem: feat->ialign-is-whole-bytes

(defthm feat->ialign-is-whole-bytes
  (b* ((?ialign (feat->ialign feat)))
    (integerp (/ ialign 8)))
  :rule-classes (:rewrite :type-prescription))

Theorem: feat->ialign-of-feat-fix-feat

(defthm feat->ialign-of-feat-fix-feat
  (equal (feat->ialign (feat-fix feat))
         (feat->ialign feat)))

Theorem: feat->ialign-feat-equiv-congruence-on-feat

(defthm feat->ialign-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (feat->ialign feat)
                  (feat->ialign feat-equiv)))
  :rule-classes :congruence)