feat: end-to-end modexp, ecadd, ecmul and ecpairing #22
Conversation
NikitaMasych
force-pushed
the
dl-precompiles
branch
from
6806fe4
to
31d01c1
Compare
NikitaMasych
force-pushed
the
dl-precompiles
branch
from
b0d43be
to
88349a3
Compare
NikitaMasych
force-pushed
the
dl-precompiles
branch
2 times, most recently
from
ca1c9a0
to
7e89898
Compare
There was a problem hiding this comment.
There are many places in the code where it can be optimized. I have a question about the tests; they check whether the witnesses are correctly calculated but do not check whether the constraints are satisfied. Please add this check (check_if_satisfied). This function is an important indicator of whether or not the circuits are working
| ) -> ((NN, NN), Boolean<F>) { | ||
| let params = self.x.get_params().clone(); | ||
| let is_point_at_infty = NN::is_zero(&mut self.z, cs); | ||
|
|
| let rhs = rhs.add(cs, &mut gamma); | ||
|
|
||
| let zero = Fq6::zero(cs, params); | ||
| let is_zero_sum = sum.is_zero(cs); |
There was a problem hiding this comment.
I assume you got this code from our old version of franklin-crypto. There are two versions, safe and not. This code was taken from an unsafe version. The point is that we do not check that the sum of g1 and g2 is zero because the constraint guarantees that malicious will not find such g2 = -g1 that won't be the root of gamma. The unsafe version was made on the assumption to reduce constraints ( that means that we are pretty sure that this is not underconstrained)
| let params = f.get_params(); | ||
| let mut c0 = f.c0.clone(); | ||
| let mut c1 = f.c1.clone(); | ||
|
|
There was a problem hiding this comment.
Why do you use two versions here but didn't implement two versions for the other code?
| // rhs = g == 0 ? zero : gamma | ||
| let zero = Fq6::zero(cs, params); | ||
| let gamma = Fq6::gamma(cs, params); | ||
| let is_zero_g = self.encoding.is_zero(cs); |
There was a problem hiding this comment.
I mean, it isn't possible that gamma could be zero
| pub fn inverse<CS>(&mut self, cs: &mut CS) -> Self | ||
| where | ||
| CS: ConstraintSystem<F>, | ||
| { |
There was a problem hiding this comment.
I think this version will be cheaper if you compute inv like a witness and prove a*a_inv = 1
| Self::from_le_bytes(cs, bytes) | ||
| } | ||
|
|
||
| /// Finds the result of multiplying `self` by `other` mod `modulo`. |
| @@ -351,6 +358,64 @@ impl<F: SmallField> UInt256<F> { | |||
| }); | |||
| Self::from_le_bytes(cs, bytes) | |||
| } | |||
|
|
|||
| /// Finds the result of multiplying `self` by `other` mod `modulo`. | |||
| pub fn modmul<CS: ConstraintSystem<F>>( | |||
There was a problem hiding this comment.
This function has trouble with generating witnesses.
2. You check that the module is zero, which is exceptional; you should do this through the constraint is_zero.
3. You did this wrong first; it creates many inefficiencies because you perform additional range checks on the variables that were already checked.
4. It looks like you didn't wrap properly carry
// let mut carry = (q[0] * p[0] + r[0] - a[0] * b[0]) >> 16;
// carry = (q[1] * p[0] + q[0] * p[1] + r[1] - a[1] * b[0] - a[0] * b[0] + carry) >> 16;
|
|
||
| let rhs = q.widening_mul(cs, &modulo, 8, 8); | ||
| let r_u512 = r.to_u512(cs); | ||
| let (rhs, overflow) = rhs.overflowing_add(cs, &r_u512); |
There was a problem hiding this comment.
We don't need to check overflow because this m_ge_than_r is doing this
| let (rhs, overflow) = rhs.overflowing_add(cs, &r_u512); | ||
| Boolean::enforce_equal(cs, &overflow, &bool_false); | ||
|
|
||
| let are_equal = UInt512::equals(cs, &lhs, &rhs); |
There was a problem hiding this comment.
Dont do this twice; write enforce_equal for UInt512
|
|
||
| /// Returns `true` if `self >= other`, and `false` otherwise. | ||
| /// Here, `self` and `other` are represented as `UInt512<F>` and `UInt256<F>` respectively. | ||
| pub fn geq_than_u256<CS>(&self, cs: &mut CS, other: &UInt256<F>) -> Boolean<F> |
There was a problem hiding this comment.
I think here could be optimization for this; we have a special type of gate UIntXAddGate
see u16_long_subtraction_noborrow_must_borrow
…onNativeFieldOverU16
NikitaMasych
force-pushed
the
dl-precompiles
branch
from
8d65413
to
778b95c
Compare
What?
Implementation of
modexp,ecadd,ecmulandecpairingprecompiles as circuits.Previous PR
Basically all changes are made to
boojumcrate's gadgets. Previous PR for deprecated repository which has been reviewed:era-boojum
Homogeneity with previous PR
Code has certain changes apart from contained in previous PR such as caused by rebasing and noticing missed problems.