• 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
              • Semantics64
                • Exec64-bgeu
                • Exec64-bltu
                • Exec64-blt
                • Exec64-bge
                • Exec64-bne
                • Exec64-beq
                • Exec64-jalr
                • Exec64-branch
                • Exec64-jal
                • Exec64-op-imms-32
                • Exec64-op-32
                • Exec64-op
                • Exec64-srlw
                • Exec64-sraw
                • Exec64-op-imm-32
                • Exec64-op-imm
                • Exec64-auipc
                • Exec64-store
                • Exec64-sra
                • Exec64-sltiu
                • Exec64-remw
                • Exec64-remuw
                • Exec64-op-imms
                  • Exec64-load
                  • Exec64-srliw
                  • Exec64-srl
                  • Exec64-sraiw
                  • Exec64-slti
                  • Exec64-sllw
                  • Exec64-remu
                  • Exec64-rem
                  • Exec64-divw
                  • Exec64-divuw
                  • Exec64-addiw
                  • Exec64-xori
                  • Exec64-srli
                  • Exec64-srai
                  • Exec64-ori
                  • Exec64-divu
                  • Exec64-andi
                  • Exec64-addi
                  • Exec64-sltu
                  • Exec64-slt
                  • Exec64-slliw
                  • Exec64-sll
                  • Exec64-mulhsu
                  • Exec64-lwu
                  • Exec64-lhu
                  • Exec64-div
                  • Exec64-xor
                  • Exec64-sw
                  • Exec64-slli
                  • Exec64-sh
                  • Exec64-mulw
                  • Exec64-mulhu
                  • Exec64-mulh
                  • Exec64-lw
                  • Exec64-lh
                  • Exec64-lbu
                  • Exec64-addw
                  • Exec64-subw
                  • Exec64-sub
                  • Exec64-sd
                  • Exec64-sb
                  • Exec64-or
                  • Exec64-ld
                  • Exec64-lb
                  • Exec64-and
                  • Exec64-mul
                  • Exec64-add
                  • Exec64-instr
                  • Eff64-addr
                  • Exec64-lui
                • States64
                • Execution64
              • Rv32im
              • 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
    • Semantics64

    Exec64-op-imms

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

    Signature
    (exec64-op-imms funct rd rs1 imm stat) → new-stat
    Arguments
    funct — Guard (op-imms-funct-p funct).
    rd — Guard (ubyte5p rd).
    rs1 — Guard (ubyte5p rs1).
    imm — Guard (ubyte6p imm).
    stat — Guard (state64p stat).
    Returns
    new-stat — Type (state64p new-stat).

    Definitions and Theorems

    Function: exec64-op-imms

    (defun exec64-op-imms (funct rd rs1 imm stat)
      (declare (xargs :guard (and (op-imms-funct-p funct)
                                  (ubyte5p rd)
                                  (ubyte5p rs1)
                                  (ubyte6p imm)
                                  (state64p stat))))
      (let ((__function__ 'exec64-op-imms))
        (declare (ignorable __function__))
        (op-imms-funct-case funct
                            :slli (exec64-slli rd rs1 imm stat)
                            :srli (exec64-srli rd rs1 imm stat)
                            :srai (exec64-srai rd rs1 imm stat))))

    Theorem: state64p-of-exec64-op-imms

    (defthm state64p-of-exec64-op-imms
      (b* ((new-stat (exec64-op-imms funct rd rs1 imm stat)))
        (state64p new-stat))
      :rule-classes :rewrite)

    Theorem: exec64-op-imms-of-op-imms-funct-fix-funct

    (defthm exec64-op-imms-of-op-imms-funct-fix-funct
      (equal (exec64-op-imms (op-imms-funct-fix funct)
                             rd rs1 imm stat)
             (exec64-op-imms funct rd rs1 imm stat)))

    Theorem: exec64-op-imms-op-imms-funct-equiv-congruence-on-funct

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

    Theorem: exec64-op-imms-of-ubyte5-fix-rd

    (defthm exec64-op-imms-of-ubyte5-fix-rd
      (equal (exec64-op-imms funct (ubyte5-fix rd)
                             rs1 imm stat)
             (exec64-op-imms funct rd rs1 imm stat)))

    Theorem: exec64-op-imms-ubyte5-equiv-congruence-on-rd

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

    Theorem: exec64-op-imms-of-ubyte5-fix-rs1

    (defthm exec64-op-imms-of-ubyte5-fix-rs1
      (equal (exec64-op-imms funct rd (ubyte5-fix rs1)
                             imm stat)
             (exec64-op-imms funct rd rs1 imm stat)))

    Theorem: exec64-op-imms-ubyte5-equiv-congruence-on-rs1

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

    Theorem: exec64-op-imms-of-ubyte6-fix-imm

    (defthm exec64-op-imms-of-ubyte6-fix-imm
      (equal (exec64-op-imms funct rd rs1 (ubyte6-fix imm)
                             stat)
             (exec64-op-imms funct rd rs1 imm stat)))

    Theorem: exec64-op-imms-ubyte6-equiv-congruence-on-imm

    (defthm exec64-op-imms-ubyte6-equiv-congruence-on-imm
      (implies (acl2::ubyte6-equiv imm imm-equiv)
               (equal (exec64-op-imms funct rd rs1 imm stat)
                      (exec64-op-imms funct rd rs1 imm-equiv stat)))
      :rule-classes :congruence)

    Theorem: exec64-op-imms-of-state64-fix-stat

    (defthm exec64-op-imms-of-state64-fix-stat
      (equal (exec64-op-imms funct rd rs1 imm (state64-fix stat))
             (exec64-op-imms funct rd rs1 imm stat)))

    Theorem: exec64-op-imms-state64-equiv-congruence-on-stat

    (defthm exec64-op-imms-state64-equiv-congruence-on-stat
      (implies (state64-equiv stat stat-equiv)
               (equal (exec64-op-imms funct rd rs1 imm stat)
                      (exec64-op-imms funct rd rs1 imm stat-equiv)))
      :rule-classes :congruence)