		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Stat32-from-stat

Convert from stat-rv32im-le-p to stat32.

Signature
(stat32-from-stat stat) → stat32
Arguments: stat — Guard (stat-rv32im-le-p stat).
Returns: stat32 — Type (stat32p stat32).

Definitions and Theorems

Function: stat32-from-stat

(defun stat32-from-stat (stat)
  (declare (xargs :guard (stat-rv32im-le-p stat)))
  (make-stat32 :xregs (riscv::stat->xregs stat)
               :pc (riscv::stat->pc stat)
               :memory (riscv::stat->memory stat)
               :error (riscv::stat->error stat)))

Theorem: stat32p-of-stat32-from-stat

(defthm stat32p-of-stat32-from-stat
  (b* ((stat32 (stat32-from-stat stat)))
    (stat32p stat32))
  :rule-classes :rewrite)