feat: end-to-end modexp, ecadd, ecmul and ecpairing #22

NikitaMasych · 2024-09-05T07:11:05Z

What?

Implementation of modexp, ecadd, ecmul and ecpairing precompiles as circuits.

Previous PR

Basically all changes are made to boojum crate'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.

Fitznik

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

Fitznik · 2024-10-30T00:47:05Z

crates/boojum/src/gadgets/curves/sw_projective/extended.rs

+    ) -> ((NN, NN), Boolean<F>) {
+        let params = self.x.get_params().clone();
+        let is_point_at_infty = NN::is_zero(&mut self.z, cs);
+


You can normalize once

Fitznik · 2024-10-30T01:00:35Z

crates/boojum/src/gadgets/tower_extension/algebraic_torus.rs

+        let rhs = rhs.add(cs, &mut gamma);
+
+        let zero = Fq6::zero(cs, params);
+        let is_zero_sum = sum.is_zero(cs);


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)

Fitznik · 2024-10-30T01:05:13Z

crates/boojum/src/gadgets/tower_extension/algebraic_torus.rs

+        let params = f.get_params();
+        let mut c0 = f.c0.clone();
+        let mut c1 = f.c1.clone();
+


Why do you use two versions here but didn't implement two versions for the other code?

Fitznik · 2024-10-30T01:08:42Z

crates/boojum/src/gadgets/tower_extension/algebraic_torus.rs

+        // 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);


The same is mention here

I mean, it isn't possible that gamma could be zero

Fitznik · 2024-10-30T01:14:20Z

crates/boojum/src/gadgets/tower_extension/fq2.rs

+    pub fn inverse<CS>(&mut self, cs: &mut CS) -> Self
+    where
+        CS: ConstraintSystem<F>,
+    {


I think this version will be cheaper if you compute inv like a witness and prove a*a_inv = 1

Fitznik · 2024-10-30T01:31:55Z

crates/boojum/src/gadgets/u2048/mod.rs

+        Self::from_le_bytes(cs, bytes)
+    }
+
+    /// Finds the result of multiplying `self` by `other` mod `modulo`.


do mul through the ab = qP + rem

Fitznik · 2024-10-30T01:40:23Z

crates/boojum/src/gadgets/u256/mod.rs

@@ -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>>(


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;

Fitznik · 2024-10-30T01:41:27Z

crates/boojum/src/gadgets/u256/mod.rs

+
+        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);


We don't need to check overflow because this m_ge_than_r is doing this

Fitznik · 2024-10-30T01:43:15Z

crates/boojum/src/gadgets/u256/mod.rs

+        let (rhs, overflow) = rhs.overflowing_add(cs, &r_u512);
+        Boolean::enforce_equal(cs, &overflow, &bool_false);
+
+        let are_equal = UInt512::equals(cs, &lhs, &rhs);


Dont do this twice; write enforce_equal for UInt512

Fitznik · 2024-10-30T01:45:29Z

crates/boojum/src/gadgets/u512/mod.rs

+
+    /// 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>


I think here could be optimization for this; we have a special type of gate UIntXAddGate
see u16_long_subtraction_noborrow_must_borrow

…e_affine

…odexp

… of extensions

…onNativeFieldOverU16

… of cs

Fitznik · 2024-11-15T20:09:52Z

crates/boojum/src/gadgets/u256/mod.rs

@@ -394,19 +394,21 @@ impl<F: SmallField> UInt256<F> {
        let q = UInt256::allocate(cs, q);
        let r = UInt256::allocate(cs, r);

-        let (_, m_greater_than_r) = r.overflowing_sub(cs, &modulo);
+        let mod_is_zero = Boolean::allocate(cs, m.is_zero());


you can't do this. Allocate just m and then check with constraint is_zero this 'm'

NikitaMasych force-pushed the dl-precompiles branch from 6806fe4 to 31d01c1 Compare September 11, 2024 12:32

NikitaMasych force-pushed the dl-precompiles branch from b0d43be to 88349a3 Compare October 2, 2024 22:10

NikitaMasych force-pushed the dl-precompiles branch 2 times, most recently from ca1c9a0 to 7e89898 Compare October 11, 2024 14:55

NikitaMasych marked this pull request as ready for review October 17, 2024 12:52

Fitznik reviewed Oct 30, 2024

View reviewed changes

NikitaMasych added 17 commits November 15, 2024 14:31

chore: added .idea to .gitignore

18d120b

feat(boojum): added implementations to non_native_field gadget

157988d

feat(boojum): curves: added extended sw projective, implement zeroabl…

3462d63

…e_affine

feat(boojum): added HardexpCompatible trait

58ad993

feat(boojum): add fundamental implementations for u256 and u512 for m…

51ceade

…odexp

feat(boojum): added u1024, u2048, u4096 as gadgets

a04390c

feat(boojum): added tower of extensions

12757c4

feat(boojum): added WitnessVarLengthEncodable implementation to tower…

5d55450

… of extensions

fix(boojum): added inf point handling in add/sub mixed for sw_projective

81e94b5

feat(boojum): added CSAllocatable inner methods implementations for N…

f9fd920

…onNativeFieldOverU16

fix(boojum): fixed frobenius map for non-witness evaluateable configs…

5a40e41

… of cs

feat: added set method to FFProxyValue

ad810f6

feat(boojum): optimized modmul for u256

b62d71a

feat: implemented cast_into_source

fc378c3

refactor(boojum): modmul for UInt256 - better conversions

308c34c

fix(boojum): handling zero mod in modmul for UInt256

a99ba27

fix: correct m > r constraint for zero mod

778b95c

NikitaMasych force-pushed the dl-precompiles branch from 8d65413 to 778b95c Compare November 15, 2024 12:31

Fitznik reviewed Nov 15, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: end-to-end modexp, ecadd, ecmul and ecpairing #22

feat: end-to-end modexp, ecadd, ecmul and ecpairing #22

NikitaMasych commented Sep 5, 2024 •

edited

Loading

Fitznik left a comment

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

Fitznik Nov 15, 2024

feat: end-to-end modexp, ecadd, ecmul and ecpairing #22

Are you sure you want to change the base?

feat: end-to-end modexp, ecadd, ecmul and ecpairing #22

Conversation

NikitaMasych commented Sep 5, 2024 • edited Loading

What?

Previous PR

Homogeneity with previous PR

Fitznik left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikitaMasych commented Sep 5, 2024 •

edited

Loading