|
|
|---|
|
|
|
|---|
Property that no valid RLP tree encoding is a strict prefix of another one.
This is quite analogous to the proof for byte array encoding.
We cannot, and do not need to, prove a similar property for encodings of lists of trees, because a list of encoded trees could be extended with another one. However, when we decode a list of trees, we know the total length of their super-tree, because at the top level we always start by decoding a tree, never a list of trees.
Theorem:
(defthm rlp-encode-tree-umamb-prefix (implies (and (not (mv-nth 0 (rlp-encode-tree x))) (not (mv-nth 0 (rlp-encode-tree y)))) (equal (prefixp (mv-nth 1 (rlp-encode-tree x)) (mv-nth 1 (rlp-encode-tree y))) (equal (mv-nth 1 (rlp-encode-tree x)) (mv-nth 1 (rlp-encode-tree y))))))