Rlp-encode-bytes-injectivity-proof
Injectivity of rlp-encode-bytes,
over the encodable byte arrays.
We prove, as a preliminary lemma, that
if two byte arrays are encodable
(i.e. the error result of rlp-encode-bytes is nil for both),
and their encodings are the same
(i.e. the bytes results of rlp-encode-bytes are identical),
then the two byte arrays are identical.
Then we use the lemma to prove the theorem in a form that
omits the byte-listp hypotheses
and weakens the equality to byte-list-equiv
(i.e. equality of byte-list-fix applied to both).
The theorem readily subsumes the lemma
because of the fixing theorems for byte-list,
but attempting to prove the theorem directly
(instead of via the lemma first) fails.
The lemma is proved automatically,
by unfolding rlp-encode-bytes
and letting ACL2 handle all the combinations of the encoding cases.
Critically, the proof for
the case in which both byte arrays are encoded with a big endian length
uses the rule equal-of-appends-decompose
to reduce the equality of the two encodings
to the equality of the parts of the encodings after the lengths
(these parts are the byte arrays being encoded);
the hypothesis of this rule,
namely that the lengths of the two big endian lengths are the same,
is relieved from the equality
between the first byte of the two encodings.
Definitions and Theorems
Theorem: rlp-encode-bytes-injective
(defthm rlp-encode-bytes-injective
(implies (and (not (mv-nth 0 (rlp-encode-bytes x)))
(not (mv-nth 0 (rlp-encode-bytes y))))
(equal (equal (mv-nth 1 (rlp-encode-bytes x))
(mv-nth 1 (rlp-encode-bytes y)))
(equal (byte-list-fix x)
(byte-list-fix y)))))
