• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Sdm-instruction-set-summary
      • Tlb
      • Booting-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
          • Two-byte-opcodes
          • One-byte-opcodes
          • Fp-opcodes
          • Instruction-semantic-functions
            • Sar-spec
            • Shr-spec
            • Sal/shl-spec
            • Rol-spec
            • Ror-spec
            • Rcl-spec
            • Rcr-spec
            • Simd-sub-spec
            • Simd-add-spec
            • Imul-spec
            • Mul-spec
              • Mul-spec-64
              • Mul-spec-8
              • Mul-spec-32
              • Mul-spec-16
            • Idiv-spec
            • Div-spec
            • Shrd-spec
            • Shld-spec
            • Gpr-arith/logic-spec
            • Shrx-spec
            • Shlx-spec
            • Sarx-spec
            • Floating-point-specifications
          • X86-illegal-instruction
          • Implemented-opcodes
          • Opcode-maps
          • X86-general-protection
          • X86-device-not-available
          • X86-step-unimplemented
          • Privileged-opcodes
          • Three-byte-opcodes
        • Register-readers-and-writers
        • 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

• Instruction-semantic-functions

Mul-spec

Specification for the MUL (unsigned multiply) instruction

Signature

(mul-spec size dst src) → (mv * * *)

Definitions and Theorems

Function: mul-spec$inline

(defun mul-spec$inline (size dst src)
  (declare (type (member 1 2 4 8) size))
  (declare (xargs :guard
                  (case size
                    (1 (and (n08p src) (n08p dst)))
                    (2 (and (n16p src) (n16p dst)))
                    (4 (and (n32p src) (n32p dst)))
                    (8 (and (n64p src) (n64p dst)))
                    (otherwise nil))))
  (case size
    (1 (mul-spec-8 dst src))
    (2 (mul-spec-16 dst src))
    (4 (mul-spec-32 dst src))
    (8 (mul-spec-64 dst src))
    (otherwise (mv 0 0 0))))

Theorem: mv-nth-0-mul-spec

(defthm mv-nth-0-mul-spec
 (implies (member size '(1 2 4 8))
          (unsigned-byte-p (ash size 3)
                           (mv-nth 0 (mul-spec size dst src))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (member size '(1 2 4 8))
                          (natp (mv-nth 0 (mul-spec size dst src))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies (member size '(1 2 4 8))
            (and (<= 0 (mv-nth 0 (mul-spec size dst src)))
                 (< (mv-nth 0 (mul-spec size dst src))
                    (expt 2 (ash size 3)))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: mv-nth-1-mul-spec

(defthm mv-nth-1-mul-spec
 (implies (member size '(1 2 4 8))
          (unsigned-byte-p (ash size 3)
                           (mv-nth 1 (mul-spec size dst src))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (member size '(1 2 4 8))
                          (natp (mv-nth 1 (mul-spec size dst src))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies (member size '(1 2 4 8))
            (and (<= 0 (mv-nth 1 (mul-spec size dst src)))
                 (< (mv-nth 1 (mul-spec size dst src))
                    (expt 2 (ash size 3)))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: mv-nth-2-mul-spec

(defthm mv-nth-2-mul-spec
 (implies (member size '(1 2 4 8))
          (unsigned-byte-p (* 2 (ash size 3))
                           (mv-nth 2 (mul-spec size dst src))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary (implies (member size '(1 2 4 8))
                          (natp (mv-nth 2 (mul-spec size dst src))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies (member size '(1 2 4 8))
            (and (<= 0 (mv-nth 2 (mul-spec size dst src)))
                 (< (mv-nth 2 (mul-spec size dst src))
                    (expt 2 (* 2 (ash size 3))))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Subtopics

Mul-spec-64

Mul-spec-8

Mul-spec-32

Mul-spec-16