@@ -6,7 +6,7 @@ use curve25519_dalek::scalar::Scalar;
66/// The interface for a constraint system, abstracting over the prover
77/// and verifier's roles.
88///
9- /// Statements to be proved by an [`R1CSProof`] are specified by
9+ /// Statements to be proved by an [`R1CSProof`](::r1cs::R1CSProof) are specified by
1010/// programmatically constructing constraints. These constraints need
1111/// to be identical between the prover and verifier, since the prover
1212/// and verifier need to construct the same statement.
@@ -16,35 +16,43 @@ use curve25519_dalek::scalar::Scalar;
1616/// using the `ConstraintSystem` trait, so that the prover and
1717/// verifier share the logic for specifying constraints.
1818pub trait ConstraintSystem {
19- /// Constrain `left`, `right`, and `out` linear combinations such that:
20- /// `left` = `l_var` (by adding a constraint)
21- /// `right` = `r_var` (by adding a constraint)
22- /// `out` = `o_var` (by adding a constraint)
23- /// `l_var` * `r_var` = `o_var` (by allocating multiplier variables)
24- /// Where:
25- /// `l_var` is either `left.eval()` (prover) or `Missing` (verifier)
26- /// `r_var` is either `right.eval()` (prover) or `Missing` (verifier)
27- /// `o_var` is either `out.eval()` (prover) or `Missing` (verifier)
28- /// This is used when all three gates of a multiplication gate should be
29- /// constrained by linear constraints.
19+ /// Allocate variables `left`, `right`, and `out`
20+ /// with the implicit constraint that
21+ /// ```text
22+ /// left * right = out
23+ /// ```
24+ /// and the explicit constraints that
25+ /// ```text
26+ /// left = left_constraint
27+ /// right = right_constraint
28+ /// out = out_constraint
29+ /// ```
30+ /// This is used when all three multiplier variables can be constrained up-front.
31+ ///
32+ /// Returns `(left, right, out)` for use in further constraints.
3033 fn add_constraint (
3134 & mut self ,
32- left : LinearCombination ,
33- right : LinearCombination ,
34- out : LinearCombination ,
35+ left_constraint : LinearCombination ,
36+ right_constraint : LinearCombination ,
37+ out_constraint : LinearCombination ,
3538 ) -> ( Variable , Variable , Variable ) ;
3639
37- /// Constrain `left` and `right` linear combinations such that:
38- /// `left` = `l_var` (by adding a constraint)
39- /// `right` = `r_var` (by adding a constraint)
40- /// `l_var` * `r_var` = `o_var` (by allocating multiplier variables)
41- /// Where:
42- /// `l_var` is either `left.eval()` (prover) or `Missing` (verifier)
43- /// `r_var` is either `right.eval()` (prover) or `Missing` (verifier)
44- /// `o_var` is either `left.eval() * right.eval()` (prover) or `Missing` (verifier)
45- /// This is used when only the left and right inputs of a multiplication gate
46- /// should be constrained by linear constraints.
47- fn add_intermediate_constraint (
40+ /// Allocate variables `left`, `right`, and `out`
41+ /// with the implicit constraint that
42+ /// ```text
43+ /// left * right = out
44+ /// ```
45+ /// and the explicit constraints that
46+ /// ```text
47+ /// left = left_constraint
48+ /// right = right_constraint
49+ /// ```
50+ /// This is used when the output variable cannot be immediately
51+ /// constrained (for instance, because it should be constrained to
52+ /// match a variable that has not yet been allocated).
53+ ///
54+ /// Returns `(left, right, out)` for use in further constraints.
55+ fn add_partial_constraint (
4856 & mut self ,
4957 left : LinearCombination ,
5058 right : LinearCombination ,
0 commit comments