Skip addition of trivial constraints to canonical representation of the linear relation #70
Conversation
|
Can you lint this PR? |
|
Also to address your question - do you know of any situations where we would actually want to include a trivial constraint? If not, then I'm okay with making it disallowed (as the only settings where people would try to include it, are if they are using the API incorrectly - and they should be warned if so!) |
|
Actually, maybe there is an argument for allowing "trivial" relations - eg in the range proof, this is a nice way to denote that a relation should be checked outside of the proof: |
|
Ya, I'm not immediately sure here! Starting with the trivially false, its my feeling that this should be rejected at this canonicalization step, or as early as possible really. I know there is an argument for allowing it, as it might be part of an OR branch and so the statement as a whole may still have a proof. My concern with this is that it leads to situations where the proof may not be providing the hiding properties that were intended (e.g. A proof of "I am a dog OR x = x + 1" gives definitive proof that I am a dog). In trivially true case, if we were building the relation fully at compile-time, then I might write a rule that gives an error (or perhaps a warning) that a given constraint is trivial and can be removed. However, that's not what we are doing of course. We are filling in values for the group elements at runtime, often using values sent over to the verifier from the prover. As you mention, it is very helpful in this case to have a native way to express constraints over the public values received. If we don't provide that, then it may force the developer to hand-write that check, and be careful not to either forget to add it or end up with a check that does not match the rest of the statement (seems like bad news). However, it does feel a little odd and I think part of that may be that there is no notion of whether or not a given group element is "variable" or "constant". I am thinking about this because if there was a way to know that during this canonicalization step (or really just whenever the system knows a given constant is done being built), then I would want to reject a trivial statement containing only constants. |
|
@nategraf do you see an advantage in testing there rather than directly upon conversion? I find that having a conversion step that does all validation in one place more clear to study: |
|
Agreed that we should check during conversation primarily. We may also want to check here due to the fact that the data structure we are using can have an empty right-hand side (as opposed to having this struct not be able to represent constraints with an empty RHS). |
mmaker
force-pushed
the
victor/a-check-and-a-question
branch
from
430d5b5 to
5a8cd7c
Compare
mmaker
left a comment
mmaker
left a comment
There was a problem hiding this comment.
I think we're converging here, I have only minor comments about the documentation.
[Apologies for the git merge mess]
| .contains("trivially false constraint")); | ||
|
|
||
| // Also in this case, we know that no witness will ever satisfy the relation. | ||
| // Also here, the relation is built even though the prover will never be able to give a valid proof for it. |
There was a problem hiding this comment.
this comment needs to change I think
src/linear_relation/canonical.rs
Outdated
|
|
||
| // Only include constraints that are non-trivial (not zero constraints) | ||
| // QUESTION: Should this actually be done? In the 0 = [] case, this seems to be no loss. In | ||
| // the error case, this precludes including an always-false OR branch. |
There was a problem hiding this comment.
my understanding is that we do not need trivially false OR branches, so I'd be happy just removing the above comment
|
I think the "shortcut" of adding trivial constraints to the canonical representation, for them to get parsed out and checked outside the proof at verification time, is a neat shortcut but easily causes confusion, as it is hard to differentiate between the trivial constraint (eg in the range proof here, the check that C is the sum of the secret shares: https://github.com/sigma-rs/sigma-proofs/pull/80/files#diff-bb2226f419827182b41b4c86ad14506a89355c6cffa47f007c69dbb1e041a5aeR239) and an actual constraint. I think having a different API name would help explicitly denote the difference. Maybe this would also help with the comment/confusion here:
|
|
@mmaker, I adjusted the comments you pointed to. I am not totally sure if you were also asking me to make some other changes. How does it look now. |
So, as written now a relation of only public values in our (non-canonical) What gives me some pause is that if someone were to read a serialized canonical relation and verify a proof over that statement, they would miss these checks. My understanding is that doing something like this would not be intended usage for a couple of reasons. A) Verifying a statement chosen at runtime without constraints would not provide any meaningful guarantees and B) The canonical representation is intended for Fiat-Shamir, and if not actually intended to be a wire or storage format. So, my current thought is that as written this PR is the correct handling within the canonicalization routine. I am still thinking about how we might provide more of a notion to the user of whether a given group element is "constant" or "variable", but I'm not sure how (or whether) to address this. At this point, I don't think it would handle how we do canonicalization. |
|
fantastic thank you! @cathieyun I'm closing this for now, but if you have other questions here your input is welcome. |
|
ah, wait it's still marked as a draft. let me know if you need help merging this after approval! |
A comment implied that only non-trivial constraints should be added to the canonical linear relation. This PR implemts that, but I am unsure if we actually want to include this or not. I additionally had another question about the canonicalization of the linear relations, which I've added in a comment in this PR.