Merge pull request #14 from HerodotusDev/feat/oods

AIR + OODS

src/air.cairo

@@ -0,0 +1,8 @@
+mod composition;
+mod global_values;
+mod constants;
+mod public_input;
+mod public_memory;
+mod diluted;
+mod pedersen;
+mod autogenerated;

src/air/composition.cairo

@@ -0,0 +1,81 @@
+use cairo_verifier::air::global_values::{EcPoint, InteractionElements, GlobalValues};
+use cairo_verifier::air::constants::{
+    PUBLIC_MEMORY_STEP, DILUTED_N_BITS, DILUTED_SPACING, PEDERSEN_BUILTIN_RATIO,
+    PEDERSEN_BUILTIN_REPETITIONS, segments
+};
+use cairo_verifier::air::public_input::{PublicInput, PublicInputTrait};
+use cairo_verifier::air::diluted::get_diluted_product;
+use cairo_verifier::air::pedersen::{eval_pedersen_x, eval_pedersen_y};
+use cairo_verifier::air::autogenerated::eval_composition_polynomial_inner;
+use cairo_verifier::common::math::{Felt252Div, Felt252PartialOrd, pow, assert_range_u128};
+
+const SHIFT_POINT_X: felt252 = 0x49ee3eba8c1600700ee1b87eb599f16716b0b1022947733551fde4050ca6804;
+const SHIFT_POINT_Y: felt252 = 0x3ca0cfe4b3bc6ddf346d49d06ea0ed34e621062c0e056c1d0405d266e10268a;
+
+fn eval_composition_polynomial(
+    interaction_elements: InteractionElements,
+    public_input: PublicInput,
+    mask_values: Array<felt252>,
+    constraint_coefficients: Array<felt252>,
+    point: felt252,
+    trace_domain_size: felt252,
+    trace_generator: felt252
+) -> felt252 {
+    let memory_z = interaction_elements.memory_multi_column_perm_perm_interaction_elm;
+    let memory_alpha = interaction_elements.memory_multi_column_perm_hash_interaction_elm0;
+
+    // Public memory
+    let public_memory_column_size = trace_domain_size / PUBLIC_MEMORY_STEP;
+    assert_range_u128(public_memory_column_size);
+    let public_memory_prod_ratio = public_input
+        .get_public_memory_product_ratio(memory_z, memory_alpha, public_memory_column_size);
+
+    // 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
+    );
+
+    // Periodic columns
+    let n_steps = pow(2, public_input.log_n_steps);
+    let n_pedersen_hash_copies = n_steps / (PEDERSEN_BUILTIN_RATIO * PEDERSEN_BUILTIN_REPETITIONS);
+    assert_range_u128(n_pedersen_hash_copies);
+    let pedersen_point = pow(point, n_pedersen_hash_copies);
+    let pedersen_points_x = eval_pedersen_x(pedersen_point);
+    let pedersen_points_y = eval_pedersen_y(pedersen_point);
+
+    let global_values = GlobalValues {
+        trace_length: trace_domain_size,
+        initial_pc: *public_input.segments.at(segments::PROGRAM).begin_addr,
+        final_pc: *public_input.segments.at(segments::PROGRAM).stop_ptr,
+        initial_ap: *public_input.segments.at(segments::EXECUTION).begin_addr,
+        final_ap: *public_input.segments.at(segments::EXECUTION).stop_ptr,
+        initial_pedersen_addr: *public_input.segments.at(segments::PEDERSEN).begin_addr,
+        initial_rc_addr: *public_input.segments.at(segments::RANGE_CHECK).begin_addr,
+        initial_bitwise_addr: *public_input.segments.at(segments::BITWISE).begin_addr,
+        rc_min: public_input.rc_min,
+        rc_max: public_input.rc_max,
+        offset_size: 0x10000, // 2**16
+        half_offset_size: 0x8000,
+        pedersen_shift_point: EcPoint { x: SHIFT_POINT_X, y: SHIFT_POINT_Y },
+        pedersen_points_x,
+        pedersen_points_y,
+        memory_multi_column_perm_perm_interaction_elm: memory_z,
+        memory_multi_column_perm_hash_interaction_elm0: memory_alpha,
+        rc16_perm_interaction_elm: interaction_elements.rc16_perm_interaction_elm,
+        diluted_check_permutation_interaction_elm: interaction_elements
+            .diluted_check_permutation_interaction_elm,
+        diluted_check_interaction_z: diluted_z,
+        diluted_check_interaction_alpha: diluted_alpha,
+        memory_multi_column_perm_perm_public_memory_prod: public_memory_prod_ratio,
+        rc16_perm_public_memory_prod: 1,
+        diluted_check_first_elm: 0,
+        diluted_check_permutation_public_memory_prod: 1,
+        diluted_check_final_cum_val: diluted_prod
+    };
+
+    eval_composition_polynomial_inner(
+        mask_values, constraint_coefficients, point, trace_generator, global_values
+    )
+}

src/air/constants.cairo

@@ -0,0 +1,40 @@
+// Recursive layout
+const N_DYNAMIC_PARAMS: felt252 = 0;
+const N_CONSTRAINTS: felt252 = 93;
+const MASK_SIZE: felt252 = 133;
+const PUBLIC_MEMORY_STEP: felt252 = 16;
+const HAS_DILUTED_POOL: felt252 = 1;
+const DILUTED_SPACING: felt252 = 4;
+const DILUTED_N_BITS: felt252 = 16;
+const PEDERSEN_BUILTIN_RATIO: felt252 = 128;
+const PEDERSEN_BUILTIN_REPETITIONS: felt252 = 1;
+const RC_BUILTIN_RATIO: felt252 = 8;
+const RC_N_PARTS: felt252 = 8;
+const BITWISE_RATIO: felt252 = 8;
+const BITWISE_TOTAL_N_BITS: felt252 = 251;
+const HAS_OUTPUT_BUILTIN: felt252 = 1;
+const HAS_PEDERSEN_BUILTIN: felt252 = 1;
+const HAS_RANGE_CHECK_BUILTIN: felt252 = 1;
+const HAS_ECDSA_BUILTIN: felt252 = 0;
+const HAS_BITWISE_BUILTIN: felt252 = 1;
+const HAS_EC_OP_BUILTIN: felt252 = 0;
+const HAS_KECCAK_BUILTIN: felt252 = 0;
+const HAS_POSEIDON_BUILTIN: felt252 = 0;
+const LAYOUT_CODE: felt252 = 0x726563757273697665;
+const CONSTRAINT_DEGREE: felt252 = 2;
+const CPU_COMPONENT_HEIGHT: felt252 = 16;
+const LOG_CPU_COMPONENT_HEIGHT: felt252 = 4;
+const MEMORY_STEP: felt252 = 2;
+const NUM_COLUMNS_FIRST: felt252 = 7;
+const NUM_COLUMNS_SECOND: felt252 = 3;
+const IS_DYNAMIC_AIR: felt252 = 0;
+
+mod segments {
+    const PROGRAM: usize = 0;
+    const EXECUTION: usize = 1;
+    const OUTPUT: usize = 2;
+    const PEDERSEN: usize = 3;
+    const RANGE_CHECK: usize = 4;
+    const BITWISE: usize = 5;
+    const N_SEGMENTS: usize = 6;
+}

src/air/diluted.cairo

@@ -0,0 +1,48 @@
+use cairo_verifier::common::math::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;
+    }
+}

src/air/global_values.cairo

@@ -0,0 +1,53 @@
+#[derive(Drop)]
+struct EcPoint {
+    x: felt252,
+    y: felt252,
+}
+
+// Accumulation of member expressions for auto generated composition polynomial code.
+#[derive(Drop)]
+struct GlobalValues {
+    // Public input.
+    trace_length: felt252,
+    initial_pc: felt252,
+    final_pc: felt252,
+    initial_ap: felt252,
+    final_ap: felt252,
+    initial_pedersen_addr: felt252,
+    initial_rc_addr: felt252,
+    initial_bitwise_addr: felt252,
+    rc_min: felt252,
+    rc_max: felt252,
+    // Constants.
+    offset_size: felt252,
+    half_offset_size: felt252,
+    pedersen_shift_point: EcPoint,
+    // Periodic columns.
+    pedersen_points_x: felt252,
+    pedersen_points_y: felt252,
+    // Interaction elements.
+    memory_multi_column_perm_perm_interaction_elm: felt252,
+    memory_multi_column_perm_hash_interaction_elm0: felt252,
+    rc16_perm_interaction_elm: felt252,
+    diluted_check_permutation_interaction_elm: felt252,
+    diluted_check_interaction_z: felt252,
+    diluted_check_interaction_alpha: felt252,
+    // Permutation products.
+    memory_multi_column_perm_perm_public_memory_prod: felt252,
+    rc16_perm_public_memory_prod: felt252,
+    diluted_check_first_elm: felt252,
+    diluted_check_permutation_public_memory_prod: felt252,
+    diluted_check_final_cum_val: felt252
+}
+
+// Elements that are sent from the prover after the commitment on the original trace.
+// Used for components after the first interaction, e.g., memory and range check.
+struct InteractionElements {
+    memory_multi_column_perm_perm_interaction_elm: felt252,
+    memory_multi_column_perm_hash_interaction_elm0: felt252,
+    rc16_perm_interaction_elm: felt252,
+    diluted_check_permutation_interaction_elm: felt252,
+    diluted_check_interaction_z: felt252,
+    diluted_check_interaction_alpha: felt252
+}
+