diff --git a/src/air.cairo b/src/air.cairo index e1b991d70..0bf3c381b 100644 --- a/src/air.cairo +++ b/src/air.cairo @@ -3,3 +3,4 @@ mod global_values; mod constants; mod public_input; mod public_memory; +mod diluted; diff --git a/src/air/composition.cairo b/src/air/composition.cairo index 0b552bc98..02df0283e 100644 --- a/src/air/composition.cairo +++ b/src/air/composition.cairo @@ -1,6 +1,7 @@ use cairo_verifier::air::global_values::{EcPoint, InteractionElements, GlobalValues}; -use cairo_verifier::air::constants::{PUBLIC_MEMORY_STEP}; +use cairo_verifier::air::constants::{PUBLIC_MEMORY_STEP, DILUTED_N_BITS, DILUTED_SPACING}; use cairo_verifier::air::public_input::{PublicInput, PublicInputTrait}; +use cairo_verifier::air::diluted::get_diluted_product; use cairo_verifier::common::felt252::{Felt252Div, Felt252PartialOrd}; fn eval_composition_polynomial( @@ -22,6 +23,11 @@ fn eval_composition_polynomial( .get_public_memory_product_ratio(memory_z, memory_alpha, public_memory_column_size); // TODO diluted + let diluted_z = interaction_elements.diluted_check_interaction_z; + let diluted_alpha = interaction_elements.diluted_check_interaction_alpha; + let diluted_prod = get_diluted_product( + DILUTED_N_BITS, DILUTED_SPACING, diluted_z, diluted_alpha + ); // TODO periodic cols diff --git a/src/air/diluted.cairo b/src/air/diluted.cairo new file mode 100644 index 000000000..9284b7502 --- /dev/null +++ b/src/air/diluted.cairo @@ -0,0 +1,48 @@ +use cairo_verifier::common::felt252::pow; + +// The cumulative value is defined using the next recursive formula: +// r_1 = 1, r_{j+1} = r_j * (1 + z * u_j) + alpha * u_j^2 +// where u_j = Dilute(j, spacing, n_bits) - Dilute(j-1, spacing, n_bits) +// and we want to compute the final value r_{2^n_bits}. +// Note that u_j depends only on the number of trailing zeros in the binary representation of j. +// Specifically, u_{(1+2k)*2^i} = u_{2^i} = u_{2^{i-1}} + 2^{i*spacing} - 2^{(i-1)*spacing + 1}. +// +// The recursive formula can be reduced to a nonrecursive form: +// r_j = prod_{n=1..j-1}(1+z*u_n) + alpha*sum_{n=1..j-1}(u_n^2 * prod_{m=n+1..j-1}(1+z*u_m)) +// +// We rewrite this equation to generate a recursive formula that converges in log(j) steps: +// Denote: +// p_i = prod_{n=1..2^i-1}(1+z*u_n) +// q_i = sum_{n=1..2^i-1}(u_n^2 * prod_{m=n+1..2^i-1}(1+z*u_m)) +// x_i = u_{2^i}. +// +// Clearly +// r_{2^i} = p_i + alpha * q_i. +// Moreover, +// p_i = p_{i-1} * (1 + z * x_{i-1}) * p_{i-1} +// q_i = q_{i-1} * (1 + z * x_{i-1}) * p_{i-1} + x_{i-1}^2 * p_{i-1} + q_{i-1} +// +// Now we can compute p_{n_bits} and q_{n_bits} in just n_bits recursive steps and we are done. +fn get_diluted_product(n_bits: felt252, spacing: felt252, z: felt252, alpha: felt252) -> felt252 { + let diff_multiplier = pow(2, spacing); + let mut diff_x = diff_multiplier - 2; + let mut x = 1; + let mut p = 1 + z; + let mut q = 1; + + let mut i = 0; + loop { + if i == n_bits { + break p + q * alpha; + } + + x = x + diff_x; + diff_x *= diff_multiplier; + let x_p = x * p; + let y = p + z * x_p; + q = q * y + x * x_p + q; + p *= y; + + i += 1; + } +} diff --git a/src/air/public_memory.cairo b/src/air/public_memory.cairo index 96a70d501..262af7ddc 100644 --- a/src/air/public_memory.cairo +++ b/src/air/public_memory.cairo @@ -40,6 +40,7 @@ impl PageImpl of PageTrait { let current = self.at(i); res *= z - (*current.address + alpha * *current.value); + i += 1; } } } @@ -56,6 +57,8 @@ fn get_continuous_pages_product(page_headers: Span) -> (fe res *= *current.prod; total_length += *current.size; + + i += 1; } }