• 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
            • Semantics
              • Exec-bltu
              • Exec-bgeu
              • Exec-bge
              • Exec-blt
              • Exec-bne
              • Exec-beq
              • Exec-jalr
              • Exec-jal
              • Exec-sra
              • Exec-op
              • Exec-srl
              • Exec-op-imms-32
              • Exec-op-32
              • Exec-sll
              • Exec-branch
              • Exec-srlw
              • Exec-sraw
              • Exec-remuw
              • Exec-op-imms64
              • Exec-op-imms32
              • Exec-op-imm-32
              • Exec-srliw
              • Exec-sraiw
              • Exec-sltiu
              • Exec-remw
              • Exec-op-imm
                • Exec-load
                • Exec-divuw
                • Exec-store
                • Exec-srli64
                • Exec-srli32
                • Exec-srai64
                • Exec-srai32
                • Exec-sllw
                • Exec-remu
                • Exec-divw
                • Exec-addiw
                • Exec-xori
                • Exec-slti
                • Exec-slliw
                • Exec-rem
                • Exec-ori
                • Exec-mulhsu
                • Exec-divu
                • Exec-auipc
                • Exec-andi
                • Exec-sw
                • Exec-sltu
                • Exec-slt
                • Exec-slli64
                • Exec-slli32
                • Exec-mulhu
                • Exec-div
                • Exec-addw
                • Exec-addi
                • Exec-xor
                • Exec-mulw
                • Exec-mulh
                • Exec-lwu
                • Exec-and
                • Exec-subw
                • Exec-sub
                • Exec-or
                • Exec-lhu
                • Exec-lbu
                • Exec-sd
                • Exec-mul
                • Exec-lh
                • Exec-ld
                • Exec-lb
                • Exec-add
                • Exec-sh
                • Exec-sb
                • Exec-lw
                • Exec-lui
                • Eff-addr
                • Exec-instr
              • Features
              • Instructions
              • Encoding
              • States
              • Reads-over-writes
              • Semantics-equivalences
              • Decoding
              • Execution
            • Executable
            • Specialized
            • 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
    • Semantics

    Exec-op-imm

    Semantics of the non-shift instructions with the OP-IMM opcode [ISA:2.4.1].

    Signature
    (exec-op-imm funct rd rs1 imm stat feat) → new-stat
    Arguments
    funct — Guard (op-imm-funct-p funct).
    rd — Guard (ubyte5p rd).
    rs1 — Guard (ubyte5p rs1).
    imm — Guard (ubyte12p imm).
    stat — Guard (statp stat).
    feat — Guard (featp feat).
    Returns
    new-stat — Type (statp new-stat).

    Definitions and Theorems

    Function: exec-op-imm

    (defun exec-op-imm (funct rd rs1 imm stat feat)
      (declare (xargs :guard (and (op-imm-funct-p funct)
                                  (ubyte5p rd)
                                  (ubyte5p rs1)
                                  (ubyte12p imm)
                                  (statp stat)
                                  (featp feat))))
      (declare (xargs :guard (and (stat-validp stat feat)
                                  (< (lnfix rd) (feat->xnum feat))
                                  (< (lnfix rs1) (feat->xnum feat)))))
      (let ((__function__ 'exec-op-imm))
        (declare (ignorable __function__))
        (op-imm-funct-case funct
                           :addi (exec-addi rd rs1 imm stat feat)
                           :slti (exec-slti rd rs1 imm stat feat)
                           :sltiu (exec-sltiu rd rs1 imm stat feat)
                           :andi (exec-andi rd rs1 imm stat feat)
                           :ori (exec-ori rd rs1 imm stat feat)
                           :xori (exec-xori rd rs1 imm stat feat))))

    Theorem: statp-of-exec-op-imm

    (defthm statp-of-exec-op-imm
      (b* ((new-stat (exec-op-imm funct rd rs1 imm stat feat)))
        (statp new-stat))
      :rule-classes :rewrite)

    Theorem: stat-validp-of-exec-op-imm

    (defthm stat-validp-of-exec-op-imm
     (implies (and (stat-validp stat feat)
                   (< (lnfix rd) (feat->xnum feat)))
              (b* ((?new-stat (exec-op-imm funct rd rs1 imm stat feat)))
                (stat-validp new-stat feat))))

    Theorem: exec-op-imm-of-op-imm-funct-fix-funct

    (defthm exec-op-imm-of-op-imm-funct-fix-funct
      (equal (exec-op-imm (op-imm-funct-fix funct)
                          rd rs1 imm stat feat)
             (exec-op-imm funct rd rs1 imm stat feat)))

    Theorem: exec-op-imm-op-imm-funct-equiv-congruence-on-funct

    (defthm exec-op-imm-op-imm-funct-equiv-congruence-on-funct
      (implies (op-imm-funct-equiv funct funct-equiv)
               (equal (exec-op-imm funct rd rs1 imm stat feat)
                      (exec-op-imm funct-equiv rd rs1 imm stat feat)))
      :rule-classes :congruence)

    Theorem: exec-op-imm-of-ubyte5-fix-rd

    (defthm exec-op-imm-of-ubyte5-fix-rd
      (equal (exec-op-imm funct (ubyte5-fix rd)
                          rs1 imm stat feat)
             (exec-op-imm funct rd rs1 imm stat feat)))

    Theorem: exec-op-imm-ubyte5-equiv-congruence-on-rd

    (defthm exec-op-imm-ubyte5-equiv-congruence-on-rd
      (implies (ubyte5-equiv rd rd-equiv)
               (equal (exec-op-imm funct rd rs1 imm stat feat)
                      (exec-op-imm funct rd-equiv rs1 imm stat feat)))
      :rule-classes :congruence)

    Theorem: exec-op-imm-of-ubyte5-fix-rs1

    (defthm exec-op-imm-of-ubyte5-fix-rs1
      (equal (exec-op-imm funct rd (ubyte5-fix rs1)
                          imm stat feat)
             (exec-op-imm funct rd rs1 imm stat feat)))

    Theorem: exec-op-imm-ubyte5-equiv-congruence-on-rs1

    (defthm exec-op-imm-ubyte5-equiv-congruence-on-rs1
      (implies (ubyte5-equiv rs1 rs1-equiv)
               (equal (exec-op-imm funct rd rs1 imm stat feat)
                      (exec-op-imm funct rd rs1-equiv imm stat feat)))
      :rule-classes :congruence)

    Theorem: exec-op-imm-of-ubyte12-fix-imm

    (defthm exec-op-imm-of-ubyte12-fix-imm
      (equal (exec-op-imm funct rd rs1 (ubyte12-fix imm)
                          stat feat)
             (exec-op-imm funct rd rs1 imm stat feat)))

    Theorem: exec-op-imm-ubyte12-equiv-congruence-on-imm

    (defthm exec-op-imm-ubyte12-equiv-congruence-on-imm
      (implies (acl2::ubyte12-equiv imm imm-equiv)
               (equal (exec-op-imm funct rd rs1 imm stat feat)
                      (exec-op-imm funct rd rs1 imm-equiv stat feat)))
      :rule-classes :congruence)

    Theorem: exec-op-imm-of-stat-fix-stat

    (defthm exec-op-imm-of-stat-fix-stat
      (equal (exec-op-imm funct rd rs1 imm (stat-fix stat)
                          feat)
             (exec-op-imm funct rd rs1 imm stat feat)))

    Theorem: exec-op-imm-stat-equiv-congruence-on-stat

    (defthm exec-op-imm-stat-equiv-congruence-on-stat
      (implies (stat-equiv stat stat-equiv)
               (equal (exec-op-imm funct rd rs1 imm stat feat)
                      (exec-op-imm funct rd rs1 imm stat-equiv feat)))
      :rule-classes :congruence)

    Theorem: exec-op-imm-of-feat-fix-feat

    (defthm exec-op-imm-of-feat-fix-feat
      (equal (exec-op-imm funct rd rs1 imm stat (feat-fix feat))
             (exec-op-imm funct rd rs1 imm stat feat)))

    Theorem: exec-op-imm-feat-equiv-congruence-on-feat

    (defthm exec-op-imm-feat-equiv-congruence-on-feat
      (implies (feat-equiv feat feat-equiv)
               (equal (exec-op-imm funct rd rs1 imm stat feat)
                      (exec-op-imm funct rd rs1 imm stat feat-equiv)))
      :rule-classes :congruence)