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

Div-spec

Specification for the DIV (unsigned divide) instruction

Signature

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

Definitions and Theorems

Function: div-spec$inline

(defun div-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 (div-spec-8 dst src))
    (2 (div-spec-16 dst src))
    (4 (div-spec-32 dst src))
    (8 (div-spec-64 dst src))
    (otherwise (mv nil 0 0))))

Theorem: mv-nth-1-div-spec

(defthm mv-nth-1-div-spec
 (implies (and (member size '(1 2 4 8))
               (not (mv-nth 0 (div-spec size dst src))))
          (unsigned-byte-p (ash size 3)
                           (mv-nth 1 (div-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 (div-spec size dst src))))
               (natp (mv-nth 1 (div-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 (div-spec size dst src))))
            (and (<= 0 (mv-nth 1 (div-spec size dst src)))
                 (< (mv-nth 1 (div-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-div-spec

(defthm mv-nth-2-div-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 (div-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 (div-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 (div-spec size dst src)))
                 (< (mv-nth 2 (div-spec size dst src))
                    (expt 2 (ash size 3)))))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Subtopics

Div-spec-8

Div-spec-64

Div-spec-32

Div-spec-16