diff --git a/src/air/layouts.cairo b/src/air/layouts.cairo index f92f4f388..cb1d571e5 100644 --- a/src/air/layouts.cairo +++ b/src/air/layouts.cairo @@ -16,5 +16,7 @@ mod recursive; // === STARKNET_WITH_KECCAK BEGIN === // mod starknet_with_keccak; // === STARKNET_WITH_KECCAK END === - +// === DYNAMIC BEGIN === +// mod dynamic; +// === DYNAMIC END === diff --git a/src/air/layouts/dynamic.cairo b/src/air/layouts/dynamic.cairo new file mode 100644 index 000000000..c10472c72 --- /dev/null +++ b/src/air/layouts/dynamic.cairo @@ -0,0 +1,45 @@ +mod autogenerated; +mod constants; +mod global_values; +mod public_input; +mod traces; + +use cairo_verifier::{ + air::{ + constants::{SHIFT_POINT_X, SHIFT_POINT_Y, StarkCurve}, air::{AIRComposition, AIROods}, + diluted::get_diluted_product, + periodic_columns::{ + eval_pedersen_x, eval_pedersen_y, eval_ecdsa_x, eval_ecdsa_y, + eval_poseidon_poseidon_full_round_key0, eval_poseidon_poseidon_full_round_key1, + eval_poseidon_poseidon_full_round_key2, eval_poseidon_poseidon_partial_round_key0, + eval_poseidon_poseidon_partial_round_key1 + }, + public_input::{PublicInput, get_public_memory_product_ratio} + }, + common::{math::{Felt252Div, Felt252PartialOrd, pow}, asserts::assert_range_u128} +}; + +impl StarknetAIRCompositionImpl of AIRComposition { + fn eval_composition_polynomial( + interaction_elements: InteractionElements, + public_input: @PublicInput, + mask_values: Span, + constraint_coefficients: Span, + point: felt252, + trace_domain_size: felt252, + trace_generator: felt252 + ) -> felt252 {// TODO REWRITE + } +} + +impl StarknetAIROodsImpl of AIROods { + fn eval_oods_polynomial( + column_values: Span, + oods_values: Span, + constraint_coefficients: Span, + point: felt252, + oods_point: felt252, + trace_generator: felt252, + ) -> felt252 {// TODO REWRITE + } +} diff --git a/src/air/layouts/dynamic/autogenerated.cairo b/src/air/layouts/dynamic/autogenerated.cairo new file mode 100644 index 000000000..31788d364 --- /dev/null +++ b/src/air/layouts/dynamic/autogenerated.cairo @@ -0,0 +1,26 @@ +use cairo_verifier::{ + air::layouts::dex::{ + global_values::GlobalValues, + constants::{CONSTRAINT_DEGREE, NUM_COLUMNS_FIRST, NUM_COLUMNS_SECOND, MASK_SIZE} + }, + common::math::{Felt252Div, pow}, +}; + +fn eval_composition_polynomial_inner( + mut mask_values: Span, + mut constraint_coefficients: Span, + point: felt252, + trace_generator: felt252, + global_values: GlobalValues +) -> felt252 { // TODO REWRITE +} + +fn eval_oods_polynomial_inner( + mut column_values: Span, + mut oods_values: Span, + mut constraint_coefficients: Span, + point: felt252, + oods_point: felt252, + trace_generator: felt252, +) -> felt252 { // TODO REWRITE +} diff --git a/src/air/layouts/dynamic/constants.cairo b/src/air/layouts/dynamic/constants.cairo new file mode 100644 index 000000000..ad7d8119a --- /dev/null +++ b/src/air/layouts/dynamic/constants.cairo @@ -0,0 +1,416 @@ +const ADD_MOD_BATCH_SIZE: felt252 = 1; +const ADD_MOD_N_WORDS: felt252 = 4; +const ADD_MOD_WORD_BIT_LEN: felt252 = 96; +const BITWISE_TOTAL_N_BITS: felt252 = 251; +const CONSTRAINT_DEGREE: u32 = 2; +const CPU_COMPONENT_HEIGHT: felt252 = 16; +const DILUTED_N_BITS: felt252 = 16; +const DILUTED_SPACING: felt252 = 4; +const EC_OP_N_BITS: felt252 = 252; +const EC_OP_SCALAR_HEIGHT: felt252 = 256; +const ECDSA_BUILTIN_REPETITIONS: felt252 = 1; +const ECDSA_ELEMENT_BITS: felt252 = 251; +const ECDSA_ELEMENT_HEIGHT: felt252 = 256; +const HAS_ADD_MOD_BUILTIN: felt252 = 1; +const HAS_BITWISE_BUILTIN: felt252 = 1; +const HAS_DILUTED_POOL: felt252 = 1; +const HAS_EC_OP_BUILTIN: felt252 = 1; +const HAS_ECDSA_BUILTIN: felt252 = 1; +const HAS_KECCAK_BUILTIN: felt252 = 1; +const HAS_MUL_MOD_BUILTIN: felt252 = 1; +const HAS_OUTPUT_BUILTIN: felt252 = 1; +const HAS_PEDERSEN_BUILTIN: felt252 = 1; +const HAS_POSEIDON_BUILTIN: felt252 = 1; +const HAS_RANGE_CHECK_BUILTIN: felt252 = 1; +const HAS_RANGE_CHECK96_BUILTIN: felt252 = 1; +const IS_DYNAMIC_AIR: felt252 = 1; +const LAYOUT_CODE: felt252 = 0x64796e616d6963; +const MASK_SIZE: u32 = 941; +const MUL_MOD_BATCH_SIZE: felt252 = 1; +const MUL_MOD_N_WORDS: felt252 = 4; +const MUL_MOD_WORD_BIT_LEN: felt252 = 96; +const N_CONSTRAINTS: u32 = 419; +const N_DYNAMIC_PARAMS: felt252 = 340; +const PEDERSEN_BUILTIN_REPETITIONS: felt252 = 1; +const POSEIDON_M: felt252 = 3; +const POSEIDON_ROUNDS_FULL: felt252 = 8; +const POSEIDON_ROUNDS_PARTIAL: felt252 = 83; +const PUBLIC_MEMORY_FRACTION: felt252 = 8; +const RANGE_CHECK_N_PARTS: felt252 = 8; +const RANGE_CHECK96_N_PARTS: felt252 = 6; + +struct DynamicParams { + add_mod_a0_suboffset: felt252, + add_mod_a1_suboffset: felt252, + add_mod_a2_suboffset: felt252, + add_mod_a3_suboffset: felt252, + add_mod_a_offset_suboffset: felt252, + add_mod_b0_suboffset: felt252, + add_mod_b1_suboffset: felt252, + add_mod_b2_suboffset: felt252, + add_mod_b3_suboffset: felt252, + add_mod_b_offset_suboffset: felt252, + add_mod_c0_suboffset: felt252, + add_mod_c1_suboffset: felt252, + add_mod_c2_suboffset: felt252, + add_mod_c3_suboffset: felt252, + add_mod_c_offset_suboffset: felt252, + add_mod_carry1_bit_column: felt252, + add_mod_carry1_bit_offset: felt252, + add_mod_carry1_sign_column: felt252, + add_mod_carry1_sign_offset: felt252, + add_mod_carry2_bit_column: felt252, + add_mod_carry2_bit_offset: felt252, + add_mod_carry2_sign_column: felt252, + add_mod_carry2_sign_offset: felt252, + add_mod_carry3_bit_column: felt252, + add_mod_carry3_bit_offset: felt252, + add_mod_carry3_sign_column: felt252, + add_mod_carry3_sign_offset: felt252, + add_mod_n_suboffset: felt252, + add_mod_offsets_ptr_suboffset: felt252, + add_mod_p0_suboffset: felt252, + add_mod_p1_suboffset: felt252, + add_mod_p2_suboffset: felt252, + add_mod_p3_suboffset: felt252, + add_mod_row_ratio: felt252, + add_mod_sub_p_bit_column: felt252, + add_mod_sub_p_bit_offset: felt252, + add_mod_values_ptr_suboffset: felt252, + bitwise_diluted_var_pool_suboffset: felt252, + bitwise_row_ratio: felt252, + bitwise_trim_unpacking192_suboffset: felt252, + bitwise_trim_unpacking193_suboffset: felt252, + bitwise_trim_unpacking194_suboffset: felt252, + bitwise_trim_unpacking195_suboffset: felt252, + bitwise_var_pool_suboffset: felt252, + bitwise_x_or_y_suboffset: felt252, + cpu_decode_mem_inst_suboffset: felt252, + cpu_decode_off0_suboffset: felt252, + cpu_decode_off1_suboffset: felt252, + cpu_decode_off2_suboffset: felt252, + cpu_decode_opcode_range_check_column_column: felt252, + cpu_decode_opcode_range_check_column_offset: felt252, + cpu_operands_mem_dst_suboffset: felt252, + cpu_operands_mem_op0_suboffset: felt252, + cpu_operands_mem_op1_suboffset: felt252, + cpu_operands_ops_mul_column: felt252, + cpu_operands_ops_mul_offset: felt252, + cpu_operands_res_column: felt252, + cpu_operands_res_offset: felt252, + cpu_registers_ap_column: felt252, + cpu_registers_ap_offset: felt252, + cpu_registers_fp_column: felt252, + cpu_registers_fp_offset: felt252, + cpu_update_registers_update_pc_tmp0_column: felt252, + cpu_update_registers_update_pc_tmp0_offset: felt252, + cpu_update_registers_update_pc_tmp1_column: felt252, + cpu_update_registers_update_pc_tmp1_offset: felt252, + cpu_component_step: felt252, + diluted_check_cumulative_value_column: felt252, + diluted_check_cumulative_value_offset: felt252, + diluted_check_permutation_cum_prod0_column: felt252, + diluted_check_permutation_cum_prod0_offset: felt252, + diluted_check_permuted_values_column: felt252, + diluted_check_permuted_values_offset: felt252, + diluted_pool_column: felt252, + diluted_pool_offset: felt252, + diluted_units_row_ratio: felt252, + ec_op_doubled_points_x_column: felt252, + ec_op_doubled_points_x_offset: felt252, + ec_op_doubled_points_y_column: felt252, + ec_op_doubled_points_y_offset: felt252, + ec_op_doubling_slope_column: felt252, + ec_op_doubling_slope_offset: felt252, + ec_op_ec_subset_sum_bit_unpacking_prod_ones192_column: felt252, + ec_op_ec_subset_sum_bit_unpacking_prod_ones192_offset: felt252, + ec_op_ec_subset_sum_bit_unpacking_prod_ones196_column: felt252, + ec_op_ec_subset_sum_bit_unpacking_prod_ones196_offset: felt252, + ec_op_ec_subset_sum_partial_sum_x_column: felt252, + ec_op_ec_subset_sum_partial_sum_x_offset: felt252, + ec_op_ec_subset_sum_partial_sum_y_column: felt252, + ec_op_ec_subset_sum_partial_sum_y_offset: felt252, + ec_op_ec_subset_sum_selector_column: felt252, + ec_op_ec_subset_sum_selector_offset: felt252, + ec_op_ec_subset_sum_slope_column: felt252, + ec_op_ec_subset_sum_slope_offset: felt252, + ec_op_ec_subset_sum_x_diff_inv_column: felt252, + ec_op_ec_subset_sum_x_diff_inv_offset: felt252, + ec_op_m_suboffset: felt252, + ec_op_p_x_suboffset: felt252, + ec_op_p_y_suboffset: felt252, + ec_op_q_x_suboffset: felt252, + ec_op_q_y_suboffset: felt252, + ec_op_r_x_suboffset: felt252, + ec_op_r_y_suboffset: felt252, + ec_op_builtin_row_ratio: felt252, + ecdsa_message_suboffset: felt252, + ecdsa_pubkey_suboffset: felt252, + ecdsa_signature0_add_results_inv_column: felt252, + ecdsa_signature0_add_results_inv_offset: felt252, + ecdsa_signature0_add_results_slope_column: felt252, + ecdsa_signature0_add_results_slope_offset: felt252, + ecdsa_signature0_doubling_slope_column: felt252, + ecdsa_signature0_doubling_slope_offset: felt252, + ecdsa_signature0_exponentiate_generator_partial_sum_x_column: felt252, + ecdsa_signature0_exponentiate_generator_partial_sum_x_offset: felt252, + ecdsa_signature0_exponentiate_generator_partial_sum_y_column: felt252, + ecdsa_signature0_exponentiate_generator_partial_sum_y_offset: felt252, + ecdsa_signature0_exponentiate_generator_selector_column: felt252, + ecdsa_signature0_exponentiate_generator_selector_offset: felt252, + ecdsa_signature0_exponentiate_generator_slope_column: felt252, + ecdsa_signature0_exponentiate_generator_slope_offset: felt252, + ecdsa_signature0_exponentiate_generator_x_diff_inv_column: felt252, + ecdsa_signature0_exponentiate_generator_x_diff_inv_offset: felt252, + ecdsa_signature0_exponentiate_key_partial_sum_x_column: felt252, + ecdsa_signature0_exponentiate_key_partial_sum_x_offset: felt252, + ecdsa_signature0_exponentiate_key_partial_sum_y_column: felt252, + ecdsa_signature0_exponentiate_key_partial_sum_y_offset: felt252, + ecdsa_signature0_exponentiate_key_selector_column: felt252, + ecdsa_signature0_exponentiate_key_selector_offset: felt252, + ecdsa_signature0_exponentiate_key_slope_column: felt252, + ecdsa_signature0_exponentiate_key_slope_offset: felt252, + ecdsa_signature0_exponentiate_key_x_diff_inv_column: felt252, + ecdsa_signature0_exponentiate_key_x_diff_inv_offset: felt252, + ecdsa_signature0_extract_r_inv_column: felt252, + ecdsa_signature0_extract_r_inv_offset: felt252, + ecdsa_signature0_extract_r_slope_column: felt252, + ecdsa_signature0_extract_r_slope_offset: felt252, + ecdsa_signature0_key_points_x_column: felt252, + ecdsa_signature0_key_points_x_offset: felt252, + ecdsa_signature0_key_points_y_column: felt252, + ecdsa_signature0_key_points_y_offset: felt252, + ecdsa_signature0_q_x_squared_column: felt252, + ecdsa_signature0_q_x_squared_offset: felt252, + ecdsa_signature0_r_w_inv_column: felt252, + ecdsa_signature0_r_w_inv_offset: felt252, + ecdsa_signature0_z_inv_column: felt252, + ecdsa_signature0_z_inv_offset: felt252, + ecdsa_builtin_row_ratio: felt252, + keccak_input_output_suboffset: felt252, + keccak_keccak_diluted_column0_suboffset: felt252, + keccak_keccak_diluted_column1_suboffset: felt252, + keccak_keccak_diluted_column2_suboffset: felt252, + keccak_keccak_diluted_column3_suboffset: felt252, + keccak_keccak_parse_to_diluted_cumulative_sum_column: felt252, + keccak_keccak_parse_to_diluted_cumulative_sum_offset: felt252, + keccak_keccak_parse_to_diluted_final_reshaped_input_column: felt252, + keccak_keccak_parse_to_diluted_final_reshaped_input_offset: felt252, + keccak_keccak_parse_to_diluted_reshaped_intermediate_column: felt252, + keccak_keccak_parse_to_diluted_reshaped_intermediate_offset: felt252, + keccak_keccak_rotated_parity0_column: felt252, + keccak_keccak_rotated_parity0_offset: felt252, + keccak_keccak_rotated_parity1_column: felt252, + keccak_keccak_rotated_parity1_offset: felt252, + keccak_keccak_rotated_parity2_column: felt252, + keccak_keccak_rotated_parity2_offset: felt252, + keccak_keccak_rotated_parity3_column: felt252, + keccak_keccak_rotated_parity3_offset: felt252, + keccak_keccak_rotated_parity4_column: felt252, + keccak_keccak_rotated_parity4_offset: felt252, + keccak_row_ratio: felt252, + mem_pool_addr_column: felt252, + mem_pool_addr_offset: felt252, + mem_pool_value_column: felt252, + mem_pool_value_offset: felt252, + memory_multi_column_perm_perm_cum_prod0_column: felt252, + memory_multi_column_perm_perm_cum_prod0_offset: felt252, + memory_sorted_addr_column: felt252, + memory_sorted_addr_offset: felt252, + memory_sorted_value_column: felt252, + memory_sorted_value_offset: felt252, + memory_units_row_ratio: felt252, + mul_mod_a0_suboffset: felt252, + mul_mod_a1_suboffset: felt252, + mul_mod_a2_suboffset: felt252, + mul_mod_a3_suboffset: felt252, + mul_mod_a_offset_suboffset: felt252, + mul_mod_b0_suboffset: felt252, + mul_mod_b1_suboffset: felt252, + mul_mod_b2_suboffset: felt252, + mul_mod_b3_suboffset: felt252, + mul_mod_b_offset_suboffset: felt252, + mul_mod_c0_suboffset: felt252, + mul_mod_c1_suboffset: felt252, + mul_mod_c2_suboffset: felt252, + mul_mod_c3_suboffset: felt252, + mul_mod_c_offset_suboffset: felt252, + mul_mod_carry0_part0_suboffset: felt252, + mul_mod_carry0_part1_suboffset: felt252, + mul_mod_carry0_part2_suboffset: felt252, + mul_mod_carry0_part3_suboffset: felt252, + mul_mod_carry0_part4_suboffset: felt252, + mul_mod_carry0_part5_suboffset: felt252, + mul_mod_carry0_part6_suboffset: felt252, + mul_mod_carry1_part0_suboffset: felt252, + mul_mod_carry1_part1_suboffset: felt252, + mul_mod_carry1_part2_suboffset: felt252, + mul_mod_carry1_part3_suboffset: felt252, + mul_mod_carry1_part4_suboffset: felt252, + mul_mod_carry1_part5_suboffset: felt252, + mul_mod_carry1_part6_suboffset: felt252, + mul_mod_carry2_part0_suboffset: felt252, + mul_mod_carry2_part1_suboffset: felt252, + mul_mod_carry2_part2_suboffset: felt252, + mul_mod_carry2_part3_suboffset: felt252, + mul_mod_carry2_part4_suboffset: felt252, + mul_mod_carry2_part5_suboffset: felt252, + mul_mod_carry2_part6_suboffset: felt252, + mul_mod_carry3_part0_suboffset: felt252, + mul_mod_carry3_part1_suboffset: felt252, + mul_mod_carry3_part2_suboffset: felt252, + mul_mod_carry3_part3_suboffset: felt252, + mul_mod_carry3_part4_suboffset: felt252, + mul_mod_carry3_part5_suboffset: felt252, + mul_mod_carry3_part6_suboffset: felt252, + mul_mod_carry4_part0_suboffset: felt252, + mul_mod_carry4_part1_suboffset: felt252, + mul_mod_carry4_part2_suboffset: felt252, + mul_mod_carry4_part3_suboffset: felt252, + mul_mod_carry4_part4_suboffset: felt252, + mul_mod_carry4_part5_suboffset: felt252, + mul_mod_carry4_part6_suboffset: felt252, + mul_mod_carry5_part0_suboffset: felt252, + mul_mod_carry5_part1_suboffset: felt252, + mul_mod_carry5_part2_suboffset: felt252, + mul_mod_carry5_part3_suboffset: felt252, + mul_mod_carry5_part4_suboffset: felt252, + mul_mod_carry5_part5_suboffset: felt252, + mul_mod_carry5_part6_suboffset: felt252, + mul_mod_n_suboffset: felt252, + mul_mod_offsets_ptr_suboffset: felt252, + mul_mod_p0_suboffset: felt252, + mul_mod_p1_suboffset: felt252, + mul_mod_p2_suboffset: felt252, + mul_mod_p3_suboffset: felt252, + mul_mod_p_multiplier0_part0_suboffset: felt252, + mul_mod_p_multiplier0_part1_suboffset: felt252, + mul_mod_p_multiplier0_part2_suboffset: felt252, + mul_mod_p_multiplier0_part3_suboffset: felt252, + mul_mod_p_multiplier0_part4_suboffset: felt252, + mul_mod_p_multiplier0_part5_suboffset: felt252, + mul_mod_p_multiplier1_part0_suboffset: felt252, + mul_mod_p_multiplier1_part1_suboffset: felt252, + mul_mod_p_multiplier1_part2_suboffset: felt252, + mul_mod_p_multiplier1_part3_suboffset: felt252, + mul_mod_p_multiplier1_part4_suboffset: felt252, + mul_mod_p_multiplier1_part5_suboffset: felt252, + mul_mod_p_multiplier2_part0_suboffset: felt252, + mul_mod_p_multiplier2_part1_suboffset: felt252, + mul_mod_p_multiplier2_part2_suboffset: felt252, + mul_mod_p_multiplier2_part3_suboffset: felt252, + mul_mod_p_multiplier2_part4_suboffset: felt252, + mul_mod_p_multiplier2_part5_suboffset: felt252, + mul_mod_p_multiplier3_part0_suboffset: felt252, + mul_mod_p_multiplier3_part1_suboffset: felt252, + mul_mod_p_multiplier3_part2_suboffset: felt252, + mul_mod_p_multiplier3_part3_suboffset: felt252, + mul_mod_p_multiplier3_part4_suboffset: felt252, + mul_mod_p_multiplier3_part5_suboffset: felt252, + mul_mod_row_ratio: felt252, + mul_mod_values_ptr_suboffset: felt252, + num_columns_first: felt252, + num_columns_second: felt252, + orig_public_memory_suboffset: felt252, + pedersen_hash0_ec_subset_sum_bit_unpacking_prod_ones192_column: felt252, + pedersen_hash0_ec_subset_sum_bit_unpacking_prod_ones192_offset: felt252, + pedersen_hash0_ec_subset_sum_bit_unpacking_prod_ones196_column: felt252, + pedersen_hash0_ec_subset_sum_bit_unpacking_prod_ones196_offset: felt252, + pedersen_hash0_ec_subset_sum_partial_sum_x_column: felt252, + pedersen_hash0_ec_subset_sum_partial_sum_x_offset: felt252, + pedersen_hash0_ec_subset_sum_partial_sum_y_column: felt252, + pedersen_hash0_ec_subset_sum_partial_sum_y_offset: felt252, + pedersen_hash0_ec_subset_sum_selector_column: felt252, + pedersen_hash0_ec_subset_sum_selector_offset: felt252, + pedersen_hash0_ec_subset_sum_slope_column: felt252, + pedersen_hash0_ec_subset_sum_slope_offset: felt252, + pedersen_input0_suboffset: felt252, + pedersen_input1_suboffset: felt252, + pedersen_output_suboffset: felt252, + pedersen_builtin_row_ratio: felt252, + poseidon_param_0_input_output_suboffset: felt252, + poseidon_param_1_input_output_suboffset: felt252, + poseidon_param_2_input_output_suboffset: felt252, + poseidon_poseidon_full_rounds_state0_column: felt252, + poseidon_poseidon_full_rounds_state0_offset: felt252, + poseidon_poseidon_full_rounds_state0_squared_column: felt252, + poseidon_poseidon_full_rounds_state0_squared_offset: felt252, + poseidon_poseidon_full_rounds_state1_column: felt252, + poseidon_poseidon_full_rounds_state1_offset: felt252, + poseidon_poseidon_full_rounds_state1_squared_column: felt252, + poseidon_poseidon_full_rounds_state1_squared_offset: felt252, + poseidon_poseidon_full_rounds_state2_column: felt252, + poseidon_poseidon_full_rounds_state2_offset: felt252, + poseidon_poseidon_full_rounds_state2_squared_column: felt252, + poseidon_poseidon_full_rounds_state2_squared_offset: felt252, + poseidon_poseidon_partial_rounds_state0_column: felt252, + poseidon_poseidon_partial_rounds_state0_offset: felt252, + poseidon_poseidon_partial_rounds_state0_squared_column: felt252, + poseidon_poseidon_partial_rounds_state0_squared_offset: felt252, + poseidon_poseidon_partial_rounds_state1_column: felt252, + poseidon_poseidon_partial_rounds_state1_offset: felt252, + poseidon_poseidon_partial_rounds_state1_squared_column: felt252, + poseidon_poseidon_partial_rounds_state1_squared_offset: felt252, + poseidon_row_ratio: felt252, + range_check16_perm_cum_prod0_column: felt252, + range_check16_perm_cum_prod0_offset: felt252, + range_check16_sorted_column: felt252, + range_check16_sorted_offset: felt252, + range_check16_pool_column: felt252, + range_check16_pool_offset: felt252, + range_check96_builtin_inner_range_check0_suboffset: felt252, + range_check96_builtin_inner_range_check1_suboffset: felt252, + range_check96_builtin_inner_range_check2_suboffset: felt252, + range_check96_builtin_inner_range_check3_suboffset: felt252, + range_check96_builtin_inner_range_check4_suboffset: felt252, + range_check96_builtin_inner_range_check5_suboffset: felt252, + range_check96_builtin_mem_suboffset: felt252, + range_check96_builtin_row_ratio: felt252, + range_check_builtin_inner_range_check_suboffset: felt252, + range_check_builtin_mem_suboffset: felt252, + range_check_builtin_row_ratio: felt252, + range_check_units_row_ratio: felt252, + uses_add_mod_builtin: felt252, + uses_bitwise_builtin: felt252, + uses_ec_op_builtin: felt252, + uses_ecdsa_builtin: felt252, + uses_keccak_builtin: felt252, + uses_mul_mod_builtin: felt252, + uses_pedersen_builtin: felt252, + uses_poseidon_builtin: felt252, + uses_range_check96_builtin: felt252, + uses_range_check_builtin: felt252, +} + +mod segments { + const ADD_MOD: usize = 11; + const BITWISE: usize = 6; + const EC_OP: usize = 7; + const ECDSA: usize = 5; + const EXECUTION: usize = 1; + const KECCAK: usize = 8; + const MUL_MOD: usize = 12; + const N_SEGMENTS: usize = 13; + const OUTPUT: usize = 2; + const PEDERSEN: usize = 3; + const POSEIDON: usize = 9; + const PROGRAM: usize = 0; + const RANGE_CHECK: usize = 4; + const RANGE_CHECK96: usize = 10; +} + +fn get_builtins() -> Array { + array![ + 'output', + 'pedersen', + 'range_check', + 'ecdsa', + 'bitwise', + 'ec_op', + 'keccak', + 'poseidon', + 'range_check96', + 'add_mod', + 'mul_mod' + ] +} diff --git a/src/air/layouts/dynamic/global_values.cairo b/src/air/layouts/dynamic/global_values.cairo new file mode 100644 index 000000000..0a052aa4e --- /dev/null +++ b/src/air/layouts/dynamic/global_values.cairo @@ -0,0 +1,95 @@ +#[derive(Drop, Copy, Serde)] +struct EcPoint { + x: felt252, + y: felt252, +} + +#[derive(Drop, Copy, Serde)] +struct CurveConfig { + alpha: felt252, + beta: felt252, +} + +#[derive(Drop, Copy, Serde)] +struct EcdsaSigConfig { + alpha: felt252, + beta: felt252, + shift_point: EcPoint, +} + +// Accumulation of member expressions for auto generated composition polynomial code. +#[derive(Drop, Copy, Serde)] +struct GlobalValues { + // Public input. + trace_length: felt252, + initial_pc: felt252, + final_pc: felt252, + initial_ap: felt252, + final_ap: felt252, + initial_pedersen_addr: felt252, + initial_range_check_addr: felt252, + initial_ecdsa_addr: felt252, + initial_bitwise_addr: felt252, + initial_ec_op_addr: felt252, + initial_keccak_addr: felt252, + initial_poseidon_addr: felt252, + initial_range_check96_addr: felt252, + add_mod_initial_mod_addr: felt252, + mul_mod_initial_mod_addr: felt252, + range_check_min: felt252, + range_check_max: felt252, + // Constants. + offset_size: felt252, + half_offset_size: felt252, + pedersen_shift_point: EcPoint, + ecdsa_sig_config: EcdsaSigConfig, + ec_op_curve_config: CurveConfig, + // Periodic columns. + pedersen_points_x: felt252, + pedersen_points_y: felt252, + ecdsa_generator_points_x: felt252, + ecdsa_generator_points_y: felt252, + keccak_keccak_keccak_round_key0: felt252, + keccak_keccak_keccak_round_key1: felt252, + keccak_keccak_keccak_round_key3: felt252, + keccak_keccak_keccak_round_key7: felt252, + keccak_keccak_keccak_round_key15: felt252, + keccak_keccak_keccak_round_key31: felt252, + keccak_keccak_keccak_round_key63: felt252, + poseidon_poseidon_full_round_key0: felt252, + poseidon_poseidon_full_round_key1: felt252, + poseidon_poseidon_full_round_key2: felt252, + poseidon_poseidon_partial_round_key0: felt252, + poseidon_poseidon_partial_round_key1: felt252, + // Interaction elements. + memory_multi_column_perm_perm_interaction_elm: felt252, + memory_multi_column_perm_hash_interaction_elm0: felt252, + range_check16_perm_interaction_elm: felt252, + diluted_check_permutation_interaction_elm: felt252, + diluted_check_interaction_z: felt252, + diluted_check_interaction_alpha: felt252, + add_mod_interaction_elm: felt252, + mul_mod_interaction_elm: felt252, + // Permutation products. + memory_multi_column_perm_perm_public_memory_prod: felt252, + range_check16_perm_public_memory_prod: felt252, + diluted_check_first_elm: felt252, + diluted_check_permutation_public_memory_prod: felt252, + diluted_check_final_cum_val: felt252, + // Dynamic params. + dynamic_params: Span, +} + +// 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. +#[derive(Drop, Copy, PartialEq, Serde)] +struct InteractionElements { + memory_multi_column_perm_perm_interaction_elm: felt252, + memory_multi_column_perm_hash_interaction_elm0: felt252, + range_check16_perm_interaction_elm: felt252, + diluted_check_permutation_interaction_elm: felt252, + diluted_check_interaction_z: felt252, + diluted_check_interaction_alpha: felt252, + add_mod_interaction_elm: felt252, + mul_mod_interaction_elm: felt252, +} diff --git a/src/air/layouts/dynamic/public_input.cairo b/src/air/layouts/dynamic/public_input.cairo new file mode 100644 index 000000000..4fe073360 --- /dev/null +++ b/src/air/layouts/dynamic/public_input.cairo @@ -0,0 +1,124 @@ +use cairo_verifier::{ + common::{ + math::{pow, Felt252PartialOrd, Felt252Div}, + asserts::{assert_range_u128_le, assert_range_u128}, + }, + air::{ + public_memory::{Page, PageTrait}, + constants::{MAX_ADDRESS, INITIAL_PC, MAX_LOG_N_STEPS, MAX_RANGE_CHECK}, + layouts::dex::constants::{ + segments, get_builtins, CPU_COMPONENT_HEIGHT, CPU_COMPONENT_STEP, LAYOUT_CODE, + PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, ECDSA_BUILTIN_ROW_RATIO + }, + public_input::{PublicInput, PublicInputTrait, verify_cairo1_public_input} + }, + domains::StarkDomains +}; + +use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Hash}}; +use poseidon::poseidon_hash_span; + +impl DexPublicInputImpl of PublicInputTrait { + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) { + let public_segments = self.segments; + + let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; + let final_pc = *public_segments.at(segments::PROGRAM).stop_ptr; + let initial_ap = *public_segments.at(segments::EXECUTION).begin_addr; + let initial_fp = initial_ap; + let final_ap = *public_segments.at(segments::EXECUTION).stop_ptr; + let output_start = *public_segments.at(segments::OUTPUT).begin_addr; + let output_stop = *public_segments.at(segments::OUTPUT).stop_ptr; + + assert(initial_ap < MAX_ADDRESS, 'Invalid initial_ap'); + assert(final_ap < MAX_ADDRESS, 'Invalid final_ap'); + + // TODO support more pages? + assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers'); + + let builtins = get_builtins(); + let memory = self.main_page; + + // 1. Program segment + assert(initial_pc == INITIAL_PC, 'Invalid initial_pc'); + assert(final_pc == INITIAL_PC + 4, 'Invalid final_pc'); + + let mut memory_index: usize = 0; + + let program_end_pc = initial_fp - 2; + let program_len = program_end_pc - initial_pc; + let program = memory + .extract_range( + initial_pc.try_into().unwrap(), program_len.try_into().unwrap(), ref memory_index + ); + + assert( + *program[0] == 0x40780017fff7fff, 'Invalid program' + ); // Instruction: ap += N_BUILTINS. + assert(*program[1] == builtins.len().into(), 'Invalid program'); + assert(*program[2] == 0x1104800180018000, 'Invalid program'); // Instruction: call rel ?. + assert(*program[4] == 0x10780017fff7fff, 'Invalid program'); // Instruction: jmp rel 0. + assert(*program[5] == 0x0, 'Invalid program'); + + let program_hash = poseidon_hash_span(program); + + // 2. Execution segment + // 2.1 Initial_fp, initial_pc + let fp2 = *memory.at(memory_index); + assert(fp2.address == initial_fp - 2, 'Invalid fp2 addr'); + assert(fp2.value == initial_fp, 'Invalid fp2 val'); + + let fp1 = *memory.at(memory_index + 1); + assert(fp1.address == initial_fp - 1, 'Invalid fp1 addr'); + assert(fp1.value == 0, 'Invalid fp1 val'); + memory_index += 2; + + // 2.2 Main arguments and return values + let mut begin_addresses = ArrayTrait::new(); + let mut stop_addresses = ArrayTrait::new(); + let mut i = 0; + let builtins_len = builtins.len(); + loop { + if i == builtins_len { + break; + } + + begin_addresses.append(*public_segments.at(2 + i).begin_addr); + stop_addresses.append(*public_segments.at(2 + i).stop_ptr); + + i += 1; + }; + memory.verify_stack(initial_ap, begin_addresses.span(), builtins_len, ref memory_index); + memory + .verify_stack( + final_ap - builtins_len.into(), + stop_addresses.span(), + builtins_len, + ref memory_index + ); + + // 3. Output segment + let output_len = output_stop - output_start; + let output = memory + .extract_range( + output_start.try_into().unwrap(), output_len.try_into().unwrap(), ref memory_index + ); + let output_hash = poseidon_hash_span(output); + + // Check main page len + assert( + *memory.at(memory_index - 1) == *self.main_page.at(self.main_page.len() - 1), + 'Invalid main page len' + ); + + (program_hash, output_hash) + } + + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) { + verify_cairo1_public_input(self) + } + + fn validate(self: @PublicInput, stark_domains: @StarkDomains) {// TODO REWRITE + } +} + diff --git a/src/air/layouts/dynamic/traces.cairo b/src/air/layouts/dynamic/traces.cairo new file mode 100644 index 000000000..d7d624866 --- /dev/null +++ b/src/air/layouts/dynamic/traces.cairo @@ -0,0 +1,119 @@ +use cairo_verifier::{ + air::layouts::dex::{ + constants::{NUM_COLUMNS_FIRST, NUM_COLUMNS_SECOND}, global_values::InteractionElements, + }, + channel::channel::{Channel, ChannelTrait}, + table_commitment::table_commitment::{ + TableCommitment, TableDecommitment, TableCommitmentWitness, table_commit, table_decommit, + TableCommitmentConfig + }, + vector_commitment::vector_commitment::VectorCommitmentConfigTrait, + common::asserts::assert_in_range +}; + +// A protocol component (see stark.cairo for details about protocol components) for the traces +// of the CPU AIR. +// This component is commonly right before the FRI component. +// In this case: +// n_queries = n_fri_queries * 2^first_fri_step. +// decommitment.original.n_queries = n_original_columns * n_queries. +// decommitment.interaction.n_queries = n_interaction_columns * n_queries. + +// Commitment values for the Traces component. Used to generate a commitment by "reading" these +// values from the channel. +#[derive(Drop, Copy, Serde)] +struct TracesUnsentCommitment { + original: felt252, + interaction: felt252, +} + +// Commitment for the Traces component. +#[derive(Drop, PartialEq, Serde)] +struct TracesCommitment { + // Commitment to the first trace. + original: TableCommitment, + // The interaction elements that were sent to the prover after the first trace commitment (e.g. + // memory interaction). + interaction_elements: InteractionElements, + // Commitment to the second (interaction) trace. + interaction: TableCommitment, +} + +// Responses for queries to the AIR commitment. +// The queries are usually generated by the next component down the line (e.g. FRI). +#[derive(Drop, Copy, Serde)] +struct TracesDecommitment { + // Responses for queries to the original trace. + original: TableDecommitment, + // Responses for queries to the interaction trace. + interaction: TableDecommitment, +} + +// A witness for a decommitment of the AIR traces over queries. +#[derive(Drop, Copy, Serde)] +struct TracesWitness { + original: TableCommitmentWitness, + interaction: TableCommitmentWitness, +} + +const MAX_N_COLUMNS: felt252 = 128; + +// Configuration for the Traces component. +#[derive(Drop, Copy, Serde)] +struct TracesConfig { + original: TableCommitmentConfig, + interaction: TableCommitmentConfig, +} + +#[generate_trait] +impl TracesConfigImpl of TracesConfigTrait { + fn validate( + self: @TracesConfig, + log_eval_domain_size: felt252, + n_verifier_friendly_commitment_layers: felt252, + ) {// TODO REWRITE + } +} + +// Reads the traces commitment from the channel. +// Returns the commitment, along with GlobalValue required to evaluate the constraint polynomial. +fn traces_commit( + ref channel: Channel, unsent_commitment: TracesUnsentCommitment, config: TracesConfig +) -> TracesCommitment { + // TODO REWRITE + + // Read original commitment. + let original_commitment = table_commit( + ref channel, unsent_commitment.original, config.original + ); + // Generate interaction elements for the first interaction. + let interaction_elements = InteractionElements { + memory_multi_column_perm_perm_interaction_elm: channel.random_felt_to_prover(), + memory_multi_column_perm_hash_interaction_elm0: channel.random_felt_to_prover(), + range_check16_perm_interaction_elm: channel.random_felt_to_prover(), + }; + // Read interaction commitment. + let interaction_commitment = table_commit( + ref channel, unsent_commitment.interaction, config.interaction + ); + + TracesCommitment { + original: original_commitment, + interaction_elements: interaction_elements, + interaction: interaction_commitment, + } +} + +// Verifies a decommitment for the traces at the query indices. +// decommitment - holds the commited values of the leaves at the query_indices. +fn traces_decommit( + queries: Span, + commitment: TracesCommitment, + decommitment: TracesDecommitment, + witness: TracesWitness, +) { + // TODO REWRITE + + table_decommit(commitment.original, queries, decommitment.original, witness.original); + table_decommit(commitment.interaction, queries, decommitment.interaction, witness.interaction) +}