		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-literal

Evaluate a literal.

Signature
(eval-literal lit) → val
Arguments: lit — Guard (literalp lit).
Returns: val — Type (value-resultp val).

Since for now our only values are 256-bit words, we evaluate boolean literals to 0 (for false) and 1 (for true), viewing the word as an unsigned integer. This is not described in [Yul], but it was discussed on Gitter. This should apply to at least the EVM dialect of Yul, while other dialects that include a boolean type may need to evaluate boolean literals differently. We will generalize this aspect of our formalization at some point.

A decimal or hexadecimal literal evaluates to the word whose unsigned integer value is the number represented by the literal. This number must fit in 256 bits, otherwise it is an error.

Plain and hex strings are evaluated as described in eval-plain-string-literal and eval-hex-string-literal.

Definitions and Theorems

Function: eval-literal

(defun eval-literal (lit)
 (declare (xargs :guard (literalp lit)))
 (let ((__function__ 'eval-literal))
  (declare (ignorable __function__))
  (literal-case
   lit :boolean
   (if lit.get (value 1) (value 0))
   :dec-number
   (if (ubyte256p lit.get)
       (value lit.get)
     (reserrf (list :dec-number-too-large lit.get)))
   :hex-number
   (b*
    ((num
      (str::hex-digit-chars-value (hex-digit-list->chars lit.get))))
    (if (ubyte256p num)
        (value num)
      (reserrf (list :hex-number-too-large lit.get))))
   :plain-string (eval-plain-string-literal lit.get)
   :hex-string (eval-hex-string-literal lit.get))))

Theorem: value-resultp-of-eval-literal

(defthm value-resultp-of-eval-literal
  (b* ((val (eval-literal lit)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-eval-literal

(defthm error-info-wfp-of-eval-literal
  (b* ((?val (eval-literal lit)))
    (implies (reserrp val)
             (error-info-wfp val))))

Theorem: eval-literal-of-literal-fix-lit

(defthm eval-literal-of-literal-fix-lit
  (equal (eval-literal (literal-fix lit))
         (eval-literal lit)))

Theorem: eval-literal-literal-equiv-congruence-on-lit

(defthm eval-literal-literal-equiv-congruence-on-lit
  (implies (literal-equiv lit lit-equiv)
           (equal (eval-literal lit)
                  (eval-literal lit-equiv)))
  :rule-classes :congruence)