|
|
|---|
|
|
|
|---|
Property that no valid RLP scalar encoding is a strict prefix of another one.
This easily follows from the analogous property for byte arrays.
Theorem:
(defthm rlp-encode-scalar-unamb-prefix (implies (and (not (mv-nth 0 (rlp-encode-scalar x))) (not (mv-nth 0 (rlp-encode-scalar y)))) (equal (prefixp (mv-nth 1 (rlp-encode-scalar x)) (mv-nth 1 (rlp-encode-scalar y))) (equal (mv-nth 1 (rlp-encode-scalar x)) (mv-nth 1 (rlp-encode-scalar y))))))