		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Stat1-from-stat

Turn a stat value into a stat1 value.

Signature
(stat1-from-stat stat) → stat1
Arguments: stat — Guard (statp stat).
Returns: stat1 — Type (stat1p stat1).

A transformation that generates the stobj definition from stat could also generate this conversion function.

This is executable, but the values it returns are unrelated to the live stobj.

Definitions and Theorems

Function: stat1-from-stat

(defun stat1-from-stat (stat)
  (declare (xargs :guard (statp stat)))
  (let ((__function__ 'stat1-from-stat))
    (declare (ignorable __function__))
    (make-stat1 (stat->xregs stat)
                (stat->pc stat)
                (stat->memory stat)
                (stat->error stat))))

Theorem: stat1p-of-stat1-from-stat

(defthm stat1p-of-stat1-from-stat
  (b* ((stat1 (stat1-from-stat stat)))
    (stat1p stat1))
  :rule-classes :rewrite)

Theorem: stat1-from-stat-of-stat-fix-stat

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

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

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