		Search-engine friendly clone of the ACL2 documentation.

Rlp-encoding

Rlp-encode-scalar

RLP encoding of a scalar.

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

This corresponds to \mathtt{RLP} [YP:(185)].

The first result of this function is an error flag, which is t if the argument scalar is so large that its big-endian representation reaches 2^{64} in length.

Definitions and Theorems

Function: rlp-encode-scalar

(defun rlp-encode-scalar (scalar)
  (declare (xargs :guard (natp scalar)))
  (rlp-encode-bytes (nat=>bebytes* (nfix scalar))))

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

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

Theorem: byte-listp-of-rlp-encode-scalar.encoding

(defthm byte-listp-of-rlp-encode-scalar.encoding
  (b* (((mv ?error? ?encoding)
        (rlp-encode-scalar scalar)))
    (byte-listp encoding))
  :rule-classes :rewrite)

Theorem: rlp-encode-scalar-of-nfix-scalar

(defthm rlp-encode-scalar-of-nfix-scalar
  (equal (rlp-encode-scalar (nfix scalar))
         (rlp-encode-scalar scalar)))

Theorem: rlp-encode-scalar-nat-equiv-congruence-on-scalar

(defthm rlp-encode-scalar-nat-equiv-congruence-on-scalar
  (implies (acl2::nat-equiv scalar scalar-equiv)
           (equal (rlp-encode-scalar scalar)
                  (rlp-encode-scalar scalar-equiv)))
  :rule-classes :congruence)