		Search-engine friendly clone of the ACL2 documentation.

Rv32im-le-states

Stat-from-stat32

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

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

Definitions and Theorems

Function: stat-from-stat32

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

Theorem: stat-rv32im-le-p-of-stat-from-stat32

(defthm stat-rv32im-le-p-of-stat-from-stat32
  (b* ((stat (stat-from-stat32 stat32)))
    (stat-rv32im-le-p stat))
  :rule-classes :rewrite)

Theorem: stat-from-stat32-of-stat32-fix-stat32

(defthm stat-from-stat32-of-stat32-fix-stat32
  (equal (stat-from-stat32 (stat32-fix stat32))
         (stat-from-stat32 stat32)))

Theorem: stat-from-stat32-stat32-equiv-congruence-on-stat32

(defthm stat-from-stat32-stat32-equiv-congruence-on-stat32
  (implies (stat32-equiv stat32 stat32-equiv)
           (equal (stat-from-stat32 stat32)
                  (stat-from-stat32 stat32-equiv)))
  :rule-classes :congruence)