New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
More ECC math #10
More ECC math #10
Conversation
Requires modifying Rescue::absorb and unpack_fe to take Num instead of AllocatedNum.
Still several constraints that need fixing.
// lambda = (y2 - y1) / (x2 - x1) | ||
// x3 = lambda^2 - x1 - x2 | ||
// y3 = -lambda x3 + lambda x1 - y1 | ||
// | ||
// p1 == p2: | ||
// p1 != p2, p1 == -p2: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indent this case so that it's clear that it is a subcase of the preceding one.
// (x2 - x1 + x_is_same) * lambda = (y2 - y1) | ||
// | ||
// p1 != p2, p1 == identity, p2 != identity: | ||
// lambda = (y2 - 0) / (x2 - 0) = y2/x2 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It may be worth noting that x2 cannot be zero in this case (because there is no point with x-coordinate 0 on the curve).
// = x2(y2/x2) - (y2/x2)^3 | ||
// | ||
// p1 != p2, p1 != identity, p2 == identity: | ||
// lambda = (0 - y1) / (0 - x1) = (y1/x1) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Similarly, it may be worth noting that x1 cannot be zero in this case.
// y3 = -lambda x3 + lambda x1 - y1 | ||
// = -((y1/x1)^2 - x1) x3 + (y1/x1) x1 - y1 | ||
// | ||
// p1 == p2 != identity: | ||
// lambda = (3 (x1)^2) / (2 y1) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It may be worth pointing out that y1 cannot be zero in this case (there is no point with y-coordinate zero on the curve, because the curve is prime-order). It's computed also in the case where p1 is the identity, but in that case x1 is also zero so it's satisfiable.
// lambda = (3 * (0)^2) / (2 * 0) ==> lambda = 0 | ||
// x3 = 0^2 - 2 * 0 = 0 | ||
// y3 = -0 * 0 + 0 * 0 - 0 = 0 | ||
// --> need to constrain lambda = 0 if p1_is_identity && p2_is_identity |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No we don't, because that's handled by the selection constraints: if p3_is_identity then we replace the result by (0, 0); if p1_is_identity then we replace the result by p2; and if p2_is_identity then we replace the result by p1. It's harmless to do all three, and in that case we don't care that lambda was unconstrained (we'll witness it as zero, but it doesn't matter if a dishonest prover witnesses it as something else).
// + y3 * (1 - p1_is_identity) * (1 - p2_is_identity) * (1 - p3_is_identity) | ||
// Constrain p3_is_identity: | ||
// (y2 + y1) * p3_is_identity = 0 | ||
// --> if different, is_same must be 0 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Inapplicable comment. Should be something like "if y2 + y1 != 0, p3_is_identity must be 0"
// + true * (1 - p1_is_identity) * (1 - p2_is_identity) * p3_is_identity | ||
// + p3_is_identity * (1 - p1_is_identity) * (1 - p2_is_identity) * (1 - p3_is_identity) | ||
// (y2 + y1) * (y2 + y1)^-1 = (x_is_same - p3_is_identity) | ||
// --> if the same, is_same must be 1 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"if y2 + y1 == 0, p3_identity must be x_is_same"
|
||
// (x2 - x1) * (x2 - x1)^-1 = (1 - x_is_same) | ||
// c = a = x2 - x1 | ||
// d := a^-1 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
d := a^-1 unless a == 0, in which case witness d := 1
f_val.map(|y2my1| { | ||
let inv = x2mx1.invert(); | ||
// (x2 - x1 + x_is_same) * lambda_diff = (y2 - y1) | ||
// i = x2 - x1 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
i = x2 - x1 + x_is_same
let h_val = g_val.and_then(|y1two| { | ||
i_val.map(|x1sq3| { | ||
// k = 2 y1 | ||
// l = 3 c = 3 x1^2 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is no longer 3 c. I think you mean 3 h.
cs.enforce_zero(LinearCombination::from(lambda_var) - m_var); | ||
let x3_lc = LinearCombination::from(n_var) - &x1_lc - &x2_lc; | ||
|
||
// (lambda - lambda_diff) = x_is_same * (lambda_same - lambda_diff) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Write this with the multiplication on the left to follow convention.
let mid_c = mid_c_val.ok_or(SynthesisError::AssignmentMissing)?; | ||
cs.enforce_zero(y2_lc.clone() + &y1_lc - u_var); | ||
cs.enforce_zero( | ||
LinearCombination::from(p3_is_identity.get_variable()) - p3_is_identity_var, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this needed? Surely p3_is_identity can just be allocated by the multiplication?
// + x3 * mid_e | ||
cs.enforce_zero(self.is_identity.lc(CS::ONE, Coeff::One) - cc_var); | ||
cs.enforce_zero(x2_lc - x4_var - dd_var); | ||
let x5_lc = LinearCombination::from(ee_var) + x4_var; | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is about the point where I start to get review fatigue because of the verbosity and the similarity of cases. We really really need to be able to just express constraints as R1CS and have the library handle adding the linear Sonic-style constraints; that would help a lot.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
💯 (same issue as the author!)
// lambda = (3 x_p^2)/(2 y_p) | ||
let lambda_val = match (x_p_val, y_p_val) { | ||
(Some(x_p), Some(y_p)) => { | ||
let inv_yp = (y_p + &y_p).invert(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Rename this variable to inv_2y_p
.
cs.enforce_zero(x_p_lc.clone() - a_var); | ||
cs.enforce_zero(x_p_lc.clone() - b_var); | ||
|
||
// (2 y_p) * lambda = (3 xx_p) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It might be useful to note that (because the curve is prime-order) y_p can only be zero if p is the identity, in which case xx_p is zero so this is satisfiable.
cs.enforce_zero(y_p_lc.clone() + &y_p_lc - c_var); | ||
cs.enforce_zero(LinearCombination::zero() + xx_p + xx_p + xx_p - d_var); | ||
|
||
// lambda * lambda = (2 x_p + x_dbl) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Include comments about the identity case: if lambda == 0 then this constrains x_dbl to 0, and then the constraint below constrains y_dbl to 0.
/// Returns [2] P + Q. | ||
/// | ||
/// Requires P != Q, P != -Q, and neither being the identity. | ||
pub fn double_and_add<CS: ConstraintSystem<C::Base>>( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would name this incomplete_double_and_add
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also include a link to zcash/zcash#3924
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Rename done in #11.
acc = acc.double_and_add(cs, &t)?; | ||
} | ||
|
||
// Compute Acc - T = P + (-T) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Extract this out to an incomplete_add
method. For bonus points, use incomplete_add
in the implementation of complete addition.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done in #11.
cs.enforce_zero(LinearCombination::from(lambda) - h_var); | ||
let y_r_lc = LinearCombination::from(i_var) - &y_p_lc; | ||
|
||
// (x_p - x_r) * k_0 = (x_out - x_r) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
More bonus points: extract this and the next constraint out to a select_point
abstraction, which can also be used in complete addition.
let (one_x, one_y) = one.get_xy().unwrap(); | ||
let (five_x, five_y) = five.get_xy().unwrap(); | ||
println!("five.x = {:?}", five_x); | ||
println!("five.y = {:?}", five_y); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A longer scalar might expose more cases of the algorithm. I suggest keeping this one and then also including a longer scalar with lowest bit zero.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Post-hoc utACK with comments.
No description provided.