|
|
|---|
|
|
|
|---|
Evaluate a hex string literal to a value.
(eval-hex-string-literal hstring) → val
We convert the hex pairs to a list of bytes, empty if the hex string is empty. 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.
Function:
(defun eval-hex-string-literal (hstring) (declare (xargs :guard (hex-stringp hstring))) (let ((__function__ 'eval-hex-string-literal)) (declare (ignorable __function__)) (b* (((hex-string hstring) hstring) (bytes (hex-string-content-option-case hstring.content :some (eval-hex-string-content hstring.content.val) :none nil)) ((unless (<= (len bytes) 32)) (reserrf (list :hex-string-too-long bytes))) (bytes (append bytes (repeat (- 32 (len bytes)) 0)))) (value (bebytes=>nat bytes)))))
Theorem:
(defthm value-resultp-of-eval-hex-string-literal (b* ((val (eval-hex-string-literal hstring))) (value-resultp val)) :rule-classes :rewrite)
Theorem:
(defthm error-info-wfp-of-eval-hex-string-literal (b* ((?val (eval-hex-string-literal hstring))) (implies (reserrp val) (error-info-wfp val))))
Theorem:
(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:
(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)