|
|
|---|
|
|
|
|---|
*uncommitted-sapling* is not in the image of pedersen.
This was Theorem 5.4.2 in certain earlier versions of [ZPS], such as version 2020.1.0. Later versions of [ZPS] have similar theorems, but not quite the same. In any case, this property still holds, and it is proved here.
The theorem is of interest when pedersen returns a good hash,
which requires pedersen-point to return a Jubjub point.
However, since our definition of pedersen
returns
We first prove the case in which pedersen-point returns a point, and we use the definition of *uncommitted-sapling* in this lemma. This is critical for the injectivity theorem of i2lebsp to apply, which reduces the goal to the inequality of the abscissa of a Jubjub point with 1, which is false by jubjub-point-abscissa-is-not-1. The latter theorem is disabled, but it appears that ACL2's tau system makes use of it.
Theorem:
(defthm pedersen-is-not-uncommitted-sapling (not (equal (pedersen d m) *uncommitted-sapling*)))