Check if the information in an error is well-formed.
For certain purposes, we need to know that the errors generated (and propagated) in our Yul formalization are well-formed according to certain criteria. Specifically, we need to know that the information is always a cons. For better encapsulation and possible future extension, we capture that in this predicate.
(defun error-info-wfp (error) (declare (xargs :guard (reserrp error))) (let ((__function__ 'error-info-wfp)) (declare (ignorable __function__)) (consp (fty::reserr->info error))))
(defthm booleanp-of-error-info-wfp (b* ((yes/no (error-info-wfp error))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm error-info-wfp-of-reserr-of-cons (error-info-wfp (reserr (cons a b))))
(defthm error-info-wfp-of-reserr-fix-error (equal (error-info-wfp (fty::reserr-fix error)) (error-info-wfp error)))
(defthm error-info-wfp-reserr-equiv-congruence-on-error (implies (fty::reserr-equiv error error-equiv) (equal (error-info-wfp error) (error-info-wfp error-equiv))) :rule-classes :congruence)