Rlp-encode-trees-injectivity-proof
Injectivity of rlp-encode-tree
and rlp-encode-tree-list,
over the encodable trees and lists thereof.
This is proved by induction.
There are two theorems:
one for rlp-encode-tree
and one for rlp-encode-tree-list.
The theorems are formulated similarly to
the one for rlp-encode-bytes.
Since the theorems involve two variables (two trees or two lists of trees),
we locally define mutually recursive functions tree and tree-list
to obtain and use an induction scheme that applies to two variables;
we use the flag theorem macro generated by this local defines.
Attempting to induct according to the mutually recursive encoding functions
only applies to one variable,
leaving the other variable unchanged in the hypotheses and conclusions
of the induction steps:
then the same unchanged variable cannot suitably ``relate''
to the different instances of the changing variable
in the hypotheses and conclusions.
Submitting the injectivity theorems
via the flag theorem macro of the encoding functions,
an examining the induction scheme printed by ACL2,
should make the problem apparent.
The induction proof makes use of two helper lemmas.
The first helper lemma applies to the two cases in which
x is a leaf tree and y is a leaf tree.
Commenting out this helper lemma from the hints of the induction theorem
shows the two corresponding subgoals,
in which the hypothesis that x or y is a leaf tree
causes rlp-encode-tree to expand on x or y,
generating a call to rlp-encode-bytes on the subtrees.
This motivates the formulation of the first helper lemma,
whose variable xy stands for x or y
and whose variable yx stands for y or x,
i.e. the other variable whose rlp-encode-tree in the subgoal
is not expanded.
We use an expansion hint to expand that; an enable hint does not suffice.
If yx is also a leaf tree,
rlp-encode-tree reduces to rlp-encode-bytes on the subtrees
and the injectivity theorem of rlp-encode-bytes applies.
Otherwise, the expansion starts with a byte that is at least 192 or 247,
which is incompatible with
the starting byte of rlp-encode-bytes on (the subtrees of) xy:
the linear rule car-of-rlp-encode-bytes-upper-bound-when-no-error
does not apply here,
so we use a :use hint with a suitable instantiation.
The second helper lemma applies to the case in which
the lists of trees xs and ys are not empty.
In this case, their encodings are the appends
of the encodings of their cars and of their cdrs.
Commenting out this helper lemma from the hints of the induction theorem
shows a subgoal that involves these appends.
To use the induction hypotheses,
we need to decompose the equality of the appends
into the equalities of their car and cdr encodings,
via the rule equal-of-appends-decompose
that we also used to prove the injectivity of rlp-encode-bytes.
For this, we need to relieve the hypothesis of that rule
that the lengths of the encodings of the cars are equal:
this is done by the lemma car-encodings-same-len.
The key to proving car-encodings-same-len
is the fact that the lengths of the encodings of the cars
are completely determined by the first (few) bytes of the encodings,
as expressed by the rule len-of-rlp-encode-tree-from-prefix,
which we therefore enable to prove car-encodings-same-len.
This rule rewrites the two lengths to prove equal
in terms of the first (few) bytes of the encodings
of the cars of xs and ys:
if we knew that those encodings were equal, we would be done.
But we only know (see hypothesis in car-encodings-same-len)
that the appends of the encodings of the cars
with something else (the encodings of the cdrs) are equal.
Fortunately, the first (few) bytes of the encodings of the cars
are also the first (few) bytes of the appends.
So we use the rules
expand-to-car-of-append and expand-to-take-of-append
to express the first (few) bytes that describe the lengths
in terms of the appends;
note that these two rules have a strictly more complex right hand side,
so they are generally undesirable,
yet they are useful in this proof.
We disable the rules
acl2::car-of-append and acl2::take-of-append,
which work ``against''
expand-to-car-of-append and expand-to-take-of-append,
to prevent the rewriter from looping.
The two helper lemmas are enabled
in the proof by induction of the injectivity lemmas,
along with the rule true-listp-when-byte-listp-rewrite,
which serves to prove another subgoal
(visible by commenting out this rule in the hints),
similar to the one proved via the second helper lemma,
but simpler due to an extra hypothesis (equal (cdr xs) (cdr ys)).
Similarly to the injectivity theorem for rlp-encode-bytes,
the injectivity theorems
for rlp-encode-tree and rlp-encode-tree-list
omit the rlp-treep and rlp-tree-listp hypotheses
and weaken the equality
with rlp-tree-fix and rlp-tree-list-fix.
These theorems subsume the lemmas,
but attempting to prove directly the theorems by induction fails.
Definitions and Theorems
Theorem: rlp-encode-tree-injective
(defthm rlp-encode-tree-injective
(implies (and (not (mv-nth 0 (rlp-encode-tree x)))
(not (mv-nth 0 (rlp-encode-tree y))))
(equal (equal (mv-nth 1 (rlp-encode-tree x))
(mv-nth 1 (rlp-encode-tree y)))
(equal (rlp-tree-fix x)
(rlp-tree-fix y)))))
Theorem: rlp-encode-tree-list-injective
(defthm rlp-encode-tree-list-injective
(implies (and (not (mv-nth 0 (rlp-encode-tree-list xs)))
(not (mv-nth 0 (rlp-encode-tree-list ys))))
(equal (equal (mv-nth 1 (rlp-encode-tree-list xs))
(mv-nth 1 (rlp-encode-tree-list ys)))
(equal (rlp-tree-list-fix xs)
(rlp-tree-list-fix ys)))))