diff --git a/src/air/constants.cairo b/src/air/constants.cairo index c59b88035..800936c56 100644 --- a/src/air/constants.cairo +++ b/src/air/constants.cairo @@ -41,3 +41,15 @@ mod segments { const PROGRAM: usize = 0; const RANGE_CHECK: usize = 4; } + +// Pedersen builtin +const SHIFT_POINT_X: felt252 = 0x49ee3eba8c1600700ee1b87eb599f16716b0b1022947733551fde4050ca6804; +const SHIFT_POINT_Y: felt252 = 0x3ca0cfe4b3bc6ddf346d49d06ea0ed34e621062c0e056c1d0405d266e10268a; + +const SECURITY_BITS: felt252 = 128; +const MAX_ADDRESS: felt252 = 0xffffffffffffffff; +const INITIAL_PC: felt252 = 1; + +fn get_builtins() -> Array { + array!['output', 'pedersen', 'range_check', 'bitwise'] +} diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 5a165380c..71c1c66f7 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -9,11 +9,15 @@ use cairo_verifier::{ public_memory::{ Page, PageTrait, ContinuousPageHeader, get_continuous_pages_product, AddrValueSize }, - constants + 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 + domains::StarkDomains, common::hash::hash_felts }; + #[derive(Drop, Copy, PartialEq)] struct SegmentInfo { // Start address of the memory segment. @@ -155,35 +159,120 @@ impl PublicInputImpl of PublicInputTrait { (prod, total_length) } - fn validate(self: @PublicInput, domains: @StarkDomains) { - assert_range_u128_le(*self.log_n_steps, constants::MAX_LOG_N_STEPS); - let n_steps = pow(2, *self.log_n_steps); + 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()); + memory_index += program.len().into(); + assert( - n_steps * constants::CPU_COMPONENT_HEIGHT == *domains.trace_domain_size, - 'Wrong trace size' + *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 + memory + .verify_stack( + initial_ap, *public_segments.at(2).begin_addr, builtins.span(), memory_index.into() + ); + memory_index += builtins.len(); + + memory + .verify_stack( + final_ap - builtins.len().into(), + *public_segments.at(2).stop_ptr, + builtins.span(), + memory_index.into() + ); + memory_index += builtins.len(); + + // 3. Output segment + let output_len = output_stop - output_start; + let output = memory + .extract_range( + memory_index + output_start.try_into().unwrap(), output_len.try_into().unwrap() + ); + memory_index += output.len().into(); + let output_hash = hash_felts(output); + + // Check main page len + assert( + *memory.at(memory_index) == *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 <= constants::MAX_RANGE_CHECK, 'wrong rc_max'); + assert(*self.rc_max <= MAX_RANGE_CHECK, 'wrong rc_max'); - assert(*self.layout == constants::LAYOUT_CODE, 'wrong layout code'); + assert(*self.layout == LAYOUT_CODE, 'wrong layout code'); - let pedersen_copies = n_steps / constants::PEDERSEN_BUILTIN_RATIO; - let pedersen_uses = (*self.segments.at(constants::segments::PEDERSEN).stop_ptr - - *self.segments.at(constants::segments::PEDERSEN).begin_addr) + 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 / constants::RC_BUILTIN_RATIO; - let range_check_uses = *self.segments.at(constants::segments::RANGE_CHECK).stop_ptr - - *self.segments.at(constants::segments::RANGE_CHECK).begin_addr; + 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 / constants::BITWISE_RATIO; - let bitwise_uses = (*self.segments.at(constants::segments::BITWISE).stop_ptr - - *self.segments.at(constants::segments::BITWISE).begin_addr) + 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/air/public_memory.cairo b/src/air/public_memory.cairo index c9258917f..bef35475d 100644 --- a/src/air/public_memory.cairo +++ b/src/air/public_memory.cairo @@ -44,6 +44,48 @@ impl PageImpl of PageTrait { i += 1; } } + + fn extract_range(self: @Page, addr: u32, len: usize) -> Span { + let mut arr = ArrayTrait::new(); + let mut i = 0; + + loop { + if i == len { + break arr.span(); + } + + let current = *self.at(addr + i); + + // 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; + } + } + + fn verify_stack( + self: @Page, + start_ap: felt252, + segment_address: felt252, + builtins: Span, + memory_index: felt252 + ) { + let mut i = 0; + + // TODO size of SegmentInfo + let size = 2; + loop { + if i == builtins.len() { + break; + } + + let current = *self.at(memory_index.try_into().unwrap() + i); + + assert(current.address == start_ap + i.into(), 'Invalid address'); + assert(current.value == segment_address + size * (i.into() + 1), 'Invalid builtin'); + i += 1; + }; + } } fn get_continuous_pages_product(page_headers: Span) -> (felt252, felt252) { diff --git a/src/common.cairo b/src/common.cairo index 3e58a86b7..85a5f897e 100644 --- a/src/common.cairo +++ b/src/common.cairo @@ -11,6 +11,7 @@ mod flip_endianness; mod from_span; mod horner_eval; mod math; +mod hash; mod merge_sort; mod powers_array; diff --git a/src/common/hash.cairo b/src/common/hash.cairo new file mode 100644 index 000000000..8981c23a7 --- /dev/null +++ b/src/common/hash.cairo @@ -0,0 +1,15 @@ +use pedersen::PedersenTrait; +use hash::HashStateTrait; + +fn hash_felts(s: Span) -> felt252 { + let mut hash_state = PedersenTrait::new(0); + let mut i = 0; + + loop { + if i == s.len() { + break hash_state.finalize(); + } + + hash_state.update(*s.at(i)); + } +}