• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Pfcs
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Riscv
      • Specification
        • Semantics
          • Exec-bltu
          • Exec-blt
          • Exec-bgeu
          • Exec-bge
          • Exec-jalr
          • Exec-bne
          • Exec-beq
          • Exec-sra
          • Exec-op
          • Exec-srl
          • Exec-op-imms-32
          • Exec-op-32
          • Exec-srlw
          • Exec-sraw
          • Exec-sll
          • Exec-remuw
          • Exec-op-imms64
          • Exec-op-imms32
          • Exec-op-imm-32
          • Exec-branch
          • Exec-addi
          • Exec-srliw
          • Exec-sraiw
          • Exec-sltiu
          • Exec-remw
          • Exec-op-imm
          • Exec-load
          • Exec-jal
          • Exec-divuw
          • Exec-sub
          • 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-andi
          • Exec-add
          • Exec-sw
          • Exec-sltu
          • Exec-slt
          • Exec-slli64
          • Exec-slli32
          • Exec-mulhu
          • Exec-div
          • Exec-auipc
          • Exec-addw
          • Exec-mulw
          • Exec-mulh
          • Exec-lwu
          • Exec-xor
          • Exec-subw
          • Exec-or
          • Exec-lhu
          • Exec-lbu
          • Exec-and
          • Exec-sd
          • Exec-mul
          • Exec-lh
          • Exec-ld
          • Exec-lb
          • Exec-sh
          • Exec-sb
          • Exec-lw
          • Exec-lui
          • Eff-addr
          • Exec-instr
        • Features
        • States
        • Instructions
        • Encoding
        • Reads-over-writes
        • Execution
        • Decoding
      • Executable
      • Specialized
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Semantics

Exec-instr

Semantics of instructions.

Signature

(exec-instr instr pc stat feat) → new-stat

Arguments

instr — Guard (instrp instr).

stat — Guard (statp stat).

feat — Guard (featp feat).

Returns

new-stat — Type (statp new-stat).

Definitions and Theorems

Function: exec-instr

(defun exec-instr (instr pc stat feat)
 (declare (xargs :guard (and (instrp instr)
                             (statp stat)
                             (featp feat))))
 (declare (xargs :guard (and (instr-validp instr feat)
                             (cond ((feat-32p feat) (ubyte32p pc))
                                   ((feat-64p feat) (ubyte64p pc))
                                   (t (impossible)))
                             (stat-validp stat feat))))
 (let ((__function__ 'exec-instr))
   (declare (ignorable __function__))
   (instr-case
        instr
        :op-imm (exec-op-imm instr.funct
                             instr.rd instr.rs1 instr.imm stat feat)
        :op-imms32
        (exec-op-imms32 instr.funct
                        instr.rd instr.rs1 instr.imm stat feat)
        :op-imms64
        (exec-op-imms64 instr.funct
                        instr.rd instr.rs1 instr.imm stat feat)
        :op-imm-32
        (exec-op-imm-32 instr.funct
                        instr.rd instr.rs1 instr.imm stat feat)
        :op-imms-32
        (exec-op-imms-32 instr.funct
                         instr.rd instr.rs1 instr.imm stat feat)
        :lui (exec-lui instr.rd instr.imm stat feat)
        :auipc (exec-auipc instr.rd instr.imm pc stat feat)
        :op (exec-op instr.funct
                     instr.rd instr.rs1 instr.rs2 stat feat)
        :op-32 (exec-op-32 instr.funct
                           instr.rd instr.rs1 instr.rs2 stat feat)
        :jal (exec-jal instr.rd instr.imm pc stat feat)
        :jalr (exec-jalr instr.rd
                         instr.rs1 instr.imm pc stat feat)
        :branch (exec-branch instr.funct instr.rs1
                             instr.rs2 instr.imm pc stat feat)
        :load (exec-load instr.funct
                         instr.rd instr.rs1 instr.imm stat feat)
        :store (exec-store instr.funct instr.rs1
                           instr.rs2 instr.imm stat feat))))

Theorem: statp-of-exec-instr

(defthm statp-of-exec-instr
  (b* ((new-stat (exec-instr instr pc stat feat)))
    (statp new-stat))
  :rule-classes :rewrite)

Theorem: stat-validp-of-exec-instr

(defthm stat-validp-of-exec-instr
  (implies (and (stat-validp stat feat)
                (instr-validp instr feat))
           (b* ((?new-stat (exec-instr instr pc stat feat)))
             (stat-validp new-stat feat))))

Theorem: exec-instr-of-instr-fix-instr

(defthm exec-instr-of-instr-fix-instr
  (equal (exec-instr (instr-fix instr)
                     pc stat feat)
         (exec-instr instr pc stat feat)))

Theorem: exec-instr-instr-equiv-congruence-on-instr

(defthm exec-instr-instr-equiv-congruence-on-instr
  (implies (instr-equiv instr instr-equiv)
           (equal (exec-instr instr pc stat feat)
                  (exec-instr instr-equiv pc stat feat)))
  :rule-classes :congruence)

Theorem: exec-instr-of-stat-fix-stat

(defthm exec-instr-of-stat-fix-stat
  (equal (exec-instr instr pc (stat-fix stat)
                     feat)
         (exec-instr instr pc stat feat)))

Theorem: exec-instr-stat-equiv-congruence-on-stat

(defthm exec-instr-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (exec-instr instr pc stat feat)
                  (exec-instr instr pc stat-equiv feat)))
  :rule-classes :congruence)

Theorem: exec-instr-of-feat-fix-feat

(defthm exec-instr-of-feat-fix-feat
  (equal (exec-instr instr pc stat (feat-fix feat))
         (exec-instr instr pc stat feat)))

Theorem: exec-instr-feat-equiv-congruence-on-feat

(defthm exec-instr-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (exec-instr instr pc stat feat)
                  (exec-instr instr pc stat feat-equiv)))
  :rule-classes :congruence)