diff --git a/runner/src/main.rs b/runner/src/main.rs index 1a4ff0cfd..27d3f6209 100644 --- a/runner/src/main.rs +++ b/runner/src/main.rs @@ -59,13 +59,9 @@ fn main() -> anyhow::Result<()> { let func = runner.find_function(function).unwrap(); let proof_arg = Arg::Array(proof.into_iter().map(Arg::Value).collect_vec()); let cairo_version_arg = Arg::Value(cli.cairo_version.into()); + let args = &[proof_arg, cairo_version_arg]; let result = runner - .run_function_with_starknet_context( - func, - &[proof_arg, cairo_version_arg], - Some(u32::MAX as usize), - Default::default(), - ) + .run_function_with_starknet_context(func, args, Some(u32::MAX as usize), Default::default()) .unwrap(); // let profiling_processor = // ProfilingInfoProcessor::new(None, sierra_program.program, UnorderedHashMap::default()); diff --git a/src/air/layouts/dex/public_input.cairo b/src/air/layouts/dex/public_input.cairo index 0d7c5ce70..c513487e2 100644 --- a/src/air/layouts/dex/public_input.cairo +++ b/src/air/layouts/dex/public_input.cairo @@ -10,7 +10,7 @@ use cairo_verifier::{ 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::{CairoVersion, PublicInput, PublicInputTrait} + public_input::{PublicInput, PublicInputTrait} }, domains::StarkDomains }; @@ -19,7 +19,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has use poseidon::poseidon_hash_span; impl DexPublicInputImpl of PublicInputTrait { - fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) { + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) { let public_segments = self.segments; let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; @@ -114,6 +114,10 @@ impl DexPublicInputImpl of PublicInputTrait { (program_hash, output_hash) } + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) { + panic!("Not implemented") + } + fn validate(self: @PublicInput, stark_domains: @StarkDomains) { assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS); let n_steps = pow(2, *self.log_n_steps); diff --git a/src/air/layouts/recursive/public_input.cairo b/src/air/layouts/recursive/public_input.cairo index ad8e71750..b4778169f 100644 --- a/src/air/layouts/recursive/public_input.cairo +++ b/src/air/layouts/recursive/public_input.cairo @@ -10,7 +10,7 @@ use cairo_verifier::{ segments, get_builtins, CPU_COMPONENT_HEIGHT, CPU_COMPONENT_STEP, LAYOUT_CODE, PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO }, - public_input::{CairoVersion, PublicInput, PublicInputTrait} + public_input::{PublicInput, PublicInputTrait} }, domains::StarkDomains }; @@ -19,7 +19,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has use poseidon::poseidon_hash_span; impl RecursivePublicInputImpl of PublicInputTrait { - fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) { + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) { let public_segments = self.segments; let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; @@ -39,66 +39,63 @@ impl RecursivePublicInputImpl of PublicInputTrait { let builtins = get_builtins(); let memory = self.main_page; - let offset = match cairo_version { - CairoVersion::Cairo0 => 0, - CairoVersion::Cairo1 => 1, - }; - // 1. Program segment assert(initial_pc == INITIAL_PC, 'Invalid initial_pc'); - assert(final_pc == INITIAL_PC + 4 + offset, 'Invalid final_pc'); + assert(final_pc == INITIAL_PC + 4, 'Invalid final_pc'); let mut memory_index: usize = 0; - let program_end_pc = initial_fp - (2 + offset); + 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 ); - if cairo_version == CairoVersion::Cairo0 { - // Instruction: ap += N_BUILTINS. - assert(*program[0] == 0x40780017fff7fff, 'Invalid program'); - assert(*program[1] == builtins.len().into(), 'Invalid program'); - // Instruction: call rel ?. - assert(*program[2] == 0x1104800180018000, 'Invalid program'); - // Instruction: jmp rel 0. - assert(*program[4] == 0x10780017fff7fff, 'Invalid program'); - assert(*program[5] == 0x0, 'Invalid 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 = array![]; - let mut stop_addresses = array![]; - let mut i = 0; - let builtins_len = builtins.len(); - while i != builtins_len { - let segment = *public_segments.at(2 + i); - begin_addresses.append(segment.begin_addr); - stop_addresses.append(segment.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 - ); - } + 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; @@ -106,18 +103,40 @@ impl RecursivePublicInputImpl of PublicInputTrait { .extract_range( output_start.try_into().unwrap(), output_len.try_into().unwrap(), ref memory_index ); + let output_hash = poseidon_hash_span(output); - if cairo_version == CairoVersion::Cairo0 { - // Check main page len - assert( - *memory.at(memory_index - 1) == *memory.at(memory.len() - 1), - 'Invalid main page len' - ); - } + // Check main page len + assert( + *memory.at(memory_index - 1) == *memory.at(memory.len() - 1), 'Invalid main page len' + ); + + (program_hash, output_hash) + } + + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) { + let public_segments = self.segments; + let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; + let initial_ap = *public_segments.at(segments::EXECUTION).begin_addr; + 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; + let output_len: u32 = (output_stop - output_start).try_into().unwrap(); + + assert(initial_ap < MAX_ADDRESS, 'Invalid initial_ap'); + assert(final_ap < MAX_ADDRESS, 'Invalid final_ap'); + assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers'); + let memory = self.main_page; + + // 1. Program segment + assert(initial_pc == INITIAL_PC, 'Invalid initial_pc'); + let program = memory + .extract_range_unchecked(initial_pc.try_into().unwrap(), memory.len() - output_len); let program_hash = poseidon_hash_span(program); - let output_hash = poseidon_hash_span(output); + // 2. Output segment + let output = memory.extract_range_unchecked(memory.len() - output_len, output_len); + let output_hash = poseidon_hash_span(output); (program_hash, output_hash) } diff --git a/src/air/layouts/recursive_with_poseidon/public_input.cairo b/src/air/layouts/recursive_with_poseidon/public_input.cairo index 91e25671b..20e7837a1 100644 --- a/src/air/layouts/recursive_with_poseidon/public_input.cairo +++ b/src/air/layouts/recursive_with_poseidon/public_input.cairo @@ -11,7 +11,7 @@ use cairo_verifier::{ PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO, POSEIDON_ROW_RATIO }, - public_input::{CairoVersion, PublicInput, PublicInputTrait} + public_input::{PublicInput, PublicInputTrait} }, domains::StarkDomains }; @@ -20,7 +20,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has use poseidon::poseidon_hash_span; impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait { - fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) { + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) { let public_segments = self.segments; let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; @@ -115,6 +115,10 @@ impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait { (program_hash, output_hash) } + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) { + panic!("Not implemented") + } + fn validate(self: @PublicInput, stark_domains: @StarkDomains) { assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS); let n_steps = pow(2, *self.log_n_steps); diff --git a/src/air/layouts/small/public_input.cairo b/src/air/layouts/small/public_input.cairo index 82a655868..ad7106239 100644 --- a/src/air/layouts/small/public_input.cairo +++ b/src/air/layouts/small/public_input.cairo @@ -10,7 +10,7 @@ use cairo_verifier::{ 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::{CairoVersion, PublicInput, PublicInputTrait} + public_input::{PublicInput, PublicInputTrait} }, domains::StarkDomains }; @@ -19,7 +19,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has use poseidon::poseidon_hash_span; impl SmallPublicInputImpl of PublicInputTrait { - fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) { + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) { let public_segments = self.segments; let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; @@ -114,6 +114,10 @@ impl SmallPublicInputImpl of PublicInputTrait { (program_hash, output_hash) } + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) { + panic!("Not implemented") + } + fn validate(self: @PublicInput, stark_domains: @StarkDomains) { assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS); let n_steps = pow(2, *self.log_n_steps); diff --git a/src/air/layouts/starknet/public_input.cairo b/src/air/layouts/starknet/public_input.cairo index 4297659ad..25905ea57 100644 --- a/src/air/layouts/starknet/public_input.cairo +++ b/src/air/layouts/starknet/public_input.cairo @@ -11,7 +11,7 @@ use cairo_verifier::{ PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO, ECDSA_BUILTIN_ROW_RATIO, EC_OP_BUILTIN_ROW_RATIO, POSEIDON_ROW_RATIO }, - public_input::{CairoVersion, PublicInput, PublicInputTrait} + public_input::{PublicInput, PublicInputTrait} }, domains::StarkDomains }; @@ -20,7 +20,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has use poseidon::poseidon_hash_span; impl StarknetPublicInputImpl of PublicInputTrait { - fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) { + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) { let public_segments = self.segments; let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; @@ -115,6 +115,10 @@ impl StarknetPublicInputImpl of PublicInputTrait { (program_hash, output_hash) } + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) { + panic!("Not implemented") + } + fn validate(self: @PublicInput, stark_domains: @StarkDomains) { assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS); let n_steps = pow(2, *self.log_n_steps); diff --git a/src/air/layouts/starknet_with_keccak/public_input.cairo b/src/air/layouts/starknet_with_keccak/public_input.cairo index b1e0f3baa..2641c2782 100644 --- a/src/air/layouts/starknet_with_keccak/public_input.cairo +++ b/src/air/layouts/starknet_with_keccak/public_input.cairo @@ -11,7 +11,7 @@ use cairo_verifier::{ PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO, ECDSA_BUILTIN_ROW_RATIO, EC_OP_BUILTIN_ROW_RATIO, POSEIDON_ROW_RATIO, KECCAK_ROW_RATIO }, - public_input::{CairoVersion, PublicInput, PublicInputTrait} + public_input::{PublicInput, PublicInputTrait} }, domains::StarkDomains }; @@ -20,7 +20,7 @@ use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Has use poseidon::poseidon_hash_span; impl StarknetWithKeccakPublicInputImpl of PublicInputTrait { - fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252) { + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252) { let public_segments = self.segments; let initial_pc = *public_segments.at(segments::PROGRAM).begin_addr; @@ -115,6 +115,10 @@ impl StarknetWithKeccakPublicInputImpl of PublicInputTrait { (program_hash, output_hash) } + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252) { + panic!("Not implemented") + } + fn validate(self: @PublicInput, stark_domains: @StarkDomains) { assert_range_u128_le(*self.log_n_steps, MAX_LOG_N_STEPS); let n_steps = pow(2, *self.log_n_steps); diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 92154aa90..623a0cef7 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -41,7 +41,8 @@ enum CairoVersion { } trait PublicInputTrait { - fn verify(self: @PublicInput, cairo_version: CairoVersion) -> (felt252, felt252); + fn verify_cairo0(self: @PublicInput) -> (felt252, felt252); + fn verify_cairo1(self: @PublicInput) -> (felt252, felt252); fn validate(self: @PublicInput, stark_domains: @StarkDomains); } diff --git a/src/air/public_memory.cairo b/src/air/public_memory.cairo index 504395ce1..0e8ab0aeb 100644 --- a/src/air/public_memory.cairo +++ b/src/air/public_memory.cairo @@ -11,7 +11,7 @@ type Page = Array; // 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])). +// 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 @@ -64,6 +64,17 @@ impl PageImpl of PageTrait { } } + fn extract_range_unchecked(self: @Page, addr: u32, len: usize) -> Span { + let mut arr = ArrayTrait::new(); + let mut slice = self.span().slice(addr, len); + while !slice + .is_empty() { + let current = *slice.pop_front().unwrap(); + arr.append(current.value); + }; + arr.span() + } + fn verify_stack( self: @Page, start_ap: felt252, diff --git a/src/lib.cairo b/src/lib.cairo index 4bff68054..5553d0c7f 100644 --- a/src/lib.cairo +++ b/src/lib.cairo @@ -48,7 +48,10 @@ fn main(mut serialized: Span, cairo_version: CairoVersion) -> (felt252, let stark_proof: StarkProof = stark_proof_serde.into(); stark_proof.verify(SECURITY_BITS); - let (program_hash, output_hash) = stark_proof.public_input.verify(cairo_version); + let (program_hash, output_hash) = match cairo_version { + CairoVersion::Cairo0 => stark_proof.public_input.verify_cairo0(), + CairoVersion::Cairo1 => stark_proof.public_input.verify_cairo1(), + }; (program_hash, output_hash) }