Public input validation

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;

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;

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);
+    }
 }

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::<felt252, u128>::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');
+}

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::<felt252, u128>::try_into(x).is_some(), 'range check failed');
-}
-
 impl Felt252Div of Div<felt252> {
     fn div(lhs: felt252, rhs: felt252) -> felt252 {
         (Into::<felt252, u256>::into(lhs) / Into::<felt252, u256>::into(rhs)).try_into().unwrap()