Introduce UIntGadget and ComparisonGadget #163

nicholas-mainardi · 2022-01-19T15:31:03Z

This PR addresses issues #149 and #150.

It defines a new trait UIntGadget which defines the functions available for small unsigned integers (up to 128 bits). In particular, the UIntGadget comprises most common gadgets (e.g, EqGadget, AllocGadget) and specific functions like bitiwise and arithmetic operations. This PR introduces also a macro, named impl_uint_gadget, which allows to define a UIntGadget for an unsigned integer given a bit_size and an underlying Rust native type. The macro contains also unit tests that verifies the correctness of the functions implemented for the UIntGadget being defined with the macro. The macro is employed to define UIntGadget for all the Rust native types for unsigned integers, starting from u8 up to u128. This macro mostly addresses issue #149.

Furthermore, this PR introduces also a ComparisonGadget trait, which defines the operations that enable the comparison between gadgets implementing this trait. Two implementations of the ComparisonGadget are provided in this PR:

Comparison between the small unsigned integers gadgets implementing the UIntGadget trait. In particular, the implementation of the ComparisonGadget trait is part of the impl_uint_gadget macro. This implementation addresses issue Optimized arithmetic and comparisons for UInt gadgets #150.
Comparison between FpGadget elements, integrating the comparison functions already introduced in rc/feat/comp_gadget branch; the implementation found in this PR is enriched with additional functions that allow to compare arbitrary field elements, as opposed to the implementation in rc/feat/comp_gadget which requires the field elements to be smaller than (p-1)/2, where p is the modulus of the prime field. Remarkably, the functions added in this PR to deal with arbitrary field elements require only few constraints more than the corresponding ones requiring field elements smaller than (p-1)/2; however, the latter functions are retained in the implementation of the ComparisonGadget because they are still useful in case it is known that the field elements are smaller than (p-1)/2

Lastly, an optimize implementation of the EqGadget is added in this PR for vectors of Booleans. This optimization allows to implement equality/inequality constraints on vectors of Booleans with about 4*len/field_bits constraints over a field for vectors with len bits, as opposed to the existing implementation that requires approximately 2 constraints per bit.

r1cs/gadgets/std/src/bits/boolean.rs

r1cs/gadgets/std/src/eq.rs

r1cs/gadgets/std/src/bits/macros.rs

DanieleDiBenedetto

Amazing work overall !
A small note my side:

Sometimes, especially when enforcing constraints involving Vec, we often write constraints involving explicitly huge LCs instead of Field Elements read from such LCs using the FromBits gadget. While this allows to save some constraints (not much in the end, maybe a couple) it dramatically increase circuit densities, and since our focus, now, is on densities more than number of constraints, this over complication might be unnecessary. Let's discuss this.

r1cs/gadgets/std/src/bits/macros.rs

r1cs/gadgets/std/src/bits/boolean.rs

r1cs/gadgets/std/src/bits/macros.rs

DDT92 · 2022-04-06T14:21:43Z

r1cs/gadgets/std/src/bits/boolean.rs

@@ -631,6 +631,57 @@ impl Boolean {
        }
    }

+    /// Enforce that at least one operand is true, given that bits.len() is less than the size of


The last modifications are ok.
I would modify other parts of the file if it is possible.

In the function kary_and there should be given a short description of what this function is and what is its purpose.

For the functions enforce_smaller_or_equal_than_le it could be good a more detailed description in in-line comments about how it works.

Also conditional_enforce_equal and conditional_enforce_not_equal some inline comments should be given.

DDT92 · 2022-04-06T15:01:29Z

r1cs/gadgets/std/src/bits/boolean.rs

+    /// In addition, the function also returns a flag which specifies if there are no "real" variables
+    /// in the linear combination, that is if the sequence of Booleans comprises all constant values.
+    /// Assumes that `bits` can be packed in a single field element (i.e., bits.len() <= ConstraintF::Params::CAPACITY).
+    pub fn bits_to_linear_combination<'a, ConstraintF:Field, CS: ConstraintSystemAbstract<ConstraintF>>(_cs: CS, bits: impl Iterator<Item=&'a Boolean>) -> (LinearCombination<ConstraintF>, Option<ConstraintF>, bool)


Split the definition of the function in multiple lines.

Ok, I will also run cargo fmt to automatically fix these formatting issues

DDT92 · 2022-04-06T15:17:29Z

r1cs/gadgets/std/src/bits/boolean.rs

@@ -808,7 +892,16 @@ impl<ConstraintF: Field> EqGadget<ConstraintF> for Boolean {
            // 1 - 1 = 0 - 0 = 0
            (Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
            // false != true
-            (Constant(_), Constant(_)) => return Err(SynthesisError::AssignmentMissing),
+            (Constant(_), Constant(_)) => {
+                if should_enforce.is_constant() {


What is the utility of this if?
Why is it not present in conditional_enforce_not_equal.

It was a bugfix for a bug I found out when running unit tests I wrote for UIntGadget. In the previous implementation, if self and other were constants with different values, conditional_enforce_equal would simply return an error, independently from the value of should_enforce flag, which was wrong. Therefore, I modified the code to handle all the possible cases depending on the should_enforce variable.

The bug was triggered in my unit tests only for conditional_enforce_equal function, but I forgot to check if the same bug exists also for conditional_enforce_not_equal, which explains why the code differs between the 2 functions. Thanks to your comment, I found out that the same bug should exist also for conditional_enforce_not_equal, so I will modify the code accordingly

While reviewing the code of conditional_enforce_not_equal to fix the bug for the case when self and other are both constants with the same value, I found out that the constraint enforced at the end of the function was wrong. Therefore I had to modify the constraint, which also required to add the eval_lc function the ConstraintSystemAbstract trait to compute the value of a linear combination of variables in the constraint system. I have also modified the unit test for conditional_enforce_equal to test also the conditional_enforce_not_equal function, which was not tested before, explaining why we missed the incorrect constraint previously enforced in such function

r1cs/gadgets/std/src/bits/macros.rs

DDT92 · 2022-04-07T16:40:57Z

r1cs/gadgets/std/src/bits/macros.rs

+                    let mut value: Option<$native_type> = Some(0);
+                    for (i, el) in bits_iter.enumerate() {
+                        bits.push(*el);
+                        value = match el.get_value() {


What "value" should be?
Should it not be the the integer corresponding to the sequence of bits? It does not seem from the definition.

It is the integer corresponding to the sequence of bits interpreted in little-endian. I will update the description of the function to specify that the bits are considered as the little-endian representation of the integer being constructed

r1cs/gadgets/std/src/bits/macros.rs

DDT92 · 2022-04-08T10:29:56Z

r1cs/gadgets/std/src/bits/macros.rs

+                    // max_overflow_bits are the maximum number of non-zero bits a `Self` element
+                    // can have to be multiplied to another `Self` without overflowing the field
+                    let max_overflow_bits = field_bits - $bit_size;
+                    // given a base b = 2^m, where m=2^max_overflow_bits, the `other` operand is


m = max_overflow_bits

Ok, thanks for pointing it out

DDT92 · 2022-04-12T09:44:51Z

r1cs/gadgets/std/src/bits/macros.rs

+                fn mulmany<CS>(mut cs: CS, operands: &[Self]) -> Result<Self, SynthesisError>
+                where CS: ConstraintSystemAbstract<ConstraintF> {
+                    let num_operands = operands.len();
+                    let field_bits = (ConstraintF::Params::CAPACITY) as usize;


Better to call it capacity. field_bits reminds more MODULUS_BITS.

Ok, I will rename it, also in other functions

DDT92 · 2022-04-13T12:41:35Z

r1cs/gadgets/std/src/bits/macros.rs

+                    test_uint_gadget_value(result_value, &result_var, "result correctness");
+                    assert!(cs.is_satisfied());
+
+                    // negative test


What does it precisely mean? Can you provide a description of what are you testing here?

I will add more details to the comment, thanks

DDT92 · 2022-04-13T12:42:11Z

r1cs/gadgets/std/src/bits/macros.rs

+                    assert!(cs.is_satisfied());
+
+
+                    if MAX_NUM_OPERANDS >= 2 { // negative tests are skipped if if double and add must be used because the field is too small


Same as above

I will add more details to the comment, thanks

DDT92 · 2022-04-13T13:15:00Z

r1cs/gadgets/std/src/bits/macros.rs

+                    let mut is_overflowing = false;
+                    let result_value: $native_type = operand_values.iter().cloned().reduce(|a,b| {
+                        let (updated_sum, overflow) = a.overflowing_add(b);
+                        is_overflowing |= overflow;


why don't you define directly
let (updated_sum, is_overflowing) = a.overflowing_add(b); ?

With your proposal I think that is_overflowing will be true only if the last addition overflows. However, the addition of all the operands does not overflow only if none of the additions between the accumulator and each operand overflows. That's why I compute is_overflowing as the OR of all the overflow flags of each addition. Does it look sound to you?

DDT92 · 2022-04-13T14:24:33Z

r1cs/gadgets/std/src/bits/macros.rs

+                    const NUM_OPERANDS: usize = MAX_NUM_OPERANDS*2+5;
+
+                    // we want to test a case when the operands must be split in multiple chunks
+                    assert!(NUM_OPERANDS > MAX_NUM_OPERANDS);


What is the need for this assert?

It ensures that the test is run with a number of operands that will force the mulmany operation to process the operands by splitting them in multiple chunks, as otherwise the result would overflow the field size. Although the assertion may seem redundant given that it is performed over constant values, I added it to avoid that possible future modifications of the parameters of the test (e.g., the field being used) will no longer ensure that operands are split in multiple chunks

DDT92 · 2022-04-14T10:32:38Z

r1cs/gadgets/std/src/eq.rs

+        let len = self.len();
+        if field_bits < len {
+            // In this case we cannot split in chunks here, as it's not true that if two bit vectors
+            // are not equal, then they are not equal chunkwise too. Therefore, we


I do not understand this. The "chunks" are just a partition of the original bit of vectors. How is it possible that the chunks are equal but the original sequence of bits is different?

I am sorry, probably the comment wasn't clear enough. I meant that there may be corresponding chunks which are equal even if the bit vectors differ (i.e., self and other may differ in only one chunk). I will modify the comment as follows to make it clearer:

// In this case we cannot split `self` and `other` in chunks here and enforce that each // pair of chunks differ, as it's not true that if two bit vectors // are not equal, then all their corresponding chunks differ.`

r1cs/gadgets/std/src/fields/cmp.rs

…force_eq for Boolean

DanieleDiBenedetto · 2022-05-05T12:55:25Z

r1cs/gadgets/crypto/src/prf/sha256.rs

@@ -73,15 +78,17 @@ where
        cur = sha256_compression_function(cs.ns(|| format!("block {}", i)), block, &cur)?;
    }

-    Ok(cur.into_iter().flat_map(|e| e.into_bits_be()).collect())
+    //Ok(cur.into_iter().enumerate().map(|(i,e)| e.to_bits(cs.ns(|| format!("unpack word {} of sha256 digest", i)))).collect::<Result<Vec<_>, SynthesisError>>()?.into_iter().flat_map(|e| e).collect())


Remove commented code

…oduce-UInt-gadget

nicholas-mainardi marked this pull request as ready for review January 20, 2022 08:42

This was linked to issues Feb 4, 2022

Import macro-generated UInt gadgets from arkworks #149

Open

Optimized arithmetic and comparisons for UInt gadgets #150

Open

DanieleDiBenedetto requested review from DanieleDiBenedetto and UlrichHaboeck75 February 10, 2022 14:46

DanieleDiBenedetto requested changes Feb 14, 2022

View reviewed changes

r1cs/gadgets/std/src/bits/macros.rs Outdated Show resolved Hide resolved

r1cs/gadgets/std/src/bits/macros.rs Show resolved Hide resolved

DanieleDiBenedetto requested changes Mar 21, 2022

View reviewed changes

r1cs/gadgets/std/src/bits/boolean.rs Outdated Show resolved Hide resolved

r1cs/gadgets/std/src/bits/macros.rs Outdated Show resolved Hide resolved

DanieleDiBenedetto approved these changes Mar 25, 2022

View reviewed changes

DanieleDiBenedetto requested review from DDT92 and removed request for UlrichHaboeck75 March 30, 2022 08:20

DDT92 reviewed Apr 6, 2022

View reviewed changes

DDT92 reviewed Apr 13, 2022

View reviewed changes

DDT92 reviewed Apr 14, 2022

View reviewed changes

DDT92 approved these changes Apr 27, 2022

View reviewed changes

nicholas-mainardi and others added 15 commits May 5, 2022 11:20

UIntGadget trait + macro implementation

9799ed9

Define cmp gadget + implementation for FpGadget

997bd8f

functions to compare arbitrary field elements

64756f4

Implement ComparisonGadget and sub for UIntGadet

f78a28a

Fix security issue on is_smaller_than + add comments

856f5be

Implement uint16/128 + deal with field too small for mul

2e126d5

Optimize EqGadget for vector of bits

4fc7f89

Fix non-native tests

3b0858f

deleting files with old implementations of uint8. uint32 and uint64

150cf1f

Add conditional_enforce_cmp to comparison gadget + fix conditional_en…

5dec26f

…force_eq for Boolean

Address requested changes in PR

7a293f8

merge to little-endian bits functions

d60b85b

Move rotate functions to UIntGadget

a4eab00

remove modules for each uint implementation

2cfea88

Fix conditional_enforce_not_equal for boolean + improve unit test

b1649ea

nicholas-mainardi added 2 commits May 5, 2022 12:37

Addressing changes

e50670f

Optimize comparison for FpGadget

4661c20

DanieleDiBenedetto reviewed May 5, 2022

View reviewed changes

nicholas-mainardi added 2 commits May 9, 2022 16:58

Fix issues after rebase

8ea676b

Merge branch 'add-little-endian-functions-to-ToBits-gadget' into intr…

81811bc

…oduce-UInt-gadget

nicholas-mainardi force-pushed the introduce-UInt-gadget branch from 7a8abe2 to 81811bc Compare May 9, 2022 17:08

nicholas-mainardi changed the base branch from refactor_ginger_monorepo to add-little-endian-functions-to-ToBits-gadget May 9, 2022 17:10

Merge branch 'fix-cmp-with-eq-implementation' into introduce-UInt-gadget

b3b2d13

nicholas-mainardi changed the base branch from add-little-endian-functions-to-ToBits-gadget to fix-cmp-with-eq-implementation May 10, 2022 09:02

DanieleDiBenedetto closed this Feb 13, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Introduce UIntGadget and ComparisonGadget #163

Introduce UIntGadget and ComparisonGadget #163

nicholas-mainardi commented Jan 19, 2022

DanieleDiBenedetto left a comment

DDT92 Apr 6, 2022

nicholas-mainardi Apr 22, 2022

DDT92 Apr 6, 2022

nicholas-mainardi Apr 20, 2022

DDT92 Apr 6, 2022

nicholas-mainardi Apr 20, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 7, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 8, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 12, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 13, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 13, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 13, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 13, 2022

nicholas-mainardi Apr 21, 2022

DDT92 Apr 14, 2022

nicholas-mainardi Apr 21, 2022

DanieleDiBenedetto May 5, 2022

		assert!(cs.is_satisfied());


		if MAX_NUM_OPERANDS >= 2 { // negative tests are skipped if if double and add must be used because the field is too small

Introduce UIntGadget and ComparisonGadget #163

Introduce UIntGadget and ComparisonGadget #163

Conversation

nicholas-mainardi commented Jan 19, 2022

DanieleDiBenedetto 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

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