		Search-engine friendly clone of the ACL2 documentation.

Rlp-encoding

Rlp-encode-bytes

RLP encoding of a byte array.

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

This corresponds to R_{\mathrm{b}} [YP:(180)].

The first result of this function is an error flag, which is t if the argument byte array cannot be encoded; in this case, nil is returned as the (irrelevant) second result.

Encodings are never empty, i.e. they always consist of at least one byte: see theorem consp-of-rlp-encode-bytes-when-no-error.

The first byte of an encoding is always below 192: see theorem car-of-rlp-encode-bytes-bound-when-no-error.

The total length of an encoding can be determined from the first few bytes (i.e. a prefix) of the encoding: see theorem len-of-rlp-encode-bytes-from-prefix. This rewrite rule is disabled by default, because it turns the left-hand side into a more complex right-hand side; however, it is usefully enabled in certain proofs.

The total length of an encoding that uses a ``long'' length field (i.e. when the initial byte is followed by the length of the length, and the actual length consists of one or more bytes) is larger than the length field itself: see theorem len-of-rlp-encode-bytes-lower-bound-when-len-len.

Definitions and Theorems

Function: rlp-encode-bytes

(defun rlp-encode-bytes (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (b* ((bytes (byte-list-fix bytes)))
    (cond ((and (= (len bytes) 1)
                (< (car bytes) 128))
           (mv nil bytes))
          ((< (len bytes) 56)
           (b* ((encoding (cons (+ 128 (len bytes)) bytes)))
             (mv nil encoding)))
          ((< (len bytes) (expt 2 64))
           (b* ((be (nat=>bebytes* (len bytes)))
                (encoding (cons (+ 183 (len be))
                                (append be bytes))))
             (mv nil encoding)))
          (t (mv t nil)))))

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

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

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

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

Theorem: consp-of-rlp-encode-bytes-when-no-error

(defthm consp-of-rlp-encode-bytes-when-no-error
  (implies (not (mv-nth 0 (rlp-encode-bytes bytes)))
           (consp (mv-nth 1 (rlp-encode-bytes bytes))))
  :rule-classes :type-prescription)

Theorem: car-of-rlp-encode-bytes-upper-bound-when-no-error

(defthm car-of-rlp-encode-bytes-upper-bound-when-no-error
  (implies (not (mv-nth 0 (rlp-encode-bytes bytes)))
           (<= (car (mv-nth 1 (rlp-encode-bytes bytes)))
               191))
  :rule-classes :linear)

Theorem: len-of-rlp-encode-bytes-from-prefix

(defthm len-of-rlp-encode-bytes-from-prefix
 (b* (((mv error? encoding)
       (rlp-encode-bytes bytes)))
  (implies
   (not error?)
   (equal
    (len encoding)
    (cond
         ((< (car encoding) 128) 1)
         ((< (car encoding) (+ 128 56))
          (1+ (- (car encoding) 128)))
         (t (b* ((lenlen (- (car encoding) 183)))
              (+ 1 lenlen
                 (bebytes=>nat (take lenlen (cdr encoding)))))))))))

Theorem: len-of-rlp-encode-bytes-lower-bound-when-len-len

(defthm len-of-rlp-encode-bytes-lower-bound-when-len-len
  (b* (((mv error? encoding)
        (rlp-encode-bytes bytes)))
    (implies (and (not error?)
                  (>= (car encoding) (+ 128 56)))
             (> (len encoding)
                (- (car encoding) 183))))
  :rule-classes :linear)

Theorem: rlp-encode-bytes-of-byte-list-fix-bytes

(defthm rlp-encode-bytes-of-byte-list-fix-bytes
  (equal (rlp-encode-bytes (byte-list-fix bytes))
         (rlp-encode-bytes bytes)))

Theorem: rlp-encode-bytes-byte-list-equiv-congruence-on-bytes

(defthm rlp-encode-bytes-byte-list-equiv-congruence-on-bytes
  (implies (byte-list-equiv bytes bytes-equiv)
           (equal (rlp-encode-bytes bytes)
                  (rlp-encode-bytes bytes-equiv)))
  :rule-classes :congruence)