-
Notifications
You must be signed in to change notification settings - Fork 23
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into feat/vcommitment
- Loading branch information
Showing
12 changed files
with
2,268 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
mod composition; | ||
mod global_values; | ||
mod constants; | ||
mod public_input; | ||
mod public_memory; | ||
mod diluted; | ||
mod pedersen; | ||
mod autogenerated; |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
} | ||
|
Oops, something went wrong.