Merge branch 'main' into feature/range_check

Author: TomWambsgans

README.md

@@ -56,6 +56,19 @@ RUSTFLAGS='-C target-cpu=native' cargo run --release -- xmss --n-signatures 990
 
 ![Alt text](docs/benchmark_graphs/graphs/xmss_aggregated_overhead.svg)
 
+### Fibonacci:
+
+n = 2,000,000
+
+```
+RUSTFLAGS='-C target-cpu=native' cargo test --release --package lean_prover --test test_zkvm -- --nocapture -- test_prove_fibonacci --exact --nocapture
+```
+
+Proving time:
+
+- i9-12900H: 2.0 s (1.0 MHz)
+- mac m4 max: 1.2 s (1.7 MHz)
+
 ### Proof size
 
 With conjecture "up to capacity", current proofs with rate = 1/2 are about ≈ 400 - 500 KiB, of which ≈ 300 KiB comes from WHIR.

TODO.md

@@ -27,6 +27,25 @@
 - Opti WHIR https://github.com/tcoratger/whir-p3/issues/303 and https://github.com/tcoratger/whir-p3/issues/306
 - Avoid committing to the 3 index columns, and replace it by a sumcheck? Using this idea, we would only commit to PC and FP for the execution table. Idea by Georg (Powdr). Do we even need to commit to FP then?
 
+- About the ordering of the variables in sumchecks, currently we do as follows:
+
+[a, b, c, d, e, f, g, h]                                        (1st round of sumcheck)
+[(a-r).a + r.e, (1-r).b + r.f, (1-r).c + r.g, (1-r).d + r.h]    (2nd round of sumcheck)
+... etc
+
+This is otpimal for packing (SIMD) but not optimal when to comes to padding.
+When there are a lot of "ending" zeros, the optimal way of folding is:
+
+[a, b, c, d, e, 0, 0, 0]                                        (1st round of sumcheck)
+[(a-r).a + r.b, (1-r).c + r.d, (1-r).e, 0]                      (2nd round of sumcheck)
+... etc
+
+But we can get the bost of both worlds (suggested by Lev, TODO implement):
+
+[a, b, c, d, e, f, g, h, i, 0, 0, 0, 0, 0, 0, 0]                                    (1st round of sumcheck)
+[(1-r).a + r.c, (1-r).b + r.d, (1-r).e + r.g, (1-r).f + r.h, (1-r).i, 0, 0, 0]      (2nd round of sumcheck)
+... etc
+
 About "the packed pcs" (similar to SP1 Jagged PCS, slightly less efficient, but simpler (no sumchecks)):
 - The best strategy is probably to pack as much as possible (the cost increasing the density = additional inner evaluations), if we can fit below a power of 2 - epsilon  (epsilon = 20% for instance, tbd), if the sum of the non zero data is just above a power of 2, no packed technique, even the best, can help us, so we should spread aniway (to reduce the pressure of inner evaluations)
 - About those inner evaluations, there is a trick: we need to compute M1(a, b, c, d, ...) then M2(b, c, d, ...), then M3(c, d, ...) -> The trick = compute the "eq(.) for (b, c, d), then dot product with M3. Then expand to eq(b, c, d, ...), dot product with M2. Then expand to eq(a, b, c, d, ...), dot product with M1. The idea is that in this order, computing each "eq" is easier is we start from the previous one.
@@ -68,6 +87,10 @@ But we reduce proof size a lot using instead (TODO):
 └────────────────────────┘└──────────┘└─┘
 ```
 
+## Security:
+
+Fiat Shamir: add a claim tracing feature, to ensure all the claims are indeed checked (Lev)
+
 ## Not Perf
 
 - Whir batching: handle the case where the second polynomial is too small compared to the first one

crates/lean_compiler/src/a_simplify_lang.rs

@@ -96,6 +96,7 @@ pub enum SimpleLine {
         condition: SimpleExpr,
         then_branch: Vec<Self>,
         else_branch: Vec<Self>,
+        line_number: SourceLineNumber,
     },
     TestZero {
         // Test that the result of the given operation is zero
@@ -107,6 +108,7 @@ pub enum SimpleLine {
         function_name: String,
         args: Vec<SimpleExpr>,
         return_data: Vec<Var>,
+        line_number: SourceLineNumber,
     },
     FunctionRet {
         return_data: Vec<SimpleExpr>,
@@ -320,7 +322,7 @@ fn simplify_lines(
                     const_malloc,
                 );
             }
-            Line::Assert(boolean) => match boolean {
+            Line::Assert(boolean, line_number) => match boolean {
                 Boolean::Different { left, right } => {
                     let left = simplify_expr(left, &mut res, counters, array_manager, const_malloc);
                     let right =
@@ -337,6 +339,7 @@ fn simplify_lines(
                         condition: diff_var.into(),
                         then_branch: vec![],
                         else_branch: vec![SimpleLine::Panic],
+                        line_number: *line_number,
                     });
                 }
                 Boolean::Equal { left, right } => {
@@ -362,6 +365,7 @@ fn simplify_lines(
                 condition,
                 then_branch,
                 else_branch,
+                line_number,
             } => {
                 let (condition_simplified, then_branch, else_branch) = match condition {
                     Condition::Comparison(condition) => {
@@ -472,6 +476,7 @@ fn simplify_lines(
                     condition: condition_simplified,
                     then_branch: then_branch_simplified,
                     else_branch: else_branch_simplified,
+                    line_number: *line_number,
                 });
             }
             Line::ForLoop {
@@ -481,6 +486,7 @@ fn simplify_lines(
                 body,
                 rev,
                 unroll,
+                line_number,
             } => {
                 if *unroll {
                     let (internal_variables, _) = find_variable_usage(body);
@@ -538,7 +544,7 @@ fn simplify_lines(
                 const_malloc.counter = loop_const_malloc.counter;
                 array_manager.valid = valid_aux_vars_in_array_manager_before; // restore the valid aux vars
 
-                let func_name = format!("@loop_{}", counters.loops);
+                let func_name = format!("@loop_{}_line_{}", counters.loops, line_number);
                 counters.loops += 1;
 
                 // Find variables used inside loop but defined outside
@@ -578,6 +584,7 @@ fn simplify_lines(
                 // Create recursive function body
                 let recursive_func = create_recursive_function(
                     func_name.clone(),
+                    *line_number,
                     func_args,
                     iterator.clone(),
                     end_simplified,
@@ -594,12 +601,14 @@ fn simplify_lines(
                     function_name: func_name,
                     args: call_args,
                     return_data: vec![],
+                    line_number: *line_number,
                 });
             }
             Line::FunctionCall {
                 function_name,
                 args,
                 return_data,
+                line_number,
             } => {
                 let simplified_args = args
                     .iter()
@@ -609,6 +618,7 @@ fn simplify_lines(
                     function_name: function_name.clone(),
                     args: simplified_args,
                     return_data: return_data.clone(),
+                    line_number: *line_number,
                 });
             }
             Line::FunctionRet { return_data } => {
@@ -884,6 +894,7 @@ pub fn find_variable_usage(lines: &[Line]) -> (BTreeSet<Var>, BTreeSet<Var>) {
                 condition,
                 then_branch,
                 else_branch,
+                line_number: _,
             } => {
                 on_new_condition(condition, &internal_vars, &mut external_vars);
 
@@ -906,7 +917,7 @@ pub fn find_variable_usage(lines: &[Line]) -> (BTreeSet<Var>, BTreeSet<Var>) {
                 }
                 internal_vars.extend(return_data.iter().cloned());
             }
-            Line::Assert(condition) => {
+            Line::Assert(condition, _line_number) => {
                 on_new_condition(
                     &Condition::Comparison(condition.clone()),
                     &internal_vars,
@@ -953,6 +964,7 @@ pub fn find_variable_usage(lines: &[Line]) -> (BTreeSet<Var>, BTreeSet<Var>) {
                 body,
                 rev: _,
                 unroll: _,
+                line_number: _,
             } => {
                 let (body_internal, body_external) = find_variable_usage(body);
                 internal_vars.extend(body_internal);
@@ -1052,6 +1064,7 @@ pub fn inline_lines(
                 condition,
                 then_branch,
                 else_branch,
+                line_number: _,
             } => {
                 inline_condition(condition);
 
@@ -1070,7 +1083,7 @@ pub fn inline_lines(
                     inline_internal_var(return_var);
                 }
             }
-            Line::Assert(condition) => {
+            Line::Assert(condition, _line_number) => {
                 inline_comparison(condition);
             }
             Line::FunctionRet { return_data } => {
@@ -1124,6 +1137,7 @@ pub fn inline_lines(
                 body,
                 rev: _,
                 unroll: _,
+                line_number: _,
             } => {
                 inline_lines(body, args, res, inlining_count);
                 inline_internal_var(iterator);
@@ -1246,6 +1260,7 @@ fn handle_array_assignment(
 
 fn create_recursive_function(
     name: String,
+    line_number: SourceLineNumber,
     args: Vec<Var>,
     iterator: Var,
     end: SimpleExpr,
@@ -1269,6 +1284,7 @@ fn create_recursive_function(
         function_name: name.clone(),
         args: recursive_args,
         return_data: vec![],
+        line_number,
     });
     body.push(SimpleLine::FunctionRet {
         return_data: vec![],
@@ -1289,6 +1305,7 @@ fn create_recursive_function(
             else_branch: vec![SimpleLine::FunctionRet {
                 return_data: vec![],
             }],
+            line_number,
         },
     ];
 
@@ -1428,7 +1445,10 @@ fn replace_vars_for_unroll(
                     internal_vars,
                 );
             }
-            Line::Assert(Boolean::Equal { left, right } | Boolean::Different { left, right }) => {
+            Line::Assert(
+                Boolean::Equal { left, right } | Boolean::Different { left, right },
+                _line_number,
+            ) => {
                 replace_vars_for_unroll_in_expr(
                     left,
                     iterator,
@@ -1448,6 +1468,7 @@ fn replace_vars_for_unroll(
                 condition,
                 then_branch,
                 else_branch,
+                line_number: _,
             } => {
                 match condition {
                     Condition::Comparison(
@@ -1501,6 +1522,7 @@ fn replace_vars_for_unroll(
                 body,
                 rev: _,
                 unroll: _,
+                line_number: _,
             } => {
                 assert!(other_iterator != iterator);
                 *other_iterator =
@@ -1531,6 +1553,7 @@ fn replace_vars_for_unroll(
                 function_name: _,
                 args,
                 return_data,
+                line_number: _,
             } => {
                 // Function calls are not unrolled, so we don't need to change them
                 for arg in args {
@@ -1721,6 +1744,7 @@ fn handle_inlined_functions_helper(
                 function_name,
                 args,
                 return_data,
+                line_number: _,
             } => {
                 if let Some(func) = inlined_functions.get(&*function_name) {
                     let mut inlined_lines = vec![];
@@ -1872,6 +1896,7 @@ fn handle_const_arguments_helper(
                 function_name,
                 args,
                 return_data: _,
+                line_number: _,
             } => {
                 if let Some(func) = constant_functions.get(function_name) {
                     // If the function has constant arguments, we need to handle them
@@ -2064,6 +2089,7 @@ fn replace_vars_by_const_in_lines(lines: &mut [Line], map: &BTreeMap<Var, F>) {
                 condition,
                 then_branch,
                 else_branch,
+                line_number: _,
             } => {
                 match condition {
                     Condition::Comparison(Boolean::Equal { left, right })
@@ -2085,7 +2111,7 @@ fn replace_vars_by_const_in_lines(lines: &mut [Line], map: &BTreeMap<Var, F>) {
                 replace_vars_by_const_in_expr(end, map);
                 replace_vars_by_const_in_lines(body, map);
             }
-            Line::Assert(condition) => match condition {
+            Line::Assert(condition, _line_number) => match condition {
                 Boolean::Equal { left, right } | Boolean::Different { left, right } => {
                     replace_vars_by_const_in_expr(left, map);
                     replace_vars_by_const_in_expr(right, map);
@@ -2225,6 +2251,7 @@ impl SimpleLine {
                 condition,
                 then_branch,
                 else_branch,
+                line_number: _,
             } => {
                 let then_str = then_branch
                     .iter()
@@ -2250,6 +2277,7 @@ impl SimpleLine {
                 function_name,
                 args,
                 return_data,
+                line_number: _,
             } => {
                 let args_str = args
                     .iter()

crates/lean_compiler/src/b_compile_intermediate.rs

@@ -288,16 +288,17 @@ fn compile_lines(
                 condition,
                 then_branch,
                 else_branch,
+                line_number,
             } => {
                 validate_vars_declared(&[condition], declared_vars)?;
 
                 let if_id = compiler.if_counter;
                 compiler.if_counter += 1;
 
                 let (if_label, else_label, end_label) = (
-                    Label::if_label(if_id),
-                    Label::else_label(if_id),
-                    Label::if_else_end(if_id),
+                    Label::if_label(if_id, *line_number),
+                    Label::else_label(if_id, *line_number),
+                    Label::if_else_end(if_id, *line_number),
                 );
 
                 // c: condition
@@ -426,10 +427,11 @@ fn compile_lines(
                 function_name: callee_function_name,
                 args,
                 return_data,
+                line_number,
             } => {
                 let call_id = compiler.call_counter;
                 compiler.call_counter += 1;
-                let return_label = Label::return_from_call(call_id);
+                let return_label = Label::return_from_call(call_id, *line_number);
 
                 let new_fp_pos = compiler.stack_size;
                 compiler.stack_size += 1;