• 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
          • Executable
          • Specialized
            • Specialized-features
            • Rv64im
              • Semantics64
              • States64
                • Write64-xreg
                • Write64-xreg-32
                • Write64-mem-ubyte64-lendian
                • Write64-mem-ubyte16-lendian
                • Xregfile64
                • State64
                • Memory64
                • Write64-mem-ubyte32-lendian
                • Write64-pc
                • Read64-mem-ubyte64-lendian
                • Read64-mem-ubyte16-lendian
                • Write64-mem-ubyte8
                • Read64-xreg-unsigned
                • Read64-mem-ubyte32-lendian
                • Read64-mem-ubyte8
                • Read64-xreg-unsigned32
                  • Read64-xreg-signed32
                  • Read64-xreg-signed
                  • Inc64-pc
                  • Read64-pc
                  • Error64p
                  • Error64
                  • *mem64-size*
                • Execution64
              • Rv32im
              • Specialized-states
            • 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
    • States64

    Read64-xreg-unsigned32

    Read an unsigned 32-bit integer from the low bits of an x register.

    Signature
    (read64-xreg-unsigned32 reg stat) → val
    Arguments
    reg — Guard (ubyte5p reg).
    stat — Guard (state64p stat).
    Returns
    val — Type (ubyte32p val).

    The register index consists of 5 bits. We read an unsigned 64-bit integer from the register, and we keep the low 32 bits, stil unsigned.

    Definitions and Theorems

    Function: read64-xreg-unsigned32

    (defun read64-xreg-unsigned32 (reg stat)
      (declare (xargs :guard (and (ubyte5p reg) (state64p stat))))
      (let ((__function__ 'read64-xreg-unsigned32))
        (declare (ignorable __function__))
        (loghead 32 (read64-xreg-unsigned reg stat))))

    Theorem: ubyte32p-of-read64-xreg-unsigned32

    (defthm ubyte32p-of-read64-xreg-unsigned32
      (b* ((val (read64-xreg-unsigned32 reg stat)))
        (ubyte32p val))
      :rule-classes :rewrite)

    Theorem: read64-xreg-unsigned32-of-ubyte5-fix-reg

    (defthm read64-xreg-unsigned32-of-ubyte5-fix-reg
      (equal (read64-xreg-unsigned32 (ubyte5-fix reg)
                                     stat)
             (read64-xreg-unsigned32 reg stat)))

    Theorem: read64-xreg-unsigned32-ubyte5-equiv-congruence-on-reg

    (defthm read64-xreg-unsigned32-ubyte5-equiv-congruence-on-reg
      (implies (ubyte5-equiv reg reg-equiv)
               (equal (read64-xreg-unsigned32 reg stat)
                      (read64-xreg-unsigned32 reg-equiv stat)))
      :rule-classes :congruence)

    Theorem: read64-xreg-unsigned32-of-state64-fix-stat

    (defthm read64-xreg-unsigned32-of-state64-fix-stat
      (equal (read64-xreg-unsigned32 reg (state64-fix stat))
             (read64-xreg-unsigned32 reg stat)))

    Theorem: read64-xreg-unsigned32-state64-equiv-congruence-on-stat

    (defthm read64-xreg-unsigned32-state64-equiv-congruence-on-stat
      (implies (state64-equiv stat stat-equiv)
               (equal (read64-xreg-unsigned32 reg stat)
                      (read64-xreg-unsigned32 reg stat-equiv)))
      :rule-classes :congruence)