# 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)))))