• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
        • Mmp-trees
        • Semaphore
        • Database
        • Cryptography
        • Rlp
          • Rlp-tree
          • Rlp-decoding-executable
          • Rlp-decodability
          • Rlp-encoding
            • Rlp-encode-tree
              • Rlp-encode-tree-list
            • Rlp-encode-bytes
            • Rlp-scalar-encoding-p
            • Rlp-bytes-encoding-p
            • Rlp-tree-encoding-p
            • Rlp-encode-scalar
          • Rlp-decoding-declarative
          • Rlp-big-endian-representations
        • Transactions
        • Hex-prefix
        • Basics
        • Addresses
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Rlp-encoding

Rlp-encode-tree

RLP encoding of a tree.

Signature

(rlp-encode-tree tree) → (mv error? encoding)

Arguments

tree — Guard (rlp-treep tree).

Returns

error? — Type (booleanp error?).

encoding — Type (byte-listp encoding).

This corresponds to \mathtt{RLP} [YP:(179)], R_{\mathrm{l}} [YP:(183)], and s [YP:(184)]. More precisely, rlp-encode-tree corresponds to \mathtt{RLP}, the branching case of rlp-encode-tree corresponds to R_{\mathrm{l}}, and rlp-encode-tree-list corresponds to s.

The first result of rlp-encode-tree and rlp-encode-tree-list is an error flag, which is t if the argument tree or list of trees 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-tree-when-no-error.

The first byte of the encoding of a leaf tree is always below 192: see theorems car-of-rlp-encode-tree-leaf-upper-bound-when-no-error and rlp-encode-tree-car-ineq-to-tree-leaf. The first byte of the encoding of a branching tree is always at least 192: see theorems car-of-rlp-encode-tree-leaf-upper-bound-when-no-error and rlp-encode-tree-car-ineq-to-tree-branch.

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-tree-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 theorems len-of-rlp-encode-tree-lower-bound-when-len-len-1 and len-of-rlp-encode-tree-lower-bound-when-len-len-2.

Once rlp-encode-tree is defined, rlp-encode-bytes could be alternatively ``defined'' by wrapping the byte array in a tree and encoding the tree. This alternative definition rule is disabled by default, but may be useful sometimes. It should not be enabled if the definition of rlp-encode-tree is enabled (since the latter is defined in terems of rlp-encode-bytes, so we add a theory invariant to that effect.

Function: rlp-encode-tree

(defun rlp-encode-tree (tree)
  (declare (xargs :guard (rlp-treep tree)))
  (rlp-tree-case
       tree :leaf (rlp-encode-bytes tree.bytes)
       :branch
       (b* (((mv error? subencoding)
             (rlp-encode-tree-list tree.subtrees))
            ((when error?) (mv t nil)))
         (cond ((< (len subencoding) 56)
                (b* ((encoding (cons (+ 192 (len subencoding))
                                     subencoding)))
                  (mv nil encoding)))
               ((< (len subencoding) (expt 2 64))
                (b* ((be (nat=>bebytes* (len subencoding)))
                     (encoding (cons (+ 247 (len be))
                                     (append be subencoding))))
                  (mv nil encoding)))
               (t (mv t nil))))))

Function: rlp-encode-tree-list

(defun rlp-encode-tree-list (trees)
  (declare (xargs :guard (rlp-tree-listp trees)))
  (b* (((when (endp trees)) (mv nil nil))
       ((mv error? encoding1)
        (rlp-encode-tree (car trees)))
       ((when error?) (mv t nil))
       ((mv error? encoding2)
        (rlp-encode-tree-list (cdr trees)))
       ((when error?) (mv t nil)))
    (mv nil (append encoding1 encoding2))))

Theorem: return-type-of-rlp-encode-tree.error?

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

Theorem: return-type-of-rlp-encode-tree.encoding

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

Theorem: return-type-of-rlp-encode-tree-list.error?

(defthm return-type-of-rlp-encode-tree-list.error?
  (b* (((mv ?error? ?encoding)
        (rlp-encode-tree-list trees)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: return-type-of-rlp-encode-tree-list.encoding

(defthm return-type-of-rlp-encode-tree-list.encoding
  (b* (((mv ?error? ?encoding)
        (rlp-encode-tree-list trees)))
    (byte-listp encoding))
  :rule-classes :rewrite)

Theorem: rlp-encode-tree-of-rlp-tree-fix-tree

(defthm rlp-encode-tree-of-rlp-tree-fix-tree
  (equal (rlp-encode-tree (rlp-tree-fix tree))
         (rlp-encode-tree tree)))

Theorem: rlp-encode-tree-list-of-rlp-tree-list-fix-trees

(defthm rlp-encode-tree-list-of-rlp-tree-list-fix-trees
  (equal (rlp-encode-tree-list (rlp-tree-list-fix trees))
         (rlp-encode-tree-list trees)))

Theorem: rlp-encode-tree-rlp-tree-equiv-congruence-on-tree

(defthm rlp-encode-tree-rlp-tree-equiv-congruence-on-tree
  (implies (rlp-tree-equiv tree tree-equiv)
           (equal (rlp-encode-tree tree)
                  (rlp-encode-tree tree-equiv)))
  :rule-classes :congruence)

Theorem: rlp-encode-tree-list-rlp-tree-list-equiv-congruence-on-trees

(defthm rlp-encode-tree-list-rlp-tree-list-equiv-congruence-on-trees
  (implies (rlp-tree-list-equiv trees trees-equiv)
           (equal (rlp-encode-tree-list trees)
                  (rlp-encode-tree-list trees-equiv)))
  :rule-classes :congruence)

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

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

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

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

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

(defthm car-of-rlp-encode-tree-branch-upper-bound-when-no-error
  (implies (and (not (mv-nth 0 (rlp-encode-tree tree)))
                (rlp-tree-case tree :branch))
           (>= (car (mv-nth 1 (rlp-encode-tree tree)))
               192))
  :rule-classes :linear)

Theorem: rlp-encode-tree-car-ineq-to-tree-leaf

(defthm rlp-encode-tree-car-ineq-to-tree-leaf
  (implies (not (mv-nth 0 (rlp-encode-tree tree)))
           (equal (<= (car (mv-nth 1 (rlp-encode-tree tree)))
                      191)
                  (rlp-tree-case tree :leaf))))

Theorem: rlp-encode-tree-car-ineq-to-tree-branch

(defthm rlp-encode-tree-car-ineq-to-tree-branch
  (implies (not (mv-nth 0 (rlp-encode-tree tree)))
           (equal (>= (car (mv-nth 1 (rlp-encode-tree tree)))
                      192)
                  (rlp-tree-case tree :branch))))

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

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

Theorem: len-of-rlp-encode-tree-lower-bound-when-len-len-1

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

Theorem: len-of-rlp-encode-tree-lower-bound-when-len-len-2

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

Theorem: consp-of-rlp-encode-tree-list-when-no-error

(defthm consp-of-rlp-encode-tree-list-when-no-error
  (implies (not (mv-nth 0 (rlp-encode-tree-list trees)))
           (equal (consp (mv-nth 1 (rlp-encode-tree-list trees)))
                  (consp trees))))

Theorem: nonnil-rlp-encode-tree-list-when-no-error

(defthm nonnil-rlp-encode-tree-list-when-no-error
  (implies (not (mv-nth 0 (rlp-encode-tree-list trees)))
           (iff (mv-nth 1 (rlp-encode-tree-list trees))
                (consp trees))))

Theorem: rlp-encode-bytes-alt-def

(defthm rlp-encode-bytes-alt-def
  (equal (rlp-encode-bytes bytes)
         (rlp-encode-tree (rlp-tree-leaf bytes))))

Subtopics

Rlp-encode-tree-list