openvm_continuations/circuit/deferral/hook/decommit/
air.rs

1use std::borrow::Borrow;
2
3use openvm_circuit_primitives::{
4    utils::not, ColumnsAir, StructReflection, StructReflectionHelper, SubAir,
5};
6use openvm_recursion_circuit::{prelude::DIGEST_SIZE, utils::assert_zeros};
7use openvm_recursion_circuit_derive::AlignedBorrow;
8use openvm_stark_backend::{
9    interaction::InteractionBuilder, BaseAirWithPublicValues, PartitionedBaseAir,
10};
11use p3_air::{Air, AirBuilder, AirBuilderWithPublicValues, BaseAir};
12use p3_field::PrimeCharacteristicRing;
13use p3_matrix::Matrix;
14
15use crate::circuit::{
16    deferral::hook::bus::{IoCommitBus, IoCommitMessage},
17    subair::{MerkleTreeCols, MerkleTreeSubAir},
18};
19
20#[repr(C)]
21#[derive(AlignedBorrow, StructReflection)]
22pub struct MerkleDecommitCols<F> {
23    pub merkle_tree_cols: MerkleTreeCols<F>,
24    pub tagged_left_child: [F; DIGEST_SIZE],
25    pub send_commits: F,
26    pub num_rows: F,
27}
28
29#[derive(ColumnsAir)]
30#[columns_via(MerkleDecommitCols<u8>)]
31pub struct MerkleDecommitAir {
32    pub subair: MerkleTreeSubAir,
33    pub io_commit_bus: IoCommitBus,
34}
35
36impl<F> BaseAir<F> for MerkleDecommitAir {
37    fn width(&self) -> usize {
38        MerkleDecommitCols::<u8>::width()
39    }
40}
41impl<F> BaseAirWithPublicValues<F> for MerkleDecommitAir {}
42impl<F> PartitionedBaseAir<F> for MerkleDecommitAir {}
43
44impl<AB: AirBuilder + InteractionBuilder + AirBuilderWithPublicValues> Air<AB>
45    for MerkleDecommitAir
46{
47    fn eval(&self, builder: &mut AB) {
48        let main = builder.main();
49        let (local, next) = (
50            main.row_slice(0).expect("window should have two elements"),
51            main.row_slice(1).expect("window should have two elements"),
52        );
53        let local: &MerkleDecommitCols<AB::Var> = (*local).borrow();
54        let next: &MerkleDecommitCols<AB::Var> = (*next).borrow();
55
56        self.subair.eval(
57            builder,
58            (
59                &local.merkle_tree_cols,
60                &next.merkle_tree_cols,
61                local.num_rows.into(),
62                Some(&local.tagged_left_child),
63            ),
64        );
65        builder.assert_eq(local.num_rows, next.num_rows);
66
67        /*
68         * We send the input and output commits (i.e. left_child and right_child) to
69         * OnionHashAir when send_commits is 1. We constrain that we send at least one
70         * commit by forcing it to be 1 on the first row, and that all the sends are
71         * at the beginning. Additionally, we need constrain that send_commits is only
72         * 1 on Merkle leaves, and that non-send Merkle leaves are unset.
73         */
74        builder.assert_bool(local.send_commits);
75        builder.when_first_row().assert_one(local.send_commits);
76        builder
77            .when_transition()
78            .assert_bool(local.send_commits - next.send_commits);
79
80        let is_leaf = local.merkle_tree_cols.receive_type
81            * (AB::Expr::TWO - local.merkle_tree_cols.receive_type);
82        builder.when(local.send_commits).assert_one(is_leaf.clone());
83
84        let mut when_no_send = builder.when(not(local.send_commits));
85        let mut when_no_send_and_leaf = when_no_send.when(is_leaf);
86        assert_zeros(
87            &mut when_no_send_and_leaf,
88            local.merkle_tree_cols.left_child,
89        );
90        assert_zeros(
91            &mut when_no_send_and_leaf,
92            local.merkle_tree_cols.right_child,
93        );
94
95        self.io_commit_bus.send(
96            builder,
97            IoCommitMessage {
98                idx: local.merkle_tree_cols.row_idx,
99                input_commit: local.merkle_tree_cols.left_child,
100                output_commit: local.merkle_tree_cols.right_child,
101            },
102            local.send_commits,
103        );
104    }
105}
openvm_continuations/circuit/deferral/hook/decommit/air.rs

openvm_continuations/circuit/deferral/hook/decommit/
air.rs
