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

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

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

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?

We based our torus implementation on franklin-crypto. There with flag safe are following methods:

square

mul

pow

compress

mul

We did use what in franklin-crypto is marked as unsafe due to several reasons:

mathematically, as you mentioned, "unsafe" version is actually quite safe

computationally cheaper

easier to use and maintain from the engineering perspective

pow

This one has safe flag only because square has one. Below I'll explain why we didn't use it there, thus it is not added here.

square and compress safeness:

These two actually have different taste of what unsafe flag is switching. While in square we potentially divide by zero, in compress, we at first make an enforcement that there won't be one.

overall

In production settings, we use safe version. I am struggling to imagine where the unsafe variant may be utilized, therefore we favoured the implementations of safe methods.

The flag was added for compress because it is still quite safe compared to others, and we thought that it may be still usable in some production settings.

Therefore, if we desire to achieve some homogeneity of the codebase, we better to simply remove unsafe version from compress method, or, if this has some potential, leave it in there.

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

In case of multiplication, we ensure that g + g' cannot be zero due to algebraic impossibility of that. Here, on the other hand, it is completely possible that g will be zero, leading to division by that. That's why we need the check; I mean, in code, the gamma/g must be masked to zero, if g is zero.

This is particularly what is happening in franklin-crypto:

https://github.com/matter-labs/franklin-crypto/blob/finalization/src/plonk/circuit/bigint/algebraic_torus.rs#L254

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

AFAIK, inversion in torus is a fairly cheap operation, since it's additive negation −g in Fq6 maps to the multiplicative inverse of the corresponding element in Fq12. So, since we make inner negation there is no optimizational trick like this one.

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

Cannot quite understand what do you mean here, can you please clarify?

If you are talking about leveraging the same approach as in U256, I would rather not do that because:

We don't actually use types u1024, u2048 and u4096. These were planned for modexp, but the decision was to go with u256. Since we've spent some time on these implementations, they were left.

There is enhanced complexity compared to U256, because primitive_types crate, from which we take the functionality for witnesses is limited by max U512 type, meaning that in these bigger types, there would be need to build complex compositional logics.

Summarizing, there is no particular benefit to spend time on building extra optimizations for unused things, which as well may introduce additional space for error.

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;

Fixed second point. I am not particularly sure what to change in 3-rd and 4-th, can you please explain wdym?

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

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

No enforce_equal is implemented for any uint gadgets unfortunately

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

I see that it is also used in u16 and u32 implementations. However, can't use it in u256 directly because max supported width for this gate is 32. It is though used under the hood in UInt256::overflowing_sub -> UInt32::overflowing_sub_with_borrow_in, so I suppose the optimization via this gate already holds 🙂

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

…e_affine

…odexp

… of extensions

…onNativeFieldOverU16

… of cs

NikitaMasych · 2024-12-11T12:04:33Z

Hey there, @Fitznik !

I've marked as resolved all undisputable issues, which I resolved in code, there are left a few ones which I need your agreement/clarification

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 force-pushed the dl-precompiles branch from 8d65413 to 778b95c Compare November 15, 2024 12:31

Fitznik reviewed Nov 15, 2024

View reviewed changes

crates/boojum/src/gadgets/u256/mod.rs Outdated Show resolved Hide resolved

NikitaMasych force-pushed the dl-precompiles branch from 778b95c to da49f64 Compare December 5, 2024 11:53

NikitaMasych added 18 commits December 11, 2024 13:47

chore: added .idea to .gitignore

288b98f

feat(boojum): added implementations to non_native_field gadget

8031e50

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

c3307ec

…e_affine

feat(boojum): added HardexpCompatible trait

e95d6cd

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

379e662

…odexp

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

324e08b

feat(boojum): added tower of extensions

9dcf895

feat(boojum): added WitnessVarLengthEncodable implementation to tower…

c92a0c4

… of extensions

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

5e100aa

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

80f417f

…onNativeFieldOverU16

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

54c58a5

… of cs

feat: added set method to FFProxyValue

dd45a88

feat(boojum): optimized modmul for u256

7c7c016

feat: implemented cast_into_source

6c27bb6

refactor(boojum): modmul for UInt256 - better conversions

2e7c3ef

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

a3ae103

fix: correct m > r constraint for zero mod

667a27d

fix: post-review fixes

a66be00

NikitaMasych force-pushed the dl-precompiles branch from 6af6df5 to a66be00 Compare December 11, 2024 11:47

feat: added unsafe convertion projective -> affine

75bfb47

feat: added mixed point add with passage of inf flag

936cf2d

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

NikitaMasych Dec 5, 2024

Fitznik Oct 30, 2024

Fitznik Oct 30, 2024

NikitaMasych Dec 5, 2024

Fitznik Oct 30, 2024

NikitaMasych Dec 5, 2024

Fitznik Oct 30, 2024

NikitaMasych Dec 10, 2024

NikitaMasych Dec 10, 2024

Fitznik Oct 30, 2024

NikitaMasych Dec 11, 2024

Fitznik Oct 30, 2024

NikitaMasych Dec 10, 2024

Fitznik Oct 30, 2024

NikitaMasych Dec 11, 2024

NikitaMasych commented Dec 11, 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

mul

pow

square and compress safeness:

overall

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

Choose a reason for hiding this comment

NikitaMasych commented Dec 11, 2024

NikitaMasych commented Sep 5, 2024 •

edited

Loading

`mul`

`pow`

`square` and `compress` safeness: