openvm_continuations/verifier/common/
mod.rs

1use std::array;
2
3use openvm_circuit::{
4    arch::{
5        CONNECTOR_AIR_ID, MERKLE_AIR_ID, PROGRAM_AIR_ID, PROGRAM_CACHED_TRACE_INDEX,
6        PUBLIC_VALUES_AIR_ID,
7    },
8    system::{connector::VmConnectorPvs, memory::merkle::MemoryMerklePvs},
9};
10use openvm_native_compiler::{ir::Config, prelude::*};
11use openvm_native_recursion::{digest::DigestVariable, vars::StarkProofVariable};
12use openvm_stark_sdk::openvm_stark_backend::p3_field::PrimeCharacteristicRing;
13
14use crate::verifier::internal::types::InternalVmVerifierPvs;
15
16pub mod non_leaf;
17pub mod types;
18
19pub fn assert_or_assign_app_and_leaf_commit_pvs<C: Config>(
20    builder: &mut Builder<C>,
21    dst: &InternalVmVerifierPvs<Felt<C::F>>,
22    proof_idx: RVar<C::N>,
23    proof_pvs: &InternalVmVerifierPvs<Felt<C::F>>,
24) {
25    builder.if_eq(proof_idx, RVar::zero()).then_or_else(
26        |builder| {
27            builder.assign(
28                &dst.vm_verifier_pvs.app_commit,
29                proof_pvs.vm_verifier_pvs.app_commit,
30            );
31            builder.assign(
32                &dst.extra_pvs.leaf_verifier_commit,
33                proof_pvs.extra_pvs.leaf_verifier_commit,
34            );
35        },
36        |builder| {
37            builder.assert_eq::<[_; DIGEST_SIZE]>(
38                dst.vm_verifier_pvs.app_commit,
39                proof_pvs.vm_verifier_pvs.app_commit,
40            );
41            builder.assert_eq::<[_; DIGEST_SIZE]>(
42                dst.extra_pvs.leaf_verifier_commit,
43                proof_pvs.extra_pvs.leaf_verifier_commit,
44            );
45        },
46    );
47}
48
49pub fn assert_or_assign_connector_pvs<C: Config>(
50    builder: &mut Builder<C>,
51    dst: &VmConnectorPvs<Felt<C::F>>,
52    proof_idx: RVar<C::N>,
53    proof_pvs: &VmConnectorPvs<Felt<C::F>>,
54) {
55    builder.if_eq(proof_idx, RVar::zero()).then_or_else(
56        |builder| {
57            builder.assign(&dst.initial_pc, proof_pvs.initial_pc);
58        },
59        |builder| {
60            // assert prev.final_pc == curr.initial_pc
61            builder.assert_felt_eq(dst.final_pc, proof_pvs.initial_pc);
62            // assert prev.is_terminate == 0
63            builder.assert_felt_eq(dst.is_terminate, C::F::ZERO);
64        },
65    );
66    // Update final_pc
67    builder.assign(&dst.final_pc, proof_pvs.final_pc);
68    // Update is_terminate
69    builder.assign(&dst.is_terminate, proof_pvs.is_terminate);
70    // Update exit_code
71    builder.assign(&dst.exit_code, proof_pvs.exit_code);
72}
73
74pub fn assert_or_assign_memory_pvs<C: Config>(
75    builder: &mut Builder<C>,
76    dst: &MemoryMerklePvs<Felt<C::F>, DIGEST_SIZE>,
77    proof_idx: RVar<C::N>,
78    proof_pvs: &MemoryMerklePvs<Felt<C::F>, DIGEST_SIZE>,
79) {
80    builder.if_eq(proof_idx, RVar::zero()).then_or_else(
81        |builder| {
82            builder.assign(&dst.initial_root, proof_pvs.initial_root);
83        },
84        |builder| {
85            // assert prev.final_root == curr.initial_root
86            builder.assert_eq::<[_; DIGEST_SIZE]>(dst.final_root, proof_pvs.initial_root);
87        },
88    );
89    // Update final_root
90    builder.assign(&dst.final_root, proof_pvs.final_root);
91}
92
93pub fn get_program_commit<C: Config>(
94    builder: &mut Builder<C>,
95    proof: &StarkProofVariable<C>,
96) -> [Felt<C::F>; DIGEST_SIZE] {
97    let t_id = RVar::from(PROGRAM_CACHED_TRACE_INDEX);
98    let commit = builder.get(&proof.commitments.main_trace, t_id);
99    let commit = if let DigestVariable::Felt(commit) = commit {
100        commit
101    } else {
102        unreachable!()
103    };
104    array::from_fn(|i| builder.get(&commit, i))
105}
106
107/// # Safety
108///
109/// `proof.per_air.len()` must be at least `CONNECTOR_AIR_ID + 1`.
110pub fn get_connector_pvs<C: Config>(
111    builder: &mut Builder<C>,
112    proof: &StarkProofVariable<C>,
113) -> VmConnectorPvs<Felt<C::F>> {
114    get_connector_pvs_impl(builder, proof, CONNECTOR_AIR_ID)
115}
116
117/// # Safety
118///
119/// `proof.per_air.len()` must be greater than `connector_air_id`.
120fn get_connector_pvs_impl<C: Config>(
121    builder: &mut Builder<C>,
122    proof: &StarkProofVariable<C>,
123    connector_air_id: usize,
124) -> VmConnectorPvs<Felt<C::F>> {
125    let a_id = RVar::from(connector_air_id);
126    let a_input = builder.get(&proof.per_air, a_id);
127    let proof_pvs = &a_input.public_values;
128    VmConnectorPvs {
129        initial_pc: builder.get(proof_pvs, 0),
130        final_pc: builder.get(proof_pvs, 1),
131        exit_code: builder.get(proof_pvs, 2),
132        is_terminate: builder.get(proof_pvs, 3),
133    }
134}
135
136/// # Safety
137///
138/// `proof.per_air.len()` must be at least `MERKLE_AIR_ID + 1`.
139pub fn get_memory_pvs<C: Config>(
140    builder: &mut Builder<C>,
141    proof: &StarkProofVariable<C>,
142) -> MemoryMerklePvs<Felt<C::F>, DIGEST_SIZE> {
143    let a_id = RVar::from(MERKLE_AIR_ID);
144    let a_input = builder.get(&proof.per_air, a_id);
145    MemoryMerklePvs {
146        initial_root: array::from_fn(|i| builder.get(&a_input.public_values, i)),
147        final_root: array::from_fn(|i| builder.get(&a_input.public_values, i + DIGEST_SIZE)),
148    }
149}
150
151/// Asserts that a single segment VM  exits successfully.
152///
153/// # Safety
154///
155/// `proof.per_air.len()` must be at least `CONNECTOR_AIR_ID + 1`.
156pub fn assert_single_segment_vm_exit_successfully<C: Config>(
157    builder: &mut Builder<C>,
158    proof: &StarkProofVariable<C>,
159) {
160    assert_single_segment_vm_exit_successfully_with_connector_air_id(
161        builder,
162        proof,
163        CONNECTOR_AIR_ID,
164    )
165}
166
167/// # Safety
168///
169/// `proof.per_air.len()` must be greater than `connector_air_id`.
170pub fn assert_single_segment_vm_exit_successfully_with_connector_air_id<C: Config>(
171    builder: &mut Builder<C>,
172    proof: &StarkProofVariable<C>,
173    connector_air_id: usize,
174) {
175    let connector_pvs = get_connector_pvs_impl(builder, proof, connector_air_id);
176    // Start PC should be 0
177    builder.assert_felt_eq(connector_pvs.initial_pc, C::F::ZERO);
178    // Terminate should be 1
179    builder.assert_felt_eq(connector_pvs.is_terminate, C::F::ONE);
180    // Exit code should be 0
181    builder.assert_felt_eq(connector_pvs.exit_code, C::F::ZERO);
182}
183
184/// Asserts that the aggregation VM proof contains the required fixed AIR slots.
185///
186/// This also establishes `proof.per_air.len() >= PUBLIC_VALUES_AIR_ID + 1`.
187pub fn assert_required_air_for_agg_vm_present<C: Config>(
188    builder: &mut Builder<C>,
189    proof: &StarkProofVariable<C>,
190) {
191    builder.assert_less_than_slow_small_lhs(RVar::from(PUBLIC_VALUES_AIR_ID), proof.per_air.len());
192
193    let program_air = builder.get(&proof.per_air, PROGRAM_AIR_ID);
194    builder.assert_usize_eq(program_air.air_id, RVar::from(PROGRAM_AIR_ID));
195    let connector_air = builder.get(&proof.per_air, CONNECTOR_AIR_ID);
196    builder.assert_usize_eq(connector_air.air_id, RVar::from(CONNECTOR_AIR_ID));
197    let public_values_air = builder.get(&proof.per_air, PUBLIC_VALUES_AIR_ID);
198    builder.assert_usize_eq(public_values_air.air_id, RVar::from(PUBLIC_VALUES_AIR_ID));
199}
200
201/// Asserts that the app VM proof contains the required fixed AIR slots.
202///
203/// This also establishes `proof.per_air.len() >= MERKLE_AIR_ID + 1`.
204pub fn assert_required_air_for_app_vm_present<C: Config>(
205    builder: &mut Builder<C>,
206    proof: &StarkProofVariable<C>,
207) {
208    builder.assert_less_than_slow_small_lhs(RVar::from(MERKLE_AIR_ID), proof.per_air.len());
209
210    let program_air = builder.get(&proof.per_air, PROGRAM_AIR_ID);
211    builder.assert_usize_eq(program_air.air_id, RVar::from(PROGRAM_AIR_ID));
212    let connector_air = builder.get(&proof.per_air, CONNECTOR_AIR_ID);
213    builder.assert_usize_eq(connector_air.air_id, RVar::from(CONNECTOR_AIR_ID));
214    let merkle_air = builder.get(&proof.per_air, MERKLE_AIR_ID);
215    builder.assert_usize_eq(merkle_air.air_id, RVar::from(MERKLE_AIR_ID));
216}
openvm_continuations/verifier/common/mod.rs

openvm_continuations/verifier/common/
mod.rs
