diff --git a/src/air/composition.cairo b/src/air/composition.cairo index e1be67112..2ce2fc37f 100644 --- a/src/air/composition.cairo +++ b/src/air/composition.cairo @@ -9,7 +9,8 @@ use cairo_verifier::air::pedersen::{eval_pedersen_x, eval_pedersen_y}; use cairo_verifier::air::autogenerated::{ eval_composition_polynomial_inner, eval_oods_polynomial_inner }; -use cairo_verifier::common::math::{Felt252Div, Felt252PartialOrd, pow, assert_range_u128}; +use cairo_verifier::common::math::{Felt252Div, Felt252PartialOrd, pow}; +use cairo_verifier::common::asserts::assert_range_u128; const SHIFT_POINT_X: felt252 = 0x49ee3eba8c1600700ee1b87eb599f16716b0b1022947733551fde4050ca6804; const SHIFT_POINT_Y: felt252 = 0x3ca0cfe4b3bc6ddf346d49d06ea0ed34e621062c0e056c1d0405d266e10268a; diff --git a/src/air/constants.cairo b/src/air/constants.cairo index 0d93a7955..5d9851d2a 100644 --- a/src/air/constants.cairo +++ b/src/air/constants.cairo @@ -29,6 +29,9 @@ const NUM_COLUMNS_FIRST: u32 = 7; const NUM_COLUMNS_SECOND: u32 = 3; const IS_DYNAMIC_AIR: felt252 = 0; +const MAX_LOG_N_STEPS: felt252 = 50; +const MAX_RANGE_CHECK: felt252 = 0xffff; // 2 ** 16 - 1 + mod segments { const PROGRAM: usize = 0; const EXECUTION: usize = 1; diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 8f73c2414..db253e756 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -1,9 +1,13 @@ use cairo_verifier::{ common::{ flip_endianness::FlipEndiannessTrait, array_append::ArrayAppendTrait, blake2s::blake2s, - math::{pow, Felt252PartialOrd, Felt252Div} + math::{pow, Felt252PartialOrd, Felt252Div}, asserts::assert_range_u128_le }, - air::public_memory::{Page, PageTrait, ContinuousPageHeader, get_continuous_pages_product} + air::{ + public_memory::{Page, PageTrait, ContinuousPageHeader, get_continuous_pages_product}, + constants + }, + domains::StarkDomains }; use core::{pedersen::PedersenTrait, hash::{HashStateTrait, HashStateExTrait, Hash}}; @@ -148,4 +152,36 @@ 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); + assert( + n_steps * constants::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.layout == constants::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) + / 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; + 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) + / 5; + assert_range_u128_le(bitwise_uses, bitwise_copies); + } } diff --git a/src/common/asserts.cairo b/src/common/asserts.cairo index 5603bf777..d5cc641e5 100644 --- a/src/common/asserts.cairo +++ b/src/common/asserts.cairo @@ -4,3 +4,13 @@ fn assert_in_range(x: felt252, min: felt252, max: felt252) { assert(min <= x, 'Value too small'); assert(x < max, 'Value too large'); } + +// Verifies that 0 <= x < RANGE_CHECK_BOUND +fn assert_range_u128(x: felt252) { + assert(TryInto::::try_into(x).is_some(), 'range check failed'); +} + +fn assert_range_u128_le(x: felt252, max: felt252) { + assert_range_u128(x); + assert(x <= max, 'range check failed'); +} diff --git a/src/common/math.cairo b/src/common/math.cairo index fd143489e..e6e0b04c9 100644 --- a/src/common/math.cairo +++ b/src/common/math.cairo @@ -28,11 +28,6 @@ fn mul_inverse(x: felt252) -> felt252 { pow(x, STARK_PRIME_MINUS_TWO) } -// Verifies that 0 <= x < RANGE_CHECK_BOUND -fn assert_range_u128(x: felt252) { - assert(TryInto::::try_into(x).is_some(), 'range check failed'); -} - impl Felt252Div of Div { fn div(lhs: felt252, rhs: felt252) -> felt252 { (Into::::into(lhs) / Into::::into(rhs)).try_into().unwrap()