Discuss: enforce mul_by_inverse

[weikengchen]

Description

It seems that the mul_by_inverse implementation has a soundness issue that the newly allocated d_inv does not need to be the inverse of d but could be any value. This can be a soundness issue as the poly gadgets have used this API.

The speed improvement seems okay for FpVar, but the constraint needs to be manually written (otherwise, mul + inverse or mul + equal always cause two constraints).

It passes the existing tests.

---

Before we can merge this PR, please make sure that all the following items have been
checked off. If any of the checklist items are not applicable, please leave them but
write a little note why.

• Targeted PR against correct branch (master)
• Linked to Github issue with discussion and accepted design OR have an explanation in the PR that describes this work.
• Wrote unit tests
• Updated relevant documentation in the code
• Added a relevant changelog entry to the Pending section in CHANGELOG.md
• Re-reviewed Files changed in the Github PR explorer

[weikengchen]

This one would need a little bit more mental effort to review, as it is not straightforward.

[Pratyush]

I feel like we previously used to enforce these constraints; was there a reason why we stopped, @ValarDragon ?

[weikengchen]

I think this issue was noticed in the discussion of #42 (comment) but we just forgot to follow up with it.

[weikengchen]

Nope, I found that this one (the one-constraint version) is still not sound.

When self = 0, d = 0, doing mul_by_inverse, the constraint system is satisfiable, but it should be unsatisfiable since the result is also wrong. And this is problematic because this allows double_and_double in NonZeroAffine to go through if the self and other are the same, but it shouldn't since the result will be incorrect.

[weikengchen]

It is another thing to discuss: do we want to require the caller to mul_by_inverse to ensure that self is not zero (NOTE: not d to be nonzero, but self)? Since this soundness issue, with the change in this PR, is only present now when self = 0, d = 0.

This has an effect on non-zero affine gadgets, as it now requires additional constraints to handle the case of adding the point to itself and doubling-and-adding the point to itself.

[weikengchen]

Given the discussion above, it seems that all the single-constraint implementation of mul_by_inverse would have soundness issues somewhere.

So, I replaced the mul_by_inverse with the naive implementation of getting the inverse and then multiplying the inverse. This change is somehow needed for the soundness of NonZeroAffine.

[Pratyush]

Hmm it should not be satisfiable; the constraint we want is that self * d == 1, right? In the prime field case, that can be performed by allocating d, and enforcing the foregoing constraint.

the appropriate pseudocode seems to be

allocate d_inv
allocate prod = self * d_inv
enforce prod * d = self (via prod.mul_equals(d, self))

I think for the self == 0 case, prod is going to be 0 no matter what, and d == 0 case is explicitly ruled out by the precondition. We can rename the method to mul_by_inverse_unchecked to emphasize that it does not check that d != 0?

[ValarDragon]

If we require the caller to ensure that d != 0, that also restricts us from being in the situation where self == 0, d== 0.

Definitely looks this has always been missing the mul_equals constraint, RIP :/

[ValarDragon]

I think this also suggests we need a general way of having tests identify allocated vars within a gadget, and try randomly mutating one at a time and ensuring failure.

[weikengchen]

Following Pratyush's suggestion, I think this:

allocate d_inv
allocate prod = self * d_inv
enforce prod * d = self (via prod.mul_equals(d, self))

has two things:
(1) first, it seems that one does not need to allocate d_inv since it is not being used.
(2) it will be satisfiable when self = 0 and d = 0, in which case prod can be any value, and that is not sound.

[weikengchen]

We may consider mul_by_inverse_unchecked where the developer is responsible to make sure d != 0 otherwise the behavior is undefined.

[weikengchen]

I will merge this one sooner, and we may need to release a new version (0.3.1) + make a security announcement, based on the discussion in Telegram.

I feel that likely we will let mul_by_inverse stay a simple combination of inverse and multiple, and add a new function mul_by_inverse_unchecked as described above.