fix typo in JohnsonBound formula (#187)

* typo in JohnsonBound formula

* improved log_eta

* missing link

---------

Co-authored-by: Tom Wambsgans <TomWambsgans@users.noreply.github.com>

Author: TomWambsgans

README.md

@@ -52,7 +52,7 @@ cargo run --release -- recursion --n 2
 
 | Proven          | Conjectured     |
 | --------------- | --------------- |
-| 0.8s - 188 KiB | 0.57s - 116 KiB |
+| 0.85s - 188 KiB | 0.57s - 116 KiB |
 
 
 ### Bonus: unbounded recursive aggregation

crates/rec_aggregation/fiat_shamir.py

@@ -179,14 +179,14 @@ def fs_finalize_sample(fs, total_n_chunks):
 
 @inline
 def fs_sample_queries(fs, n_samples):
-    debug_assert(n_samples < 256)
+    debug_assert(n_samples < 512)
     # Compute total_chunks = ceil(n_samples / 8) via bit decomposition.
-    # Big-endian: nb[0]=bit7 (MSB), nb[7]=bit0 (LSB).
-    nb = checked_decompose_bits_small_value_const(n_samples, 8)
-    floor_div = nb[0] * 16 + nb[1] * 8 + nb[2] * 4 + nb[3] * 2 + nb[4]
-    has_remainder = 1 - (1 - nb[5]) * (1 - nb[6]) * (1 - nb[7])
+    # Big-endian: nb[0]=bit8 (MSB), nb[8]=bit0 (LSB).
+    nb = checked_decompose_bits_small_value_const(n_samples, 9)
+    floor_div = nb[0] * 32 + nb[1] * 16 + nb[2] * 8 + nb[3] * 4 + nb[4] * 2 + nb[5]
+    has_remainder = 1 - (1 - nb[6]) * (1 - nb[7]) * (1 - nb[8])
     total_chunks = floor_div + has_remainder
     # Sample exactly the needed chunks (dispatch via match_range to keep n_chunks const)
-    sampled = match_range(total_chunks, range(0, 33), lambda nc: fs_sample_data_with_offset(fs, nc, 0))
+    sampled = match_range(total_chunks, range(0, 65), lambda nc: fs_sample_data_with_offset(fs, nc, 0))
     new_fs = fs_finalize_sample(fs, total_chunks)
     return sampled, new_fs

crates/rec_aggregation/src/compilation.rs

@@ -53,7 +53,7 @@ fn compile_main_program(inner_program_log_size: usize, bytecode_zero_eval: F) ->
 
 #[instrument(skip_all)]
 fn compile_main_program_self_referential() -> Bytecode {
-    let mut log_size_guess = 18;
+    let mut log_size_guess = 19;
     let bytecode_zero_eval = F::ONE;
     loop {
         let bytecode = compile_main_program(log_size_guess, bytecode_zero_eval);
@@ -145,7 +145,7 @@ fn build_replacements(
         all_potential_folding_grinding.push(format!("[{}]", folding_grinding_for_rate.join(", ")));
     }
     if too_much_grinding {
-        tracing::warn!("Too much grinding for WHIR folding",);
+        tracing::info!("Warning: Too much grinding for WHIR folding"); // TODO
     }
     replacements.insert(
         "WHIR_FIRST_RS_REDUCTION_FACTOR_PLACEHOLDER".to_string(),

crates/rec_aggregation/utils.py

@@ -17,10 +17,10 @@ def div_ceil_dynamic(a, b: Const):
 def powers(alpha, n):
     # alpha: EF
     # n: F
-    assert n < 256
+    assert n < 400
     assert 0 < n
     # 2**log2_ceil(i) is not really necessary but helps reduce byetcode size (traedoff cycles / bytecode size)
-    res = match_range(n, range(1, 256), lambda i: powers_const(alpha, 2**log2_ceil(i)))
+    res = match_range(n, range(1, 400), lambda i: powers_const(alpha, 2**log2_ceil(i)))
     return res
 
 
@@ -139,8 +139,8 @@ def eval_multilinear_coeffs_rev(coeffs, point, n: Const):
 
 
 def dot_product_be_dynamic(a, b, res, n):
-    debug_assert(n <= 256)
-    match_range(n, range(1, 257), lambda i: dot_product_be(a, b, res, i))
+    debug_assert(n < 400)
+    match_range(n, range(1, 400), lambda i: dot_product_be(a, b, res, i))
     return
 
 
@@ -150,8 +150,8 @@ def dot_product_be_const(a, b, res, n: Const):
 
 
 def dot_product_ee_dynamic(a, b, res, n):
-    debug_assert(n <= 256)
-    match_range(n, range(1, 257), lambda i: dot_product_ee(a, b, res, i))
+    debug_assert(n < 400)
+    match_range(n, range(1, 400), lambda i: dot_product_ee(a, b, res, i))
     return