• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
          • Register-readers-and-writers
            • Zmms-reads-and-writes
              • Xmms-reads-and-writes
                • !xmmi-size
                  • Xmmi-size
                  • Wx64
                  • Wx32
                  • Wx128
                  • Rx64
                  • Rx32
                  • Rx128
                • !zmmi-size
                • Wz64
                • Wz32
                • Wz128
                • Wz256
                • Vector-access-type-p
                • Rz512
                • Zmmi-size
                • Wz512
                • Rz64
                • Rz32
                • Rz256
                • Rz128
              • Gprs-reads-and-writes
              • Mmx-registers-reads-and-writes
              • Xmms-reads-and-writes
                • !xmmi-size
                  • Xmmi-size
                  • Wx64
                  • Wx32
                  • Wx128
                  • Rx64
                  • Rx32
                  • Rx128
                • Rflags-reads-and-writes
                • Gpr-indices
                • Vex-vvvv-reg-index
                • Msr-reads-and-writes
                • Ctr-reads-and-writes
              • X86-modes
              • Segmentation
              • Other-non-deterministic-computations
              • Environment
              • Paging
            • Implemented-opcodes
            • To-do
            • Proof-utilities
            • Peripherals
            • Model-validation
            • Modelcalls
            • Concrete-simulation-examples
            • Utils
            • Debugging-code-proofs
          • Axe
          • Execloader
        • Math
        • Testing-utilities
      • Xmms-reads-and-writes

      !xmmi-size

      Write val to low nbytes of an XMM register; upper bits of the ZMM register are preserved.

      Signature
      (!xmmi-size nbytes index val x86) → x86
      Returns
      x86 — Type (x86p x86), given (x86p x86).

      Definitions and Theorems

      Function: !xmmi-size$inline

      (defun !xmmi-size$inline (nbytes index val x86)
       (declare (xargs :stobjs (x86)))
       (declare (type (unsigned-byte 5) nbytes)
                (type (unsigned-byte 4) index)
                (type integer val))
       (declare (xargs :guard (and (member nbytes '(4 8 16))
                                   (unsigned-byte-p (ash nbytes 3) val))))
       (case nbytes
         (4 (wx32 index val x86))
         (8 (wx64 index val x86))
         (16 (wx128 index val x86))
         (otherwise x86)))

      Theorem: x86p-of-!xmmi-size

      (defthm x86p-of-!xmmi-size
        (implies (x86p x86)
                 (b* ((x86 (!xmmi-size$inline nbytes index val x86)))
                   (x86p x86)))
        :rule-classes :rewrite)