• 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
            • Idiv-spec
              • Idiv-spec-64
              • Idiv-spec-32
              • Idiv-spec-8
              • Idiv-spec-16
            • 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

Idiv-spec

Specification for the IDIV (unsigned idivide) instruction

Signature

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

Definitions and Theorems

Function: idiv-spec$inline

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

Theorem: mv-nth-1-idiv-spec

(defthm mv-nth-1-idiv-spec
 (implies (and (member size '(1 2 4 8))
               (not (mv-nth 0 (idiv-spec size dst src))))
          (unsigned-byte-p (ash size 3)
                           (mv-nth 1 (idiv-spec size dst src))))
 :rule-classes
 (:rewrite
  (:type-prescription
      :corollary
      (implies (and (syntaxp (quotep size))
                    (force (member size '(1 2 4 8)))
                    (not (mv-nth 0 (idiv-spec size dst src))))
               (natp (mv-nth 1 (idiv-spec size dst src))))
      :hints
      (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies (and (member size '(1 2 4 8))
                 (not (mv-nth 0 (idiv-spec size dst src))))
            (and (<= 0 (mv-nth 1 (idiv-spec size dst src)))
                 (< (mv-nth 1 (idiv-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-idiv-spec

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

Subtopics

Idiv-spec-64

Idiv-spec-32

Idiv-spec-8

Idiv-spec-16