openvm_recursion_circuit/primitives/range/
air.rs

1use core::borrow::Borrow;
2
3use openvm_circuit_primitives::{ColumnsAir, StructReflection, StructReflectionHelper};
4use openvm_recursion_circuit_derive::AlignedBorrow;
5use openvm_stark_backend::{
6    interaction::InteractionBuilder, BaseAirWithPublicValues, PartitionedBaseAir,
7};
8use p3_air::{Air, AirBuilder, BaseAir};
9use p3_field::PrimeCharacteristicRing;
10use p3_matrix::Matrix;
11
12use crate::primitives::bus::{RangeCheckerBus, RangeCheckerBusMessage};
13
14#[repr(C)]
15#[derive(AlignedBorrow, Debug, StructReflection)]
16pub struct RangeCheckerCols<T> {
17    pub value: T,
18    pub mult: T,
19}
20
21#[derive(Debug, ColumnsAir)]
22#[columns_via(RangeCheckerCols<u8>)]
23pub struct RangeCheckerAir<const NUM_BITS: usize> {
24    pub bus: RangeCheckerBus,
25}
26
27impl<F, const NUM_BITS: usize> BaseAir<F> for RangeCheckerAir<NUM_BITS> {
28    fn width(&self) -> usize {
29        RangeCheckerCols::<F>::width()
30    }
31}
32impl<F, const NUM_BITS: usize> BaseAirWithPublicValues<F> for RangeCheckerAir<NUM_BITS> {}
33impl<F, const NUM_BITS: usize> PartitionedBaseAir<F> for RangeCheckerAir<NUM_BITS> {}
34
35impl<AB: AirBuilder + InteractionBuilder, const NUM_BITS: usize> Air<AB>
36    for RangeCheckerAir<NUM_BITS>
37{
38    fn eval(&self, builder: &mut AB) {
39        let main = builder.main();
40
41        let (local, next) = (
42            main.row_slice(0).expect("window should have two elements"),
43            main.row_slice(1).expect("window should have two elements"),
44        );
45        let local: &RangeCheckerCols<AB::Var> = (*local).borrow();
46        let next: &RangeCheckerCols<AB::Var> = (*next).borrow();
47
48        builder.when_first_row().assert_zero(local.value);
49        builder
50            .when_transition()
51            .assert_eq(local.value + AB::F::ONE, next.value);
52        builder
53            .when_last_row()
54            .assert_eq(local.value, AB::F::from_usize((1 << NUM_BITS) - 1));
55
56        self.bus.add_key_with_lookups(
57            builder,
58            RangeCheckerBusMessage {
59                value: local.value.into(),
60                max_bits: AB::Expr::from_usize(NUM_BITS),
61            },
62            local.mult,
63        );
64    }
65}
openvm_recursion_circuit/primitives/range/air.rs

openvm_recursion_circuit/primitives/range/
air.rs
