		Search-engine friendly clone of the ACL2 documentation.

Rlp-decoding-declarative

Rlp-decode-scalar

RLP decoding of a scalar.

Signature
(rlp-decode-scalar encoding) → (mv error? scalar)
Arguments: encoding — Guard (byte-listp encoding).
Returns: error? — Type (booleanp error?).; scalar — Type (natp scalar).

This is analogous to rlp-decode-tree. If the returned error flag is t, we return 0 as the (irrelevant) second result.

Analogously to rlp-decode-bytes, we use the injectivity of rlp-encode-bytes to prove a relationship between rlp-scalar-encoding-witness and rlp-bytes-encoding-witness, as well as a theorem that provides an alternative definition of rlp-decode-scalar in terms of rlp-decode-bytes.

Definitions and Theorems

Function: rlp-decode-scalar

(defun rlp-decode-scalar (encoding)
  (declare (xargs :guard (byte-listp encoding)))
  (b* ((encoding (byte-list-fix encoding)))
    (if (rlp-scalar-encoding-p encoding)
        (mv nil
            (rlp-scalar-encoding-witness encoding))
      (mv t 0))))

Theorem: booleanp-of-rlp-decode-scalar.error?

(defthm booleanp-of-rlp-decode-scalar.error?
  (b* (((mv ?error? ?scalar)
        (rlp-decode-scalar encoding)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: natp-of-rlp-decode-scalar.scalar

(defthm natp-of-rlp-decode-scalar.scalar
  (b* (((mv ?error? ?scalar)
        (rlp-decode-scalar encoding)))
    (natp scalar))
  :rule-classes :rewrite)

Theorem: rlp-encode-scalar-of-rlp-decode-scalar

(defthm rlp-encode-scalar-of-rlp-decode-scalar
  (implies (rlp-scalar-encoding-p encoding)
           (b* (((mv d-error? d-scalar)
                 (rlp-decode-scalar encoding))
                ((mv e-error? e-encoding)
                 (rlp-encode-scalar d-scalar)))
             (and (not d-error?)
                  (not e-error?)
                  (equal e-encoding (byte-list-fix encoding))))))

Theorem: rlp-decode-scalar-of-rlp-encode-scalar

(defthm rlp-decode-scalar-of-rlp-encode-scalar
  (b* (((mv e-error? encoding)
        (rlp-encode-scalar scalar))
       ((mv d-error? scalar1)
        (rlp-decode-scalar encoding)))
    (implies (not e-error?)
             (and (not d-error?)
                  (equal scalar1 (nfix scalar))))))

Theorem: rlp-bytes-encoding-witness-as-rlp-scalar-encoding-witness

(defthm rlp-bytes-encoding-witness-as-rlp-scalar-encoding-witness
 (implies
    (rlp-scalar-encoding-p encoding)
    (equal (rlp-bytes-encoding-witness encoding)
           (nat=>bebytes* (rlp-scalar-encoding-witness encoding)))))

Theorem: rlp-scalar-encoding-witness-as-rlp-bytes-encoding-witness

(defthm rlp-scalar-encoding-witness-as-rlp-bytes-encoding-witness
 (implies
      (rlp-scalar-encoding-p encoding)
      (equal (rlp-scalar-encoding-witness encoding)
             (bebytes=>nat (rlp-bytes-encoding-witness encoding)))))

Theorem: rlp-decode-scalar-alt-def

(defthm rlp-decode-scalar-alt-def
  (equal (rlp-decode-scalar encoding)
         (b* (((mv error? bytes)
               (rlp-decode-bytes encoding))
              ((when error?) (mv t 0))
              ((unless (equal (trim-bendian* bytes) bytes))
               (mv t 0))
              (scalar (bebytes=>nat bytes)))
           (mv nil scalar))))

Theorem: rlp-decode-scalar-of-byte-list-fix-encoding

(defthm rlp-decode-scalar-of-byte-list-fix-encoding
  (equal (rlp-decode-scalar (byte-list-fix encoding))
         (rlp-decode-scalar encoding)))

Theorem: rlp-decode-scalar-byte-list-equiv-congruence-on-encoding

(defthm rlp-decode-scalar-byte-list-equiv-congruence-on-encoding
  (implies (byte-list-equiv encoding encoding-equiv)
           (equal (rlp-decode-scalar encoding)
                  (rlp-decode-scalar encoding-equiv)))
  :rule-classes :congruence)