From 0db219cc21531707d03cedbc322e8c9e2f09ccbf Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Thu, 11 Jan 2024 19:24:43 +0000 Subject: [PATCH 1/9] move assert_nn to asserts --- src/air/composition.cairo | 3 ++- src/common/asserts.cairo | 6 ++++++ src/common/math.cairo | 5 ----- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/air/composition.cairo b/src/air/composition.cairo index f578a175e..800234a05 100644 --- a/src/air/composition.cairo +++ b/src/air/composition.cairo @@ -7,7 +7,8 @@ use cairo_verifier::air::public_input::{PublicInput, PublicInputTrait}; use cairo_verifier::air::diluted::get_diluted_product; use cairo_verifier::air::pedersen::{eval_pedersen_x, eval_pedersen_y}; use cairo_verifier::air::autogenerated::eval_composition_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/common/asserts.cairo b/src/common/asserts.cairo index 5603bf777..b97e1479e 100644 --- a/src/common/asserts.cairo +++ b/src/common/asserts.cairo @@ -4,3 +4,9 @@ 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'); +} + 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() From 3c9ef264bf4ab24cd1df54211841d9f1c42926e2 Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Thu, 11 Jan 2024 19:27:44 +0000 Subject: [PATCH 2/9] assert_nn_le --- src/common/asserts.cairo | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/common/asserts.cairo b/src/common/asserts.cairo index b97e1479e..d5cc641e5 100644 --- a/src/common/asserts.cairo +++ b/src/common/asserts.cairo @@ -10,3 +10,7 @@ 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'); +} From 1e30c88ea0773d17dbf6b6ba5ef4acac22d3072b Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Thu, 11 Jan 2024 19:34:51 +0000 Subject: [PATCH 3/9] validation constants --- src/air/constants.cairo | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/air/constants.cairo b/src/air/constants.cairo index a42656530..36707a3bd 100644 --- a/src/air/constants.cairo +++ b/src/air/constants.cairo @@ -29,6 +29,9 @@ const NUM_COLUMNS_FIRST: felt252 = 7; const NUM_COLUMNS_SECOND: felt252 = 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; From 16cd090c986f541b21d4a8a3c39a97f53c9662fd Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Fri, 12 Jan 2024 18:15:18 +0000 Subject: [PATCH 4/9] trace size --- src/air/public_input.cairo | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 8f73c2414..7ca2168ce 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,13 @@ 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' + ); + } } From 0f8aafbb35ad9e535a603c7df18edb952dbbb017 Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Fri, 12 Jan 2024 18:19:47 +0000 Subject: [PATCH 5/9] rc ranges and layout code --- src/air/public_input.cairo | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 7ca2168ce..7344cb970 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -160,5 +160,11 @@ impl PublicInputImpl of PublicInputTrait { 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'); } } From a07fcd2a45cd9f1b7c9df4a96a08786c259305e3 Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Fri, 12 Jan 2024 18:42:11 +0000 Subject: [PATCH 6/9] pedersen --- src/air/public_input.cairo | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 7344cb970..d27cbc064 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -166,5 +166,11 @@ impl PublicInputImpl of PublicInputTrait { 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); } } From 556725f469fed75edf98fd53404a54c0f96723c7 Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Fri, 12 Jan 2024 18:48:17 +0000 Subject: [PATCH 7/9] range_check --- src/air/public_input.cairo | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index d27cbc064..4b73be16e 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -172,5 +172,10 @@ impl PublicInputImpl of PublicInputTrait { - *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); } } From 638bf27c32179f54d26fa8411d87fa07aa325470 Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Fri, 12 Jan 2024 18:49:53 +0000 Subject: [PATCH 8/9] bitwise --- src/air/public_input.cairo | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/air/public_input.cairo b/src/air/public_input.cairo index 4b73be16e..db253e756 100644 --- a/src/air/public_input.cairo +++ b/src/air/public_input.cairo @@ -177,5 +177,11 @@ impl PublicInputImpl of PublicInputTrait { 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); } } From 4cc660c68901bad09a1b7d0d9a11eef9f458d090 Mon Sep 17 00:00:00 2001 From: tiagofneto Date: Mon, 15 Jan 2024 16:16:18 +0000 Subject: [PATCH 9/9] fix import --- src/air/composition.cairo | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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;