openvm_recursion_circuit/subairs/proof_idx/
air.rs

1use openvm_circuit_primitives::SubAir;
2use openvm_recursion_circuit_derive::AlignedBorrow;
3use p3_air::AirBuilder;
4use p3_field::PrimeCharacteristicRing;
5
6#[derive(Default)]
7pub struct ProofIdxSubAir;
8
9#[repr(C)]
10#[derive(AlignedBorrow, Copy, Clone, Debug)]
11pub struct ProofIdxIoCols<T> {
12    /// Whether the current row is enabled (i.e. not padding)
13    pub is_enabled: T,
14    pub proof_idx: T,
15}
16
17impl<T> ProofIdxIoCols<T> {
18    pub fn map_into<S>(self) -> ProofIdxIoCols<S>
19    where
20        T: Into<S>,
21    {
22        ProofIdxIoCols {
23            is_enabled: self.is_enabled.into(),
24            proof_idx: self.proof_idx.into(),
25        }
26    }
27}
28
29impl<AB: AirBuilder> SubAir<AB> for ProofIdxSubAir {
30    type AirContext<'a>
31        = (ProofIdxIoCols<AB::Expr>, ProofIdxIoCols<AB::Expr>)
32    where
33        AB: 'a,
34        AB::Var: 'a,
35        AB::Expr: 'a;
36
37    fn eval<'a>(&'a self, builder: &'a mut AB, ctx: Self::AirContext<'a>)
38    where
39        AB::Var: 'a,
40        AB::Expr: 'a,
41    {
42        let (local, next) = ctx;
43
44        // 1. Boolean valid flag
45        builder.assert_bool(local.is_enabled.clone());
46        // 2. Padding rows are followed by padding rows
47        builder
48            .when_transition()
49            .when_ne(local.is_enabled.clone(), AB::Expr::ONE)
50            .assert_zero(next.is_enabled.clone());
51        // 3. Proof index starts at 0
52        builder
53            .when_first_row()
54            .assert_zero(local.proof_idx.clone());
55        // 4. Proof index increments by exactly one between valid rows
56        builder
57            .when_transition()
58            .when(next.is_enabled.clone())
59            .assert_eq(next.proof_idx, local.proof_idx + AB::Expr::ONE);
60    }
61}
openvm_recursion_circuit/subairs/proof_idx/air.rs

openvm_recursion_circuit/subairs/proof_idx/
air.rs
