Fix chunk is padding circuit

aggregator/README.md

@@ -182,7 +182,7 @@ for i in 1 ... n:
     if is_padding:
         chunk_i.prev_state_root == chunk_i.post_state_root 
         chunk_i.withdraw_root == chunk_{i-1}.withdraw_root
-        chunk_i.data_hash == [0u8; 32]
+        chunk_i.data_hash == keccak("")
 ```
 7. chunk[i]'s data_hash len is `0` when chunk[i] is padded
 

aggregator/src/aggregation/rlc/gates.rs

@@ -28,6 +28,12 @@ impl RlcConfig {
             5,
             || Value::known(Fr::from(32)),
         )?;
+        region.assign_fixed(
+            || "const two to thirty two",
+            self.fixed,
+            6,
+            || Value::known(Fr::from(1 << 32)),
+        )?;
         Ok(())
     }
 
@@ -85,6 +91,15 @@ impl RlcConfig {
         }
     }
 
+    #[inline]
+    pub(crate) fn two_to_thirty_two_cell(&self, region_index: RegionIndex) -> Cell {
+        Cell {
+            region_index,
+            row_offset: 6,
+            column: self.fixed.into(),
+        }
+    }
+
     pub(crate) fn load_private(
         &self,
         region: &mut Region<Fr>,
@@ -399,7 +414,7 @@ impl RlcConfig {
     }
 
     // return a boolean if a is smaller than b
-    // requires that both a and b are smallish
+    // requires that both a and b are less than 32 bits
     pub(crate) fn is_smaller_than(
         &self,
         region: &mut Region<Fr>,
@@ -408,11 +423,18 @@ impl RlcConfig {
         offset: &mut usize,
     ) -> Result<AssignedCell<Fr, Fr>, Error> {
         // when a and b are both small (as in our use case)
-        // if a < b, (a-b) will under flow and the highest bit of (a-b) be one
-        // else,  the highest bit of (a-b) be zero
-        let sub = self.sub(region, a, b, offset)?;
-        let bits = self.decomposition(region, &sub, offset)?;
-        Ok(bits[253].clone())
+        // if a >= b, c = 2^32 + (a-b) will be >= 2^32
+        // we bit decompose c and check the 33-th bit
+        let two_to_thirty_two = self.load_private(region, &Fr::from(1 << 32), offset)?;
+        let two_to_thirty_two_cell =
+            self.two_to_thirty_two_cell(two_to_thirty_two.cell().region_index);
+        region.constrain_equal(two_to_thirty_two_cell, two_to_thirty_two.cell())?;
+
+        let ca = self.add(region, &two_to_thirty_two, a, offset)?;
+        let c = self.sub(region, &ca, b, offset)?;
+        let bits = self.decomposition(region, &c, offset)?;
+        let res = self.not(region, &bits[32], offset)?;
+        Ok(res)
     }
 }
 #[inline]

aggregator/src/core.rs

@@ -733,10 +733,19 @@ pub(crate) fn chunk_is_valid(
     offset: &mut usize,
 ) -> Result<[AssignedCell<Fr, Fr>; MAX_AGG_SNARKS], halo2_proofs::plonk::Error> {
     let mut res = vec![];
-
-    for i in 0..MAX_AGG_SNARKS {
-        let value = rlc_config.load_private(region, &Fr::from(i as u64), offset)?;
-        let is_valid = rlc_config.is_smaller_than(region, &value, num_of_valid_chunks, offset)?;
+    let mut cur_index = rlc_config.load_private(region, &Fr::zero(), offset)?;
+    let zero_cell = rlc_config.zero_cell(cur_index.cell().region_index);
+    region.constrain_equal(cur_index.cell(), zero_cell)?;
+    let one = rlc_config.load_private(region, &Fr::one(), offset)?;
+    let one_cell = rlc_config.one_cell(one.cell().region_index);
+    region.constrain_equal(one.cell(), one_cell)?;
+
+    let is_valid = rlc_config.is_smaller_than(region, &cur_index, num_of_valid_chunks, offset)?;
+    res.push(is_valid);
+    for _ in 0..MAX_AGG_SNARKS - 1 {
+        cur_index = rlc_config.add(region, &cur_index, &one, offset)?;
+        let is_valid =
+            rlc_config.is_smaller_than(region, &cur_index, num_of_valid_chunks, offset)?;
         res.push(is_valid);
     }
     // constrain the chunks are ordered with real ones at the beginning. that is,

aggregator/src/tests/rlc/gates.rs

@@ -146,8 +146,8 @@ impl Circuit<Fr> for ArithTestCircuit {
                 // unit test: is smaller than
                 {
                     for _ in 0..10 {
-                        let a = Fr::from(rng.next_u64());
-                        let b = Fr::from(rng.next_u64());
+                        let a = Fr::from(rng.next_u32() as u64);
+                        let b = Fr::from(rng.next_u32() as u64);
                         let c = if a < b { Fr::one() } else { Fr::zero() };
                         let a = config.load_private(&mut region, &a, &mut offset)?;
                         let b = config.load_private(&mut region, &b, &mut offset)?;
@@ -157,7 +157,7 @@ impl Circuit<Fr> for ArithTestCircuit {
                     }
 
                     // equality check
-                    let a = Fr::from(rng.next_u64());
+                    let a = Fr::from(rng.next_u32() as u64);
                     let b = a;
                     let c = Fr::zero();
                     let a = config.load_private(&mut region, &a, &mut offset)?;