		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-hex-string-literal

Evaluate a hex string literal to a value.

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

We convert the list of hex pairs 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-hex-string-literal

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

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

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

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

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

Theorem: eval-hex-string-literal-of-hex-string-fix-hstring

(defthm eval-hex-string-literal-of-hex-string-fix-hstring
  (equal (eval-hex-string-literal (hex-string-fix hstring))
         (eval-hex-string-literal hstring)))

Theorem: eval-hex-string-literal-hex-string-equiv-congruence-on-hstring

(defthm
     eval-hex-string-literal-hex-string-equiv-congruence-on-hstring
  (implies (hex-string-equiv hstring hstring-equiv)
           (equal (eval-hex-string-literal hstring)
                  (eval-hex-string-literal hstring-equiv)))
  :rule-classes :congruence)