diff --git a/src/abstract_air.cairo b/src/abstract_air.cairo index e700f285c..e21a5bbea 100644 --- a/src/abstract_air.cairo +++ b/src/abstract_air.cairo @@ -1,2 +1,4 @@ mod layouts; mod pedersen; +mod diluted; +mod public_memory; diff --git a/src/abstract_air/diluted.cairo b/src/abstract_air/diluted.cairo new file mode 100644 index 000000000..d5ef55b5f --- /dev/null +++ b/src/abstract_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 - 1 { + 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/abstract_air/layouts/recursive.cairo b/src/abstract_air/layouts/recursive.cairo index 2cedbb1dc..1549f8959 100644 --- a/src/abstract_air/layouts/recursive.cairo +++ b/src/abstract_air/layouts/recursive.cairo @@ -1,3 +1,5 @@ mod autogenerated; mod constants; mod global_values; +mod public_input; +mod traces; diff --git a/src/abstract_air/layouts/recursive/public_input.cairo b/src/abstract_air/layouts/recursive/public_input.cairo new file mode 100644 index 000000000..0ce47383e --- /dev/null +++ b/src/abstract_air/layouts/recursive/public_input.cairo @@ -0,0 +1,285 @@ +use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Hash}}; +use cairo_verifier::{ + common::{ + flip_endianness::FlipEndiannessTrait, array_append::ArrayAppendTrait, blake2s::blake2s, + math::{pow, Felt252PartialOrd, Felt252Div}, asserts::assert_range_u128_le, + array_print::SpanPrintTrait, hash::hash_felts, + }, + abstract_air::{ + public_memory::{ + Page, PageTrait, ContinuousPageHeader, get_continuous_pages_product, AddrValueSize + }, + layouts::recursive::constants::{ + segments, MAX_ADDRESS, get_builtins, INITIAL_PC, MAX_LOG_N_STEPS, CPU_COMPONENT_HEIGHT, + MAX_RANGE_CHECK, LAYOUT_CODE, PEDERSEN_BUILTIN_RATIO, RC_BUILTIN_RATIO, BITWISE_RATIO + } + }, + domains::StarkDomains +}; + +#[derive(Drop, Copy, PartialEq)] +struct SegmentInfo { + // Start address of the memory segment. + begin_addr: felt252, + // Stop pointer of the segment - not necessarily the end of the segment. + stop_ptr: felt252, +} + +#[derive(Drop, PartialEq)] +struct PublicInput { + log_n_steps: felt252, + rc_min: felt252, + rc_max: felt252, + layout: felt252, + dynamic_params: Array, + segments: Array, + padding_addr: felt252, + padding_value: felt252, + main_page: Page, + continuous_page_headers: Array +} + +#[generate_trait] +impl PublicInputImpl of PublicInputTrait { + // Computes the hash of the public input, which is used as the initial seed for the Fiat-Shamir heuristic. + fn get_public_input_hash(self: @PublicInput) -> u256 { + // Main page hash. + let mut main_page_hash_state = PedersenTrait::new(0); + let mut i: u32 = 0; + loop { + if i == self.main_page.len() { + break; + } + main_page_hash_state = main_page_hash_state.update_with(*self.main_page.at(i)); + i += 1; + }; + main_page_hash_state = main_page_hash_state + .update_with(AddrValueSize * self.main_page.len()); + let main_page_hash = main_page_hash_state.finalize(); + + let mut hash_data = ArrayTrait::::new(); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, (*self.log_n_steps).into()); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, (*self.rc_min).into()); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, (*self.rc_max).into()); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, (*self.layout).into()); + + // Dynamic params. + let mut i: u32 = 0; + loop { + if i == self.dynamic_params.len() { + break; + } + + ArrayAppendTrait::< + _, u256 + >::append_big_endian(ref hash_data, (*self.dynamic_params.at(i)).into()); + + i += 1; + }; + + // Segments. + let mut i: u32 = 0; + loop { + if i == self.segments.len() { + break; + } + + let segment = *self.segments.at(i); + ArrayAppendTrait::< + _, u256 + >::append_big_endian(ref hash_data, segment.begin_addr.into()); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, segment.stop_ptr.into()); + + i += 1; + }; + + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, (*self.padding_addr).into()); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, (*self.padding_value).into()); + hash_data + .append_big_endian(Into::::into(1 + self.continuous_page_headers.len())); + + // Main page. + hash_data.append_big_endian(Into::<_, u256>::into(self.main_page.len())); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, main_page_hash.into()); + + // Add the rest of the pages. + let mut i: u32 = 0; + loop { + if i == self.continuous_page_headers.len() { + break; + } + + let continuous_page = *self.continuous_page_headers.at(i); + ArrayAppendTrait::< + _, u256 + >::append_big_endian(ref hash_data, continuous_page.start_address.into()); + ArrayAppendTrait::< + _, u256 + >::append_big_endian(ref hash_data, continuous_page.size.into()); + ArrayAppendTrait::<_, u256>::append_big_endian(ref hash_data, continuous_page.hash); + + i += 1; + }; + + blake2s(hash_data).flip_endianness() + } + + // Returns the ratio between the product of all public memory cells and z^|public_memory|. + // This is the value that needs to be at the memory__multi_column_perm__perm__public_memory_prod + // member expression. + fn get_public_memory_product_ratio( + self: @PublicInput, z: felt252, alpha: felt252, public_memory_column_size: felt252 + ) -> felt252 { + let (pages_product, total_length) = self.get_public_memory_product(z, alpha); + + // Pad and divide + let numerator = pow(z, public_memory_column_size); + let padded = z - (*self.padding_addr + alpha * *self.padding_value); + + assert(total_length <= public_memory_column_size, 'Invalid length'); + let denominator_pad = pow(padded, public_memory_column_size - total_length); + + numerator / pages_product / denominator_pad + } + + // Returns the product of all public memory cells. + fn get_public_memory_product( + self: @PublicInput, z: felt252, alpha: felt252 + ) -> (felt252, felt252) { + let main_page_prod = self.main_page.get_product(z, alpha); + + let (continuous_pages_prod, continuous_pages_total_length) = get_continuous_pages_product( + self.continuous_page_headers.span(), + ); + + let prod = main_page_prod * continuous_pages_prod; + let total_length = (self.main_page.len()).into() + continuous_pages_total_length; + + (prod, total_length) + } + + fn verify(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 = hash_felts(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 = hash_felts(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 validate(self: @PublicInput, domains: @StarkDomains) { + assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS); + let n_steps = pow(2, *self.log_n_steps); + assert(n_steps * CPU_COMPONENT_HEIGHT == *domains.trace_domain_size, 'Wrong trace size'); + + assert(0 <= *self.rc_min, 'wrong rc_min'); + assert(*self.rc_min < *self.rc_max, 'wrong rc range'); + assert(*self.rc_max <= MAX_RANGE_CHECK, 'wrong rc_max'); + + assert(*self.layout == LAYOUT_CODE, 'wrong layout code'); + + let pedersen_copies = n_steps / PEDERSEN_BUILTIN_RATIO; + let pedersen_uses = (*self.segments.at(segments::PEDERSEN).stop_ptr + - *self.segments.at(segments::PEDERSEN).begin_addr) + / 3; + assert_range_u128_le(pedersen_uses, pedersen_copies); + + let range_check_copies = n_steps / RC_BUILTIN_RATIO; + let range_check_uses = *self.segments.at(segments::RANGE_CHECK).stop_ptr + - *self.segments.at(segments::RANGE_CHECK).begin_addr; + assert_range_u128_le(range_check_uses, range_check_copies); + + let bitwise_copies = n_steps / BITWISE_RATIO; + let bitwise_uses = (*self.segments.at(segments::BITWISE).stop_ptr + - *self.segments.at(segments::BITWISE).begin_addr) + / 5; + assert_range_u128_le(bitwise_uses, bitwise_copies); + } +} + diff --git a/src/abstract_air/layouts/recursive/traces.cairo b/src/abstract_air/layouts/recursive/traces.cairo new file mode 100644 index 000000000..208986c23 --- /dev/null +++ b/src/abstract_air/layouts/recursive/traces.cairo @@ -0,0 +1,137 @@ +use cairo_verifier::{ + air::{ + public_input::PublicInput, 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)] +struct TracesUnsentCommitment { + original: felt252, + interaction: felt252, +} + +// Commitment for the Traces component. +#[derive(Drop, PartialEq)] +struct TracesCommitment { + public_input: @PublicInput, + // 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)] +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)] +struct TracesWitness { + original: TableCommitmentWitness, + interaction: TableCommitmentWitness, +} + +const MAX_N_COLUMNS: felt252 = 128; +const AIR_LAYOUT_N_ORIGINAL_COLUMNS: felt252 = 12; +const AIR_LAYOUT_N_INTERACTION_COLUMNS: felt252 = 3; + +// Configuration for the Traces component. +#[derive(Drop, Copy)] +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, + ) { + assert_in_range(*self.original.n_columns, 1, MAX_N_COLUMNS + 1); + assert_in_range(*self.interaction.n_columns, 1, MAX_N_COLUMNS + 1); + assert(*self.original.n_columns == NUM_COLUMNS_FIRST.into(), 'Wrong number of columns'); + assert(*self.interaction.n_columns == NUM_COLUMNS_SECOND.into(), 'Wrong number of columns'); + + self.original.vector.validate(log_eval_domain_size, n_verifier_friendly_commitment_layers); + + self + .interaction + .vector + .validate(log_eval_domain_size, n_verifier_friendly_commitment_layers); + } +} + +// 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, + public_input: @PublicInput, + unsent_commitment: TracesUnsentCommitment, + config: TracesConfig +) -> TracesCommitment { + // 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(), + rc16_perm_interaction_elm: channel.random_felt_to_prover(), + diluted_check_permutation_interaction_elm: channel.random_felt_to_prover(), + diluted_check_interaction_z: channel.random_felt_to_prover(), + diluted_check_interaction_alpha: channel.random_felt_to_prover(), + }; + // Read interaction commitment. + let interaction_commitment = table_commit( + ref channel, unsent_commitment.interaction, config.interaction + ); + + TracesCommitment { + public_input: public_input, + 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, +) { + table_decommit(commitment.original, queries, decommitment.original, witness.original); + table_decommit(commitment.interaction, queries, decommitment.interaction, witness.interaction) +} diff --git a/src/abstract_air/public_memory.cairo b/src/abstract_air/public_memory.cairo new file mode 100644 index 000000000..2795eaaaa --- /dev/null +++ b/src/abstract_air/public_memory.cairo @@ -0,0 +1,109 @@ +#[derive(Drop, Copy, Hash, PartialEq)] +struct AddrValue { + address: felt252, + value: felt252 +} +const AddrValueSize: u32 = 2; + +type Page = Array; + +// Information about a continuous page (a consecutive section of the public memory).. +// Each such page must be verified externally to the verifier: +// hash = Hash( +// memory[start_address], memory[start_address + 1], ..., memory[start_address + size - 1]). +// prod = prod_i (z - ((start_address + i) + alpha * (memory[start_address + i])). +// z, alpha are taken from the interaction values, and can be obtained directly from the +// StarkProof object. +// z = interaction_elements.memory_multi_column_perm_perm__interaction_elm +// alpha = interaction_elements.memory_multi_column_perm_hash_interaction_elm0 +#[derive(Drop, Copy, PartialEq)] +struct ContinuousPageHeader { + // Start address. + start_address: felt252, + // Size of the page. + size: felt252, + // Hash of the page. + hash: u256, + // Cumulative product of the page. + prod: felt252, +} + +#[generate_trait] +impl PageImpl of PageTrait { + // Returns the product of (z - (addr + alpha * val)) over a single page. + fn get_product(self: @Page, z: felt252, alpha: felt252) -> felt252 { + let mut res = 1; + let mut i = 0; + loop { + if i == self.len() { + break res; + } + let current = self.at(i); + + res *= z - (*current.address + alpha * *current.value); + i += 1; + } + } + + fn extract_range(self: @Page, addr: u32, len: usize, ref offset: usize) -> Span { + let mut arr = ArrayTrait::new(); + let mut i = 0; + + loop { + if i == len { + break arr.span(); + } + + let current = *self.at(offset); + + // TODO is this needed? If not we can just use slice directly + assert(current.address == (addr + i).into(), 'Invalid address'); + arr.append(current.value); + i += 1; + offset += 1; + } + } + + fn verify_stack( + self: @Page, + start_ap: felt252, + segment_addresses: Span, + builtins_len: usize, + ref offset: usize + ) { + let mut i = 0; + + loop { + if i == builtins_len { + break; + } + + let current = *self.at(offset); + + assert(current.address == start_ap + i.into(), 'Invalid address'); + assert(current.value == *segment_addresses.at(i), 'Invalid builtin'); + i += 1; + offset += 1; + }; + } +} + +fn get_continuous_pages_product( + mut page_headers: Span +) -> (felt252, felt252) { + let mut res = 1; + let mut total_length = 0; + + loop { + match page_headers.pop_front() { + Option::Some(header) => { + res *= *header.prod; + total_length += *header.size; + }, + Option::None => { break; } + } + }; + + (res, total_length) +} +