		Search-engine friendly clone of the ACL2 documentation.

Semantics64

Exec64-instr

Semantics of instructions.

Signature
(exec64-instr instr pc stat) → new-stat
Arguments: instr — Guard (instrp instr).; pc — Guard (ubyte64p pc).; stat — Guard (state64p stat).
Returns: new-stat — Type (state64p new-stat).

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

Definitions and Theorems

Function: exec64-instr

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

Theorem: state64p-of-exec64-instr

(defthm state64p-of-exec64-instr
  (b* ((new-stat (exec64-instr instr pc stat)))
    (state64p new-stat))
  :rule-classes :rewrite)

Theorem: exec64-instr-of-instr-fix-instr

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

Theorem: exec64-instr-instr-equiv-congruence-on-instr

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

Theorem: exec64-instr-of-ubyte64-fix-pc

(defthm exec64-instr-of-ubyte64-fix-pc
  (equal (exec64-instr instr (ubyte64-fix pc)
                       stat)
         (exec64-instr instr pc stat)))

Theorem: exec64-instr-ubyte64-equiv-congruence-on-pc

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

Theorem: exec64-instr-of-state64-fix-stat

(defthm exec64-instr-of-state64-fix-stat
  (equal (exec64-instr instr pc (state64-fix stat))
         (exec64-instr instr pc stat)))

Theorem: exec64-instr-state64-equiv-congruence-on-stat

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