Allowing for different len in fibosq (#145)

* Allowing for different len in fibosq * Module to N = 14 --------- Co-authored-by: RogerTaule <[email protected]>
0xPolygonHermez · Jan 17, 2025 · 47f48e0 · 47f48e0
1 parent 8b6d35c
commit 47f48e0
Show file tree

Hide file tree

Showing 6 changed files with 72 additions and 29 deletions.
diff --git a/examples/fibonacci-square/README.md b/examples/fibonacci-square/README.md
@@ -134,6 +134,8 @@ cargo run --bin proofman-cli prove \
 
 ### 2.9 All at once
 
+Without recursion:
+
 ```bash
 node ../pil2-compiler/src/pil.js ./examples/fibonacci-square/pil/build.pil \
      -I ./pil2-components/lib/std/pil \
@@ -156,3 +158,29 @@ node ../pil2-compiler/src/pil.js ./examples/fibonacci-square/pil/build.pil \
      --public-inputs examples/fibonacci-square/src/inputs.json \
      --output-dir examples/fibonacci-square/build/proofs
 ```
+
+With recursion:
+
+```bash
+node ../pil2-compiler/src/pil.js ./examples/fibonacci-square/pil/build.pil \
+     -I ./pil2-components/lib/std/pil \
+     -o ./examples/fibonacci-square/pil/build.pilout \
+&& node ../pil2-proofman-js/src/main_setup.js \
+     -a ./examples/fibonacci-square/pil/build.pilout \
+     -b ./examples/fibonacci-square/build \
+     -t ./pil2-stark/build/bctree \
+     -r \
+&& cargo run --bin proofman-cli pil-helpers \
+     --pilout ./examples/fibonacci-square/pil/build.pilout \
+     --path ./examples/fibonacci-square/src -o \
+&& cargo build \
+&& cargo run --bin proofman-cli verify-constraints \
+     --witness-lib ./target/debug/libfibonacci_square.so \
+     --proving-key examples/fibonacci-square/build/provingKey/ \
+     --public-inputs examples/fibonacci-square/src/inputs.json \
+&& cargo run --bin proofman-cli prove \
+     --witness-lib ./target/debug/libfibonacci_square.so \
+     --proving-key examples/fibonacci-square/build/provingKey/ \
+     --public-inputs examples/fibonacci-square/src/inputs.json \
+     --output-dir examples/fibonacci-square/build/proofs -a \
+```
diff --git a/examples/fibonacci-square/pil/build.pil b/examples/fibonacci-square/pil/build.pil
@@ -1,9 +1,9 @@
 require "fibonaccisq.pil"
 require "module.pil"
 
-// Notice that these two components have a one-to-one reationship, so they must have the same number of rows
-// for them to make sense and for the relationshhip to be satisfied
+// Notice that these two components have a one-to-one reationship
+// As they have a different trace length, we need to create multiple module instances
 airgroup FibonacciSquare {
-    FibonacciSquare(N: 2**10);
-    Module(N: 2**10);
+    FibonacciSquare(N: 2**18);
+    Module(N: 2**14);
 }
diff --git a/examples/fibonacci-square/pil/module.pil b/examples/fibonacci-square/pil/module.pil
@@ -6,14 +6,18 @@ public module;
 
 airtemplate Module(const int N = 2**8) {
 
-    col fixed LN = [0...,1];
+    col fixed SEGMENT_LN = [0...,1];
     col witness x, q, x_mod;
 
+    airval last_segment;
+    last_segment * (1 - last_segment) === 0;
+
     x === q * module + x_mod;
 
     // Ensure that 0 <= x_mod < module < PRIME <--> 0 < module - x_mod <--> module - x_mod <= module
     range_check(module - x_mod, 1, 2**8-1);
     // NOTE: The 2**8-1 is used for simplicity. Moreover, for the shake of security, module should be limited to 2**8-1 by the verifier
 
-    permutation_proves(MODULE_ID, [x, x_mod], 1 - LN);
+    // The permutation should not be applied on the last row of the last segment
+    permutation_proves(MODULE_ID, [x, x_mod], sel: 1 - SEGMENT_LN * last_segment);
 }
diff --git a/examples/fibonacci-square/src/debug.json b/examples/fibonacci-square/src/debug.json
@@ -1,3 +1,3 @@
 {
     "constraints": [{ "airgroup": "FibonacciSquare", "air_ids": [ { "air": "FibonacciSquare", "instance_ids": [ { "instance_id": 0, "constraints": [0, 2, 4] },  {"instance_id": 2 }] }, { "air": "Module"}] }]
-}
+}
diff --git a/examples/fibonacci-square/src/module.rs b/examples/fibonacci-square/src/module.rs
@@ -6,7 +6,7 @@ use pil_std_lib::Std;
 use p3_field::{AbstractField, PrimeField64};
 use num_bigint::BigInt;
 
-use crate::{BuildPublicValues, ModuleTrace};
+use crate::{BuildPublicValues, ModuleTrace, ModuleAirValues};
 
 pub struct Module<F: PrimeField64> {
     inputs: Mutex<Vec<(u64, u64)>>,
@@ -38,39 +38,46 @@ impl<F: PrimeField64 + AbstractField + Copy> WitnessComponent<F> for Module<F> {
         let publics = BuildPublicValues::from_vec_guard(pctx.get_publics());
         let module = F::as_canonical_u64(&publics.module);
 
-        let mut trace = ModuleTrace::new_zeroes();
-
         //range_check(colu: mod - x_mod, min: 1, max: 2**8-1);
         let range = self.std_lib.get_range(BigInt::from(1), BigInt::from((1 << 8) - 1), None);
 
         let inputs = self.inputs.lock().unwrap();
 
-        let inputs_len = inputs.len();
+        let num_rows = ModuleTrace::<F>::NUM_ROWS;
+        let num_instances = inputs.len().div_ceil(num_rows);
 
-        let mut x_mods = Vec::new();
+        for j in 0..num_instances {
+            let mut trace = ModuleTrace::new_zeroes();
 
-        for (i, input) in inputs.iter().enumerate() {
-            let x = input.0;
-            let q = x / module;
-            let x_mod = input.1;
+            let inputs_slice = if j < num_instances - 1 {
+                inputs[j * num_rows..(j + 1) * num_rows].to_vec()
+            } else {
+                inputs[j * num_rows..].to_vec()
+            };
 
-            trace[i].x = F::from_canonical_u64(x);
-            trace[i].q = F::from_canonical_u64(q);
-            trace[i].x_mod = F::from_canonical_u64(x_mod);
-            x_mods.push(x_mod);
-        }
+            for (i, input) in inputs_slice.iter().enumerate() {
+                let x = input.0;
+                let q = x / module;
+                let x_mod = input.1;
+
+                trace[i].x = F::from_canonical_u64(x);
+                trace[i].q = F::from_canonical_u64(q);
+                trace[i].x_mod = F::from_canonical_u64(x_mod);
 
-        let air_instance = AirInstance::new_from_trace(FromTrace::new(&mut trace));
-        let is_mine = add_air_instance::<F>(air_instance, pctx.clone());
-        if is_mine {
-            for x_mod in x_mods.iter() {
+                // Check if x_mod is in the range
                 self.std_lib.range_check(F::from_canonical_u64(module - x_mod), F::one(), range);
             }
 
             // Trivial range check for the remaining rows
-            for _ in inputs_len..trace.num_rows() {
+            for _ in inputs_slice.len()..trace.num_rows() {
                 self.std_lib.range_check(F::from_canonical_u64(module), F::one(), range);
             }
+
+            let mut air_values = ModuleAirValues::<F>::new();
+            air_values.last_segment = F::from_bool(j == num_instances - 1);
+
+            let air_instance = AirInstance::new_from_trace(FromTrace::new(&mut trace).with_air_values(&mut air_values));
+            add_air_instance::<F>(air_instance, pctx.clone());
         }
     }
 }
diff --git a/examples/fibonacci-square/src/pil_helpers/traces.rs b/examples/fibonacci-square/src/pil_helpers/traces.rs
@@ -52,24 +52,28 @@ values!(BuildProofValues<F> {
 
 trace!(FibonacciSquareTrace<F> {
  a: F, b: F,
-},  0, 0, 1024 );
+},  0, 0, 262144 );
 
 trace!(ModuleTrace<F> {
  x: F, q: F, x_mod: F,
-},  0, 1, 1024 );
+},  0, 1, 16384 );
 
 trace!(U8AirTrace<F> {
  mul: F,
 },  0, 2, 256 );
 
 trace!(FibonacciSquareRomTrace<F> {
  line: F, flags: F,
-}, 0, 0, 1024, 0 );
+}, 0, 0, 262144, 0 );
 
 values!(FibonacciSquareAirValues<F> {
  fibo1: [F; 2], fibo3: FieldExtension<F>,
 });
 
+values!(ModuleAirValues<F> {
+ last_segment: F,
+});
+
 values!(FibonacciSquareAirGroupValues<F> {
  gsum_result: FieldExtension<F>,
 });