openvm_continuations/circuit/deferral/inner/verifier/
air.rs

1use std::{array::from_fn, borrow::Borrow};
2
3use openvm_circuit_primitives::{
4    utils::{and, not},
5    ColumnsAir, StructReflection, StructReflectionHelper,
6};
7use openvm_recursion_circuit::{
8    bus::{
9        CachedCommitBus, CachedCommitBusMessage, PreHashBus, PreHashMessage, PublicValuesBus,
10        PublicValuesBusMessage,
11    },
12    primitives::bus::{RangeCheckerBus, RangeCheckerBusMessage},
13};
14use openvm_recursion_circuit_derive::AlignedBorrow;
15use openvm_stark_backend::{
16    interaction::InteractionBuilder, BaseAirWithPublicValues, PartitionedBaseAir,
17};
18use openvm_verify_stark_host::pvs::{
19    VerifierBasePvs, CONSTRAINT_EVAL_AIR_ID, CONSTRAINT_EVAL_CACHED_INDEX, LOG_MAX_RECURSION_DEPTH,
20    VERIFIER_PVS_AIR_ID,
21};
22use p3_air::{Air, AirBuilder, AirBuilderWithPublicValues, BaseAir};
23use p3_field::{Field, PrimeCharacteristicRing};
24use p3_matrix::Matrix;
25
26use crate::circuit::{
27    deferral::inner::bus::{DefPvsConsistencyBus, DefPvsConsistencyMessage},
28    utils::{assert_vk_commit_eq, assert_vk_commit_unset},
29};
30
31#[repr(C)]
32#[derive(AlignedBorrow, StructReflection)]
33pub struct DeferralVerifierPvsCols<F> {
34    pub proof_idx: F,
35    pub is_valid: F,
36    pub has_verifier_pvs: F,
37
38    pub recursion_flag: F,
39    pub depth_inv: F,
40
41    pub child_pvs: VerifierBasePvs<F>,
42}
43
44pub enum DeferralChildLevel {
45    App,
46    Leaf,
47    InternalForLeaf,
48    InternalRecursive,
49}
50
51#[derive(ColumnsAir)]
52#[columns_via(DeferralVerifierPvsCols<u8>)]
53pub struct DeferralVerifierPvsAir {
54    pub public_values_bus: PublicValuesBus,
55    pub cached_commit_bus: CachedCommitBus,
56    pub pre_hash_bus: PreHashBus,
57    pub range_bus: RangeCheckerBus,
58    pub def_pvs_consistency_bus: DefPvsConsistencyBus,
59}
60
61impl<F> BaseAir<F> for DeferralVerifierPvsAir {
62    fn width(&self) -> usize {
63        DeferralVerifierPvsCols::<u8>::width()
64    }
65}
66impl<F> BaseAirWithPublicValues<F> for DeferralVerifierPvsAir {
67    fn num_public_values(&self) -> usize {
68        VerifierBasePvs::<u8>::width()
69    }
70}
71impl<F> PartitionedBaseAir<F> for DeferralVerifierPvsAir {}
72
73impl<AB: AirBuilder + InteractionBuilder + AirBuilderWithPublicValues> Air<AB>
74    for DeferralVerifierPvsAir
75{
76    fn eval(&self, builder: &mut AB) {
77        let main = builder.main();
78        let (local, next) = (
79            main.row_slice(0).expect("window should have two elements"),
80            main.row_slice(1).expect("window should have two elements"),
81        );
82        let local: &DeferralVerifierPvsCols<AB::Var> = (*local).borrow();
83        let next: &DeferralVerifierPvsCols<AB::Var> = (*next).borrow();
84
85        builder.assert_bool(local.is_valid);
86        builder.when_first_row().assert_one(local.is_valid);
87        builder
88            .when_transition()
89            .assert_bool(local.is_valid - next.is_valid);
90
91        builder.when_first_row().assert_zero(local.proof_idx);
92        builder
93            .when_transition()
94            .when(and(local.is_valid, next.is_valid))
95            .assert_eq(local.proof_idx + AB::F::ONE, next.proof_idx);
96
97        builder.assert_bool(local.has_verifier_pvs);
98        builder
99            .when(local.has_verifier_pvs)
100            .assert_one(local.is_valid);
101
102        /*
103         * We constrain the consistency of verifier-specific public values. We can determine
104         * what layer a verifier is at using the has_verifier_pvs and internal_flag columns. If
105         * has_verifier_pvs is 0, then we have a leaf verifier that is verifying a deferral
106         * circuit proof. If has_verifier_pvs is 1 and internal_flag is 0, then
107         * we have an internal verifier that has leaf children, and if internal_flag is 1 then
108         * we have internal_for_leaf children. Finally, if internal_flag is 2 then we are
109         * verifying internal_recursive children.
110         *
111         * The recursion_flag column is a saturated selector derived from the child
112         * recursion_depth.
113         */
114        // constrain verifier pvs columns are the same across all rows (note app_vk_commit is
115        // def_vk_commit here)
116        let mut when_both = builder.when(and(local.is_valid, next.is_valid));
117        let is_leaf = not(local.has_verifier_pvs);
118        let is_internal = local.has_verifier_pvs;
119
120        when_both.assert_eq(local.has_verifier_pvs, next.has_verifier_pvs);
121        when_both.assert_eq(local.recursion_flag, next.recursion_flag);
122        when_both.assert_eq(local.child_pvs.internal_flag, next.child_pvs.internal_flag);
123        when_both.assert_eq(
124            local.child_pvs.recursion_depth,
125            next.child_pvs.recursion_depth,
126        );
127        assert_vk_commit_eq(
128            &mut when_both,
129            local.child_pvs.app_vk_commit,
130            next.child_pvs.app_vk_commit,
131        );
132        assert_vk_commit_eq(
133            &mut when_both,
134            local.child_pvs.leaf_vk_commit,
135            next.child_pvs.leaf_vk_commit,
136        );
137        assert_vk_commit_eq(
138            &mut when_both,
139            local.child_pvs.internal_for_leaf_vk_commit,
140            next.child_pvs.internal_for_leaf_vk_commit,
141        );
142        assert_vk_commit_eq(
143            &mut when_both,
144            local.child_pvs.internal_recursive_vk_commit,
145            next.child_pvs.internal_recursive_vk_commit,
146        );
147
148        // constrain that the flags are ternary
149        builder.assert_tern(local.child_pvs.internal_flag);
150        builder.assert_tern(local.recursion_flag);
151
152        // constrain that recursion_flag is 0 iff recursion_depth == 0, recursion_flag == 1
153        // if recursion_depth == 1, and recursion_flag == 2 iff recursion_depth >= 2
154        let half = AB::F::TWO.inverse();
155        let is_recursion_flag_two =
156            (local.recursion_flag - AB::F::ONE) * local.recursion_flag * half;
157
158        builder
159            .when_ne(local.recursion_flag, AB::F::TWO)
160            .assert_eq(local.child_pvs.recursion_depth, local.recursion_flag);
161        builder
162            .when_ne(local.child_pvs.recursion_depth, AB::F::ZERO)
163            .when_ne(local.child_pvs.recursion_depth, AB::F::ONE)
164            .assert_eq(local.recursion_flag, AB::F::TWO);
165        builder.assert_eq(
166            is_recursion_flag_two.clone(),
167            local.child_pvs.recursion_depth
168                * (local.child_pvs.recursion_depth - AB::F::ONE)
169                * local.depth_inv,
170        );
171
172        // constrain recursion_depth is 0 when internal_flag is 0 or 1
173        builder
174            .when_ne(local.child_pvs.internal_flag, AB::F::TWO)
175            .assert_zero(local.child_pvs.recursion_depth);
176
177        // range check child recursion_depth to be in [0, MAX_RECURSION_DEPTH)
178        self.range_bus.lookup_key(
179            builder,
180            RangeCheckerBusMessage {
181                value: local.child_pvs.recursion_depth.into(),
182                max_bits: AB::Expr::from_u8(LOG_MAX_RECURSION_DEPTH),
183            },
184            local.is_valid,
185        );
186
187        // constrain that internal_flag is 2 when recursion_flag is set, and not 2 otherwise
188        builder
189            .when(local.recursion_flag)
190            .assert_eq(local.child_pvs.internal_flag, AB::F::TWO);
191        builder
192            .when_ne(local.recursion_flag, AB::F::ONE)
193            .when_ne(local.recursion_flag, AB::F::TWO)
194            .assert_bool(local.child_pvs.internal_flag);
195
196        // constrain that child commits are 0 when they shouldn't be defined
197        builder
198            .when(is_leaf.clone())
199            .assert_zero(local.child_pvs.internal_flag);
200
201        assert_vk_commit_unset(
202            &mut builder.when(is_leaf.clone()),
203            local.child_pvs.app_vk_commit,
204        );
205        assert_vk_commit_unset(
206            &mut builder.when(
207                (local.child_pvs.internal_flag - AB::F::ONE)
208                    * (local.child_pvs.internal_flag - AB::F::TWO),
209            ),
210            local.child_pvs.leaf_vk_commit,
211        );
212        assert_vk_commit_unset(
213            &mut builder.when(local.child_pvs.internal_flag - AB::F::TWO),
214            local.child_pvs.internal_for_leaf_vk_commit,
215        );
216        assert_vk_commit_unset(
217            &mut builder.when(local.recursion_flag - AB::F::TWO),
218            local.child_pvs.internal_recursive_vk_commit,
219        );
220
221        /*
222         * If has_verifier_pvs is true (i.e. we are on some internal level) we need to receive
223         * public values from ProofShapeModule to ensure the values being read here are correct.
224         * Each inner public value should have air_idx VERIFIER_PVS_AIR_ID.
225         */
226        let verifier_pvs_id = AB::Expr::from_usize(VERIFIER_PVS_AIR_ID);
227
228        for (pv_idx, value) in local.child_pvs.as_slice().iter().enumerate() {
229            self.public_values_bus.receive(
230                builder,
231                local.proof_idx,
232                PublicValuesBusMessage {
233                    air_idx: verifier_pvs_id.clone(),
234                    pv_idx: AB::Expr::from_usize(pv_idx),
235                    value: (*value).into(),
236                },
237                local.is_valid * is_internal,
238            );
239        }
240
241        /*
242         * We want to ensure consistency between AIRs that process public values, and we do so
243         * using the def_pvs_consistency_bus.
244         */
245        self.def_pvs_consistency_bus.send(
246            builder,
247            local.proof_idx,
248            DefPvsConsistencyMessage {
249                has_verifier_pvs: local.has_verifier_pvs,
250            },
251            local.is_valid,
252        );
253
254        /*
255         * Finally, we need to constrain that the public values this AIR produces are consistent
256         * with the child's. Note that we only impose constraints for layers below the current
257         * one - it is impossible for the current layer to know its own commit, and future layers
258         * will catch if we preemptively define a current or future verifier commit.
259         */
260        let &VerifierBasePvs::<_> {
261            internal_flag,
262            app_vk_commit: def_vk_commit,
263            leaf_vk_commit,
264            internal_for_leaf_vk_commit,
265            recursion_depth,
266            internal_recursive_vk_commit,
267        } = builder.public_values().borrow();
268
269        // constrain internal_flag is 0 at the leaf level
270        builder
271            .when(and(local.is_valid, is_leaf.clone()))
272            .assert_zero(internal_flag);
273
274        // constrain recursion_depth is 0 at the leaf and internal_for_leaf levels
275        builder
276            .when(
277                local.is_valid
278                    * (local.child_pvs.internal_flag - AB::F::ONE)
279                    * (local.child_pvs.internal_flag - AB::F::TWO),
280            )
281            .assert_zero(recursion_depth);
282
283        // constraint internal_flag is incremented properly at internal levels
284        builder
285            .when(is_internal)
286            .when_ne(local.child_pvs.internal_flag, AB::F::TWO)
287            .assert_eq(internal_flag, local.child_pvs.internal_flag + AB::F::ONE);
288
289        // constrain def_vk_commit is set at all internal levels
290        assert_vk_commit_eq(
291            &mut builder.when(is_internal),
292            local.child_pvs.app_vk_commit,
293            def_vk_commit,
294        );
295
296        // constrain verifier-specific pvs at all internal_recursive levels
297        builder
298            .when(local.child_pvs.internal_flag)
299            .assert_zero(internal_flag.into() - AB::F::TWO);
300        assert_vk_commit_eq(
301            &mut builder.when(local.child_pvs.internal_flag),
302            local.child_pvs.leaf_vk_commit,
303            leaf_vk_commit,
304        );
305
306        // constrain recursion_depth increments at each internal_recursive level
307        builder
308            .when(local.child_pvs.internal_flag)
309            .assert_one(recursion_depth.into() - local.child_pvs.recursion_depth);
310
311        // constrain internal_for_leaf_vk_commit is set at internal_recursive levels after
312        // the first and matches the output public value
313        assert_vk_commit_eq(
314            &mut builder.when(local.recursion_flag),
315            local.child_pvs.internal_for_leaf_vk_commit,
316            internal_for_leaf_vk_commit,
317        );
318
319        // constrain internal_recursive_vk_commit is set at internal_recursive levels after
320        // the second and matches the output public value
321        assert_vk_commit_eq(
322            &mut builder.when(local.recursion_flag * (local.recursion_flag - AB::F::ONE)),
323            local.child_pvs.internal_recursive_vk_commit,
324            internal_recursive_vk_commit,
325        );
326
327        /*
328         * We also need to receive cached commits from ProofShapeModule. Note that the deferral
329         * circuit cached commits are received in another AIR, so only the internal verifier will
330         * receive them here.
331         */
332        let is_internal_flag_zero = (local.child_pvs.internal_flag - AB::F::ONE)
333            * (local.child_pvs.internal_flag - AB::F::TWO)
334            * AB::F::TWO.inverse();
335        let is_internal_flag_one =
336            (AB::Expr::TWO - local.child_pvs.internal_flag) * local.child_pvs.internal_flag;
337        let is_recursion_flag_one = (AB::Expr::TWO - local.recursion_flag) * local.recursion_flag;
338        let cached_commit = from_fn(|i| {
339            is_internal_flag_zero.clone() * local.child_pvs.app_vk_commit.cached_commit[i]
340                + is_internal_flag_one.clone() * local.child_pvs.leaf_vk_commit.cached_commit[i]
341                + is_recursion_flag_one.clone()
342                    * local.child_pvs.internal_for_leaf_vk_commit.cached_commit[i]
343                + is_recursion_flag_two.clone()
344                    * local.child_pvs.internal_recursive_vk_commit.cached_commit[i]
345        });
346
347        self.cached_commit_bus.receive(
348            builder,
349            local.proof_idx,
350            CachedCommitBusMessage {
351                air_idx: AB::Expr::from_usize(CONSTRAINT_EVAL_AIR_ID),
352                cached_idx: AB::Expr::from_usize(CONSTRAINT_EVAL_CACHED_INDEX),
353                global_cached_idx: AB::Expr::ZERO,
354                cached_commit,
355            },
356            local.is_valid * is_internal,
357        );
358
359        /*
360         * Unlike the cached commits, we receive the pre-hash on the same layer that it's
361         * observed. We receive it from ProofShapeModule also.
362         *
363         * By the constraints above, the output recursion_depth is 1 iff the child internal_flag
364         * is 1, and is at least 2 iff the child internal_flag is 2.
365         */
366        let internal_flag = internal_flag.into();
367
368        let is_pvs_internal_flag_zero = (internal_flag.clone() - AB::Expr::ONE)
369            * (internal_flag.clone() - AB::Expr::TWO)
370            * half;
371        let is_pvs_internal_flag_one =
372            (AB::Expr::TWO - internal_flag.clone()) * internal_flag.clone();
373        let is_internal_flag_two =
374            (local.child_pvs.internal_flag - AB::Expr::ONE) * local.child_pvs.internal_flag * half;
375
376        let vk_pre_hash = from_fn(|i| {
377            is_pvs_internal_flag_zero.clone() * def_vk_commit.vk_pre_hash[i].into()
378                + is_pvs_internal_flag_one.clone() * leaf_vk_commit.vk_pre_hash[i].into()
379                + is_internal_flag_one.clone() * internal_for_leaf_vk_commit.vk_pre_hash[i].into()
380                + is_internal_flag_two.clone() * internal_recursive_vk_commit.vk_pre_hash[i].into()
381        });
382
383        self.pre_hash_bus.receive(
384            builder,
385            local.proof_idx,
386            PreHashMessage { vk_pre_hash },
387            local.is_valid,
388        );
389    }
390}
openvm_continuations/circuit/deferral/inner/verifier/air.rs

openvm_continuations/circuit/deferral/inner/verifier/
air.rs
