		Search-engine friendly clone of the ACL2 documentation.

Errors

Reserr-limitp

Recognize limit errors.

Signature
(reserr-limitp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

As explained in the dynamic semantics, the ACL2 functions that formalize the execution of Yul code take an artificial limit counter as input, and return an error when that limit is exhausted. This is one of several kinds of errors that may be returned by those ACL2 functions, which formalize a defensive dynamic semantics.

Here we define a predicate that recognizes limit errors, i.e. values of type reserr whose innermost information starts with the keyword :limit, where `innermost' refers to the stack discussed in reserrf and fty::reserrf-push. The adequacy of this predicate definition depends on the definition of the ACL2 execution functions for Yul, in particular the fact that they return error limits of this form. This predicate must be adapted if that form changes.

Definitions and Theorems

Function: reserr-limitp-aux

(defun reserr-limitp-aux (stack)
  (declare (xargs :guard t))
  (let ((__function__ 'reserr-limitp-aux))
    (declare (ignorable __function__))
    (cond ((atom stack) nil)
          ((atom (cdr stack))
           (b* ((fun-info (car stack))
                ((unless (and (consp fun-info)
                              (consp (cdr fun-info))))
                 nil)
                (info (cadr fun-info))
                ((unless (consp info)) nil))
             (eq (car info) :limit)))
          (t (reserr-limitp-aux (cdr stack))))))

Theorem: booleanp-of-reserr-limitp-aux

(defthm booleanp-of-reserr-limitp-aux
  (b* ((yes/no (reserr-limitp-aux stack)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Function: reserr-limitp

(defun reserr-limitp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'reserr-limitp))
    (declare (ignorable __function__))
    (and (reserrp x)
         (b* ((info (fty::reserr->info x)))
           (reserr-limitp-aux info)))))

Theorem: booleanp-of-reserr-limitp

(defthm booleanp-of-reserr-limitp
  (b* ((yes/no (reserr-limitp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)