Check if a state is valid with respect to given features.
As explained in stat, that fixtype models all possible machine states for all possible features. Here we define restrictions based on features.
The features dictate
the size
Based on
The size of the memory is
Function:
(defun stat-validp (stat feat) (declare (xargs :guard (and (statp stat) (featp feat)))) (let ((__function__ 'stat-validp)) (declare (ignorable __function__)) (b* (((stat stat) stat) (xlen (feat->xlen feat)) (xnum (feat->xnum feat))) (and (unsigned-byte-listp xlen stat.xregs) (equal (len stat.xregs) (1- xnum)) (unsigned-byte-p xlen stat.pc) (equal (len stat.memory) (expt 2 xlen))))))
Theorem:
(defthm booleanp-of-stat-validp (b* ((yes/no (stat-validp stat feat))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-stat->xregs (implies (stat-validp stat feat) (true-listp (stat->xregs stat))) :rule-classes :type-prescription)
Theorem:
(defthm unsigned-byte-listp-of-stat->xregs (implies (stat-validp stat feat) (unsigned-byte-listp (feat->xlen feat) (stat->xregs stat))))
Theorem:
(defthm ubyte32-listp-of-stat->xregs-when-32p (implies (and (stat-validp stat feat) (feat-32p feat)) (ubyte32-listp (stat->xregs stat))))
Theorem:
(defthm ubyte64-listp-of-stat->xregs-when-64p (implies (and (stat-validp stat feat) (feat-64p feat)) (ubyte64-listp (stat->xregs stat))))
Theorem:
(defthm len-of-stat->xregs (implies (stat-validp stat feat) (equal (len (stat->xregs stat)) (1- (feat->xnum feat)))))
Theorem:
(defthm unsigned-byte-p-of-stat->pc (implies (stat-validp stat feat) (unsigned-byte-p (feat->xlen feat) (stat->pc stat))))
Theorem:
(defthm ubyte32p-of-stat->pc-when-32p (implies (and (stat-validp stat feat) (feat-32p feat)) (ubyte32p (stat->pc stat))))
Theorem:
(defthm ubyte64p-of-stat->pc-when-64p (implies (and (stat-validp stat feat) (feat-64p feat)) (ubyte64p (stat->pc stat))))
Theorem:
(defthm len-of-stat->memory (implies (stat-validp stat feat) (equal (len (stat->memory stat)) (expt 2 (feat->xlen feat)))))
Theorem:
(defthm stat-validp-of-stat-fix-stat (equal (stat-validp (stat-fix stat) feat) (stat-validp stat feat)))
Theorem:
(defthm stat-validp-stat-equiv-congruence-on-stat (implies (stat-equiv stat stat-equiv) (equal (stat-validp stat feat) (stat-validp stat-equiv feat))) :rule-classes :congruence)
Theorem:
(defthm stat-validp-of-feat-fix-feat (equal (stat-validp stat (feat-fix feat)) (stat-validp stat feat)))
Theorem:
(defthm stat-validp-feat-equiv-congruence-on-feat (implies (feat-equiv feat feat-equiv) (equal (stat-validp stat feat) (stat-validp stat feat-equiv))) :rule-classes :congruence)