		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-plain-string-literal

Evaluate a plain string literal to a value.

Signature
(eval-plain-string-literal pstring) → val
Arguments: pstring — Guard (plain-stringp pstring).
Returns: val — Type (value-resultp val).

We convert the list of string elements to a list of bytes. If the resulting bytes exceed 32 in number, it is an error. Otherwise, we pad the list with zeros (bytes of value 0) on the right to reach 32 bytes, and we turn the resulting list of 32 bytes to a 256-bit word, interpreting the bytes in big endian form, i.e. the first byte contains the most significant bits of the word. This evaluation is not described in detail in [Yul], but it was explained via discussions on Gitter, and [Yul] is being extended with these explanations.

Definitions and Theorems

Function: eval-plain-string-literal

(defun eval-plain-string-literal (pstring)
  (declare (xargs :guard (plain-stringp pstring)))
  (let ((__function__ 'eval-plain-string-literal))
    (declare (ignorable __function__))
    (b* ((content (plain-string->content pstring))
         (bytes (eval-string-element-list content))
         ((unless (<= (len bytes) 32))
          (reserrf (list :plain-string-too-long bytes)))
         (bytes (append bytes (repeat (- 32 (len bytes)) 0))))
      (value (acl2::bebytes=>nat bytes)))))

Theorem: value-resultp-of-eval-plain-string-literal

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

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

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

Theorem: eval-plain-string-literal-of-plain-string-fix-pstring

(defthm eval-plain-string-literal-of-plain-string-fix-pstring
  (equal (eval-plain-string-literal (plain-string-fix pstring))
         (eval-plain-string-literal pstring)))

Theorem: eval-plain-string-literal-plain-string-equiv-congruence-on-pstring

(defthm
 eval-plain-string-literal-plain-string-equiv-congruence-on-pstring
 (implies (plain-string-equiv pstring pstring-equiv)
          (equal (eval-plain-string-literal pstring)
                 (eval-plain-string-literal pstring-equiv)))
 :rule-classes :congruence)