• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Riscv
        • Semantics
        • Instructions
        • States
        • Decoding
        • Encoding
        • Features
        • Rv32im
        • Rv64im
          • Semantics64
          • States64
            • Write64-xreg
            • Write64-xreg-32
            • Write64-mem-ubyte64-lendian
            • Write64-mem-ubyte16-lendian
            • Xregfile64
              • Xregfile64p
              • Xregfile64-fix
              • State64
              • Memory64
              • Write64-mem-ubyte32-lendian
              • Write64-pc
              • Write64-mem-ubyte8
              • Read64-mem-ubyte64-lendian
              • Read64-mem-ubyte16-lendian
              • Read64-mem-ubyte32-lendian
              • Read64-xreg-unsigned
              • Read64-mem-ubyte8
              • Read64-xreg-unsigned32
              • Read64-xreg-signed32
              • Read64-xreg-signed
              • Inc64-pc
              • Read64-pc
              • Error64p
              • Error64
              • *mem64-size*
          • Execution
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Community
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Xregfile64

    Xregfile64-fix

    Fixer for xregfile64.

    Signature
    (xregfile64-fix x) → *
    Arguments
    x — Guard (xregfile64p x).

    Definitions and Theorems

    Function: xregfile64-fix

    (defun xregfile64-fix (x)
      (declare (xargs :guard (xregfile64p x)))
      (mbe :logic
           (if (xregfile64p x)
               x
             (acl2::ubyte64-list-fix (take 31 x)))
           :exec x))

    Theorem: xregfile64p-of-xregfile64-fix

    (defthm xregfile64p-of-xregfile64-fix
      (xregfile64p (xregfile64-fix x)))

    Theorem: xregfile64-fix-when-xregfile64p

    (defthm xregfile64-fix-when-xregfile64p
      (implies (xregfile64p x)
               (equal (xregfile64-fix x) x)))