		Search-engine friendly clone of the ACL2 documentation.

Rlp-decodability

Rlp-encode-bytes-prefix-unambiguity-proof

Property that no valid RLP byte array encoding is a strict prefix of another one.

This is expressed by saying that if a valid encoding is a prefix of another one, the two encodings must be equal. Thus, it is not possible for a valid encoding to be a strict prefix of another valid encoding.

We do a case split on whether the two encodings have the same length (in which case the prefix relationship implies equality), or not. In the latter case, we show that in fact the two encodings must have the same length (and therefore we get a contradiction), because the length of an encoding is determined by its first byte or few bytes: we thus enable the rule len-of-rlp-encode-bytes-from-prefix. We use suitable instances of acl2::same-car-when-prefixp-and-consp and acl2::same-take-when-prefixp-and-longer to establish that the first (few) bytes of the encodings are the same.

Definitions and Theorems

Theorem: rlp-encode-bytes-unamb-prefix

(defthm rlp-encode-bytes-unamb-prefix
  (implies (and (not (mv-nth 0 (rlp-encode-bytes x)))
                (not (mv-nth 0 (rlp-encode-bytes y))))
           (equal (prefixp (mv-nth 1 (rlp-encode-bytes x))
                           (mv-nth 1 (rlp-encode-bytes y)))
                  (equal (mv-nth 1 (rlp-encode-bytes x))
                         (mv-nth 1 (rlp-encode-bytes y))))))