• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Riscv
          • Specification
          • Executable
          • Specialized
            • Specialized-features
            • Rv64im
            • Rv32im
              • Semantics32
                • Exec32-bgeu
                • Exec32-bltu
                • Exec32-blt
                • Exec32-bge
                • Exec32-bne
                • Exec32-beq
                • Exec32-jalr
                • Exec32-branch
                • Exec32-jal
                • Exec32-op
                  • Exec32-store
                  • Exec32-op-imm
                  • Exec32-load
                  • Exec32-sra
                  • Exec32-sltiu
                  • Exec32-op-imms
                  • Exec32-srl
                  • Exec32-slti
                  • Exec32-remu
                  • Exec32-rem
                  • Exec32-auipc
                  • Exec32-xori
                  • Exec32-srli
                  • Exec32-srai
                  • Exec32-ori
                  • Exec32-divu
                  • Exec32-andi
                  • Exec32-addi
                  • Exec32-sltu
                  • Exec32-slt
                  • Exec32-sll
                  • Exec32-mulhsu
                  • Exec32-lhu
                  • Exec32-div
                  • Exec32-xor
                  • Exec32-slli
                  • Exec32-sh
                  • Exec32-mulhu
                  • Exec32-mulh
                  • Exec32-lh
                  • Exec32-lbu
                  • Exec32-sw
                  • Exec32-sub
                  • Exec32-sb
                  • Exec32-or
                  • Exec32-lw
                  • Exec32-lb
                  • Exec32-and
                  • Exec32-mul
                  • Exec32-add
                  • Exec32-instr
                  • Eff32-addr
                  • Exec32-lui
                • States32
                • Execution32
              • Specialized-states
            • Optimized
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Semantics32

    Exec32-op

    Semantics of the instructions with the OP opcode [ISA:2.4.2] [ISA:12.1] [ISA:12.2].

    Signature
    (exec32-op funct rd rs1 rs2 stat) → new-stat
    Arguments
    funct — Guard (op-funct-p funct).
    rd — Guard (ubyte5p rd).
    rs1 — Guard (ubyte5p rs1).
    rs2 — Guard (ubyte5p rs2).
    stat — Guard (stat32ip stat).
    Returns
    new-stat — Type (stat32ip new-stat).

    Definitions and Theorems

    Function: exec32-op

    (defun exec32-op (funct rd rs1 rs2 stat)
      (declare (xargs :guard (and (op-funct-p funct)
                                  (ubyte5p rd)
                                  (ubyte5p rs1)
                                  (ubyte5p rs2)
                                  (stat32ip stat))))
      (let ((__function__ 'exec32-op))
        (declare (ignorable __function__))
        (op-funct-case funct
                       :add (exec32-add rd rs1 rs2 stat)
                       :sub (exec32-sub rd rs1 rs2 stat)
                       :slt (exec32-slt rd rs1 rs2 stat)
                       :sltu (exec32-sltu rd rs1 rs2 stat)
                       :and (exec32-and rd rs1 rs2 stat)
                       :or (exec32-or rd rs1 rs2 stat)
                       :xor (exec32-xor rd rs1 rs2 stat)
                       :sll (exec32-sll rd rs1 rs2 stat)
                       :srl (exec32-srl rd rs1 rs2 stat)
                       :sra (exec32-sra rd rs1 rs2 stat)
                       :mul (exec32-mul rd rs1 rs2 stat)
                       :mulh (exec32-mulh rd rs1 rs2 stat)
                       :mulhu (exec32-mulhu rd rs1 rs2 stat)
                       :mulhsu (exec32-mulhsu rd rs1 rs2 stat)
                       :div (exec32-div rd rs1 rs2 stat)
                       :divu (exec32-divu rd rs1 rs2 stat)
                       :rem (exec32-rem rd rs1 rs2 stat)
                       :remu (exec32-remu rd rs1 rs2 stat))))

    Theorem: stat32ip-of-exec32-op

    (defthm stat32ip-of-exec32-op
      (b* ((new-stat (exec32-op funct rd rs1 rs2 stat)))
        (stat32ip new-stat))
      :rule-classes :rewrite)

    Theorem: exec32-op-of-op-funct-fix-funct

    (defthm exec32-op-of-op-funct-fix-funct
      (equal (exec32-op (op-funct-fix funct)
                        rd rs1 rs2 stat)
             (exec32-op funct rd rs1 rs2 stat)))

    Theorem: exec32-op-op-funct-equiv-congruence-on-funct

    (defthm exec32-op-op-funct-equiv-congruence-on-funct
      (implies (op-funct-equiv funct funct-equiv)
               (equal (exec32-op funct rd rs1 rs2 stat)
                      (exec32-op funct-equiv rd rs1 rs2 stat)))
      :rule-classes :congruence)

    Theorem: exec32-op-of-ubyte5-fix-rd

    (defthm exec32-op-of-ubyte5-fix-rd
      (equal (exec32-op funct (ubyte5-fix rd)
                        rs1 rs2 stat)
             (exec32-op funct rd rs1 rs2 stat)))

    Theorem: exec32-op-ubyte5-equiv-congruence-on-rd

    (defthm exec32-op-ubyte5-equiv-congruence-on-rd
      (implies (ubyte5-equiv rd rd-equiv)
               (equal (exec32-op funct rd rs1 rs2 stat)
                      (exec32-op funct rd-equiv rs1 rs2 stat)))
      :rule-classes :congruence)

    Theorem: exec32-op-of-ubyte5-fix-rs1

    (defthm exec32-op-of-ubyte5-fix-rs1
      (equal (exec32-op funct rd (ubyte5-fix rs1)
                        rs2 stat)
             (exec32-op funct rd rs1 rs2 stat)))

    Theorem: exec32-op-ubyte5-equiv-congruence-on-rs1

    (defthm exec32-op-ubyte5-equiv-congruence-on-rs1
      (implies (ubyte5-equiv rs1 rs1-equiv)
               (equal (exec32-op funct rd rs1 rs2 stat)
                      (exec32-op funct rd rs1-equiv rs2 stat)))
      :rule-classes :congruence)

    Theorem: exec32-op-of-ubyte5-fix-rs2

    (defthm exec32-op-of-ubyte5-fix-rs2
      (equal (exec32-op funct rd rs1 (ubyte5-fix rs2)
                        stat)
             (exec32-op funct rd rs1 rs2 stat)))

    Theorem: exec32-op-ubyte5-equiv-congruence-on-rs2

    (defthm exec32-op-ubyte5-equiv-congruence-on-rs2
      (implies (ubyte5-equiv rs2 rs2-equiv)
               (equal (exec32-op funct rd rs1 rs2 stat)
                      (exec32-op funct rd rs1 rs2-equiv stat)))
      :rule-classes :congruence)

    Theorem: exec32-op-of-stat32i-fix-stat

    (defthm exec32-op-of-stat32i-fix-stat
      (equal (exec32-op funct rd rs1 rs2 (stat32i-fix stat))
             (exec32-op funct rd rs1 rs2 stat)))

    Theorem: exec32-op-stat32i-equiv-congruence-on-stat

    (defthm exec32-op-stat32i-equiv-congruence-on-stat
      (implies (stat32i-equiv stat stat-equiv)
               (equal (exec32-op funct rd rs1 rs2 stat)
                      (exec32-op funct rd rs1 rs2 stat-equiv)))
      :rule-classes :congruence)