• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Riscv
          • Specification
            • Semantics
            • Features
              • Feat-base
              • Feat-endian
              • Feat
              • Feat->xlen
              • Feat->ialign
                • Feat->xnum
                • Feat-64p
                • Feat-32p
                • Feat-little-endianp
                • Feat-big-endianp
                • Feat->ilen
                • Feat-embedp
                • Feat-mp
              • Instructions
              • Encoding
              • States
              • Reads-over-writes
              • Semantics-equivalences
              • Decoding
              • Execution
            • Executable
            • Specialized
            • Optimized
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • 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)