|
|
|---|
|
|
|
|---|
Check if a literal is safe.
(check-safe-literal lit) → _
According to [Yul: Specification of Yul: Restrictions on the Grammar], literals cannot be larger than their types, and the largest type is that of 256-bit words. For now we do not model types (i.e. we assume one type), so we limit the size to 256 bits. To check this constraint, we just evaluate the literal and ensure that the evaluation does not return an error: this captures exactly the static constraints on literals.
We do not impose other restrictions on plain strings here, such as that a string surrounded by double quotes cannot contain (unescaped) double quotes. Those are simply syntactic restrictions.
Function:
(defun check-safe-literal (lit) (declare (xargs :guard (literalp lit))) (let ((__function__ 'check-safe-literal)) (declare (ignorable __function__)) (b* (((okf &) (eval-literal lit))) nil)))
Theorem:
(defthm reserr-optionp-of-check-safe-literal (b* ((_ (check-safe-literal lit))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-literal-of-literal-fix-lit (equal (check-safe-literal (literal-fix lit)) (check-safe-literal lit)))
Theorem:
(defthm check-safe-literal-literal-equiv-congruence-on-lit (implies (literal-equiv lit lit-equiv) (equal (check-safe-literal lit) (check-safe-literal lit-equiv))) :rule-classes :congruence)