		Search-engine friendly clone of the ACL2 documentation.

Semantics32

Exec32-instr

Semantics of instructions.

Signature
(exec32-instr instr pc stat) → new-stat
Arguments: instr — Guard (instrp instr).; pc — Guard (ubyte32p pc).; stat — Guard (state32p stat).
Returns: new-stat — Type (state32p new-stat).

We set the error flag for the RV64I instructions because here we are in RV32I mode.

Definitions and Theorems

Function: exec32-instr

(defun exec32-instr (instr pc stat)
 (declare (xargs :guard (and (instrp instr)
                             (ubyte32p pc)
                             (state32p stat))))
 (let ((__function__ 'exec32-instr))
  (declare (ignorable __function__))
  (instr-case
       instr
       :op-imm (exec32-op-imm instr.funct
                              instr.rd instr.rs1 instr.imm stat)
       :op-imms32 (exec32-op-imms instr.funct
                                  instr.rd instr.rs1 instr.imm stat)
       :op-imms64 (error32 stat)
       :op-imm-32 (error32 stat)
       :op-imms-32 (error32 stat)
       :lui (exec32-lui instr.rd instr.imm stat)
       :auipc (exec32-auipc instr.rd instr.imm pc stat)
       :op (exec32-op instr.funct
                      instr.rd instr.rs1 instr.rs2 stat)
       :op-32 (error32 stat)
       :jal (exec32-jal instr.rd instr.imm pc stat)
       :jalr (exec32-jalr instr.rd instr.rs1 instr.imm pc stat)
       :branch (exec32-branch instr.funct
                              instr.rs1 instr.rs2 instr.imm pc stat)
       :load (exec32-load instr.funct
                          instr.rd instr.rs1 instr.imm stat)
       :store (exec32-store instr.funct
                            instr.rs1 instr.rs2 instr.imm stat))))

Theorem: state32p-of-exec32-instr

(defthm state32p-of-exec32-instr
  (b* ((new-stat (exec32-instr instr pc stat)))
    (state32p new-stat))
  :rule-classes :rewrite)

Theorem: exec32-instr-of-instr-fix-instr

(defthm exec32-instr-of-instr-fix-instr
  (equal (exec32-instr (instr-fix instr) pc stat)
         (exec32-instr instr pc stat)))

Theorem: exec32-instr-instr-equiv-congruence-on-instr

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

Theorem: exec32-instr-of-ubyte32-fix-pc

(defthm exec32-instr-of-ubyte32-fix-pc
  (equal (exec32-instr instr (ubyte32-fix pc)
                       stat)
         (exec32-instr instr pc stat)))

Theorem: exec32-instr-ubyte32-equiv-congruence-on-pc

(defthm exec32-instr-ubyte32-equiv-congruence-on-pc
  (implies (acl2::ubyte32-equiv pc pc-equiv)
           (equal (exec32-instr instr pc stat)
                  (exec32-instr instr pc-equiv stat)))
  :rule-classes :congruence)

Theorem: exec32-instr-of-state32-fix-stat

(defthm exec32-instr-of-state32-fix-stat
  (equal (exec32-instr instr pc (state32-fix stat))
         (exec32-instr instr pc stat)))

Theorem: exec32-instr-state32-equiv-congruence-on-stat

(defthm exec32-instr-state32-equiv-congruence-on-stat
  (implies (state32-equiv stat stat-equiv)
           (equal (exec32-instr instr pc stat)
                  (exec32-instr instr pc stat-equiv)))
  :rule-classes :congruence)