diff --git a/src/air/layouts/recursive/public_input.cairo b/src/air/layouts/recursive/public_input.cairo index ab73b9456..ae1d0634a 100644 --- a/src/air/layouts/recursive/public_input.cairo +++ b/src/air/layouts/recursive/public_input.cairo @@ -1,3 +1,5 @@ +use core::array::ArrayTrait; +use core::traits::Into; use cairo_verifier::{ common::{ math::{pow, Felt252PartialOrd, Felt252Div}, @@ -10,7 +12,10 @@ 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::{PublicInput, PublicInputTrait, verify_cairo1_public_input} + public_input::{ + PublicInput, PublicInputTrait, verify_cairo1_public_input, + get_builtins as get_program_builtins + } }, domains::StarkDomains }; @@ -36,7 +41,8 @@ impl RecursivePublicInputImpl of PublicInputTrait { // TODO support more pages? assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers'); - let builtins = get_builtins(); + let layout_builtins = get_builtins(); + let program_builtins = get_program_builtins(); let memory = self.main_page; // 1. Program segment @@ -55,7 +61,7 @@ impl RecursivePublicInputImpl of PublicInputTrait { assert( *program[0] == 0x40780017fff7fff, 'Invalid program' ); // Instruction: ap += N_BUILTINS. - assert(*program[1] == builtins.len().into(), 'Invalid program'); + assert(*program[1] == program_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'); @@ -76,10 +82,10 @@ impl RecursivePublicInputImpl of PublicInputTrait { // 2.2 Main arguments and return values let mut begin_addresses = ArrayTrait::new(); let mut stop_addresses = ArrayTrait::new(); + let layout_builtins_len = layout_builtins.len(); let mut i = 0; - let builtins_len = builtins.len(); loop { - if i == builtins_len { + if i == layout_builtins_len { break; } @@ -88,12 +94,20 @@ impl RecursivePublicInputImpl of PublicInputTrait { i += 1; }; - memory.verify_stack(initial_ap, begin_addresses.span(), builtins_len, ref memory_index); memory .verify_stack( - final_ap - builtins_len.into(), + initial_ap, + begin_addresses.span(), + program_builtins.span(), + layout_builtins.span(), + ref memory_index + ); + memory + .verify_stack( + final_ap - program_builtins.len().into(), stop_addresses.span(), - builtins_len, + program_builtins.span(), + layout_builtins.span(), ref memory_index ); diff --git a/src/air/layouts/recursive_with_poseidon/public_input.cairo b/src/air/layouts/recursive_with_poseidon/public_input.cairo index 7f53bfa84..3c9c6d268 100644 --- a/src/air/layouts/recursive_with_poseidon/public_input.cairo +++ b/src/air/layouts/recursive_with_poseidon/public_input.cairo @@ -11,7 +11,10 @@ use cairo_verifier::{ PEDERSEN_BUILTIN_ROW_RATIO, RANGE_CHECK_BUILTIN_ROW_RATIO, BITWISE_ROW_RATIO, POSEIDON_ROW_RATIO }, - public_input::{PublicInput, PublicInputTrait, verify_cairo1_public_input} + public_input::{ + PublicInput, PublicInputTrait, verify_cairo1_public_input, + get_builtins as get_program_builtins + } }, domains::StarkDomains }; @@ -37,7 +40,8 @@ impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait { // TODO support more pages? assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers'); - let builtins = get_builtins(); + let layout_builtins = get_builtins(); + let program_builtins = get_program_builtins(); let memory = self.main_page; // 1. Program segment @@ -56,7 +60,7 @@ impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait { assert( *program[0] == 0x40780017fff7fff, 'Invalid program' ); // Instruction: ap += N_BUILTINS. - assert(*program[1] == builtins.len().into(), 'Invalid program'); + assert(*program[1] == program_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'); @@ -77,10 +81,10 @@ impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait { // 2.2 Main arguments and return values let mut begin_addresses = ArrayTrait::new(); let mut stop_addresses = ArrayTrait::new(); + let layout_builtins_len = layout_builtins.len(); let mut i = 0; - let builtins_len = builtins.len(); loop { - if i == builtins_len { + if i == layout_builtins_len { break; } @@ -89,12 +93,20 @@ impl RecursiveWithPoseidonPublicInputImpl of PublicInputTrait { i += 1; }; - memory.verify_stack(initial_ap, begin_addresses.span(), builtins_len, ref memory_index); memory .verify_stack( - final_ap - builtins_len.into(), + initial_ap, + begin_addresses.span(), + program_builtins.span(), + layout_builtins.span(), + ref memory_index + ); + memory + .verify_stack( + final_ap - program_builtins.len().into(), stop_addresses.span(), - builtins_len, + program_builtins.span(), + layout_builtins.span(), ref memory_index ); diff --git a/src/air/layouts/small/public_input.cairo b/src/air/layouts/small/public_input.cairo index 06dba89e7..9f36acff3 100644 --- a/src/air/layouts/small/public_input.cairo +++ b/src/air/layouts/small/public_input.cairo @@ -10,7 +10,10 @@ 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::{PublicInput, PublicInputTrait, verify_cairo1_public_input} + public_input::{ + PublicInput, PublicInputTrait, verify_cairo1_public_input, + get_builtins as get_program_builtins + } }, domains::StarkDomains }; @@ -36,7 +39,8 @@ impl SmallPublicInputImpl of PublicInputTrait { // TODO support more pages? assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers'); - let builtins = get_builtins(); + let layout_builtins = get_builtins(); + let program_builtins = get_program_builtins(); let memory = self.main_page; // 1. Program segment @@ -55,7 +59,7 @@ impl SmallPublicInputImpl of PublicInputTrait { assert( *program[0] == 0x40780017fff7fff, 'Invalid program' ); // Instruction: ap += N_BUILTINS. - assert(*program[1] == builtins.len().into(), 'Invalid program'); + assert(*program[1] == program_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'); @@ -76,10 +80,10 @@ impl SmallPublicInputImpl of PublicInputTrait { // 2.2 Main arguments and return values let mut begin_addresses = ArrayTrait::new(); let mut stop_addresses = ArrayTrait::new(); + let layout_builtins_len = layout_builtins.len(); let mut i = 0; - let builtins_len = builtins.len(); loop { - if i == builtins_len { + if i == layout_builtins_len { break; } @@ -88,12 +92,20 @@ impl SmallPublicInputImpl of PublicInputTrait { i += 1; }; - memory.verify_stack(initial_ap, begin_addresses.span(), builtins_len, ref memory_index); memory .verify_stack( - final_ap - builtins_len.into(), + initial_ap, + begin_addresses.span(), + program_builtins.span(), + layout_builtins.span(), + ref memory_index + ); + memory + .verify_stack( + final_ap - program_builtins.len().into(), stop_addresses.span(), - builtins_len, + program_builtins.span(), + layout_builtins.span(), ref memory_index ); diff --git a/src/air/layouts/starknet/public_input.cairo b/src/air/layouts/starknet/public_input.cairo index edfb424ec..ae0fccbc9 100644 --- a/src/air/layouts/starknet/public_input.cairo +++ b/src/air/layouts/starknet/public_input.cairo @@ -11,7 +11,10 @@ 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::{PublicInput, PublicInputTrait, verify_cairo1_public_input} + public_input::{ + PublicInput, PublicInputTrait, verify_cairo1_public_input, + get_builtins as get_program_builtins + } }, domains::StarkDomains }; @@ -37,7 +40,8 @@ impl StarknetPublicInputImpl of PublicInputTrait { // TODO support more pages? assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers'); - let builtins = get_builtins(); + let layout_builtins = get_builtins(); + let program_builtins = get_program_builtins(); let memory = self.main_page; // 1. Program segment @@ -56,7 +60,7 @@ impl StarknetPublicInputImpl of PublicInputTrait { assert( *program[0] == 0x40780017fff7fff, 'Invalid program' ); // Instruction: ap += N_BUILTINS. - assert(*program[1] == builtins.len().into(), 'Invalid program'); + assert(*program[1] == program_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'); @@ -77,10 +81,10 @@ impl StarknetPublicInputImpl of PublicInputTrait { // 2.2 Main arguments and return values let mut begin_addresses = ArrayTrait::new(); let mut stop_addresses = ArrayTrait::new(); + let layout_builtins_len = layout_builtins.len(); let mut i = 0; - let builtins_len = builtins.len(); loop { - if i == builtins_len { + if i == layout_builtins_len { break; } @@ -89,12 +93,20 @@ impl StarknetPublicInputImpl of PublicInputTrait { i += 1; }; - memory.verify_stack(initial_ap, begin_addresses.span(), builtins_len, ref memory_index); memory .verify_stack( - final_ap - builtins_len.into(), + initial_ap, + begin_addresses.span(), + program_builtins.span(), + layout_builtins.span(), + ref memory_index + ); + memory + .verify_stack( + final_ap - program_builtins.len().into(), stop_addresses.span(), - builtins_len, + program_builtins.span(), + layout_builtins.span(), ref memory_index ); diff --git a/src/air/layouts/starknet_with_keccak/public_input.cairo b/src/air/layouts/starknet_with_keccak/public_input.cairo index 9b477ddeb..e0ac4d3b4 100644 --- a/src/air/layouts/starknet_with_keccak/public_input.cairo +++ b/src/air/layouts/starknet_with_keccak/public_input.cairo @@ -11,7 +11,10 @@ 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::{PublicInput, PublicInputTrait, verify_cairo1_public_input} + public_input::{ + PublicInput, PublicInputTrait, verify_cairo1_public_input, + get_builtins as get_program_builtins + } }, domains::StarkDomains }; @@ -37,7 +40,8 @@ impl StarknetWithKeccakPublicInputImpl of PublicInputTrait { // TODO support more pages? assert(self.continuous_page_headers.len() == 0, 'Invalid continuous_page_headers'); - let builtins = get_builtins(); + let layout_builtins = get_builtins(); + let program_builtins = get_program_builtins(); let memory = self.main_page; // 1. Program segment @@ -56,7 +60,7 @@ impl StarknetWithKeccakPublicInputImpl of PublicInputTrait { assert( *program[0] == 0x40780017fff7fff, 'Invalid program' ); // Instruction: ap += N_BUILTINS. - assert(*program[1] == builtins.len().into(), 'Invalid program'); + assert(*program[1] == program_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'); @@ -77,10 +81,10 @@ impl StarknetWithKeccakPublicInputImpl of PublicInputTrait { // 2.2 Main arguments and return values let mut begin_addresses = ArrayTrait::new(); let mut stop_addresses = ArrayTrait::new(); + let layout_builtins_len = layout_builtins.len(); let mut i = 0; - let builtins_len = builtins.len(); loop { - if i == builtins_len { + if i == layout_builtins_len { break; } @@ -89,12 +93,20 @@ impl StarknetWithKeccakPublicInputImpl of PublicInputTrait { i += 1; }; - memory.verify_stack(initial_ap, begin_addresses.span(), builtins_len, ref memory_index); memory .verify_stack( - final_ap - builtins_len.into(), + initial_ap, + begin_addresses.span(), + program_builtins.span(), + layout_builtins.span(), + ref memory_index + ); + memory + .verify_stack( + final_ap - program_builtins.len().into(), stop_addresses.span(), - builtins_len, + program_builtins.span(), + layout_builtins.span(), ref memory_index ); diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 0ada83ebf..ca7de26ba 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -27,6 +27,22 @@ use cairo_verifier::{ }, }; +pub fn get_builtins() -> Array { + array![ + 'output', + 'pedersen', + 'range_check', + 'ecdsa', + 'bitwise', + 'ec_op', + 'keccak', + 'poseidon', + 'range_check96', + 'add_mod', + 'mul_mod' + ] +} + use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Hash}}; use poseidon::poseidon_hash_span; @@ -65,7 +81,9 @@ trait 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(public_input: @PublicInput, n_verifier_friendly_commitment_layers: felt252) -> felt252 { +fn get_public_input_hash( + public_input: @PublicInput, n_verifier_friendly_commitment_layers: felt252 +) -> felt252 { // Main page hash. let mut main_page_hash_state = PedersenTrait::new(0); let mut i: u32 = 0; diff --git a/src/air/public_memory.cairo b/src/air/public_memory.cairo index af58c1e28..3d84bbbfd 100644 --- a/src/air/public_memory.cairo +++ b/src/air/public_memory.cairo @@ -1,3 +1,5 @@ +use core::array::SpanTrait; +use core::debug::PrintTrait; #[derive(Drop, Copy, Hash, PartialEq, Serde)] struct AddrValue { address: felt252, @@ -77,21 +79,28 @@ impl PageImpl of PageTrait { self: @Page, start_ap: felt252, segment_addresses: Span, - builtins_len: usize, + program_builtins: Span, + layout_builtins: Span, ref offset: usize ) { - let mut i = 0; + let mut p = 0; + let mut l = 0; loop { - if i == builtins_len { + if p == program_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; + assert(current.address == start_ap + p.into(), 'Invalid address'); + if l < layout_builtins.len() { + if program_builtins[p] == layout_builtins[l] { + assert(current.value == *segment_addresses.at(l), 'Invalid builtin'); + l += 1; + } + } + p += 1; offset += 1; }; }