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::FieldAlgebra;
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
107pub fn get_connector_pvs<C: Config>(
108    builder: &mut Builder<C>,
109    proof: &StarkProofVariable<C>,
110) -> VmConnectorPvs<Felt<C::F>> {
111    get_connector_pvs_impl(builder, proof, CONNECTOR_AIR_ID)
112}
113
114fn get_connector_pvs_impl<C: Config>(
115    builder: &mut Builder<C>,
116    proof: &StarkProofVariable<C>,
117    connector_air_id: usize,
118) -> VmConnectorPvs<Felt<C::F>> {
119    let a_id = RVar::from(connector_air_id);
120    let a_input = builder.get(&proof.per_air, a_id);
121    let proof_pvs = &a_input.public_values;
122    VmConnectorPvs {
123        initial_pc: builder.get(proof_pvs, 0),
124        final_pc: builder.get(proof_pvs, 1),
125        exit_code: builder.get(proof_pvs, 2),
126        is_terminate: builder.get(proof_pvs, 3),
127    }
128}
129
130pub fn get_memory_pvs<C: Config>(
131    builder: &mut Builder<C>,
132    proof: &StarkProofVariable<C>,
133) -> MemoryMerklePvs<Felt<C::F>, DIGEST_SIZE> {
134    let a_id = RVar::from(MERKLE_AIR_ID);
135    let a_input = builder.get(&proof.per_air, a_id);
136    MemoryMerklePvs {
137        initial_root: array::from_fn(|i| builder.get(&a_input.public_values, i)),
138        final_root: array::from_fn(|i| builder.get(&a_input.public_values, i + DIGEST_SIZE)),
139    }
140}
141
142/// Asserts that a single segment VM  exits successfully.
143pub fn assert_single_segment_vm_exit_successfully<C: Config>(
144    builder: &mut Builder<C>,
145    proof: &StarkProofVariable<C>,
146) {
147    assert_single_segment_vm_exit_successfully_with_connector_air_id(
148        builder,
149        proof,
150        CONNECTOR_AIR_ID,
151    )
152}
153
154pub fn assert_single_segment_vm_exit_successfully_with_connector_air_id<C: Config>(
155    builder: &mut Builder<C>,
156    proof: &StarkProofVariable<C>,
157    connector_air_id: usize,
158) {
159    let connector_pvs = get_connector_pvs_impl(builder, proof, connector_air_id);
160    // Start PC should be 0
161    builder.assert_felt_eq(connector_pvs.initial_pc, C::F::ZERO);
162    // Terminate should be 1
163    builder.assert_felt_eq(connector_pvs.is_terminate, C::F::ONE);
164    // Exit code should be 0
165    builder.assert_felt_eq(connector_pvs.exit_code, C::F::ZERO);
166}
167
168// TODO: This is a temporary solution. VK should be able to specify which AIRs are required. Once
169// that is implemented in stark-backend, this function can be removed.
170pub fn assert_required_air_for_agg_vm_present<C: Config>(
171    builder: &mut Builder<C>,
172    proof: &StarkProofVariable<C>,
173) {
174    let program_air = builder.get(&proof.per_air, PROGRAM_AIR_ID);
175    builder.assert_usize_eq(program_air.air_id, RVar::from(PROGRAM_AIR_ID));
176    let connector_air = builder.get(&proof.per_air, CONNECTOR_AIR_ID);
177    builder.assert_usize_eq(connector_air.air_id, RVar::from(CONNECTOR_AIR_ID));
178    let public_values_air = builder.get(&proof.per_air, PUBLIC_VALUES_AIR_ID);
179    builder.assert_usize_eq(public_values_air.air_id, RVar::from(PUBLIC_VALUES_AIR_ID));
180}
181
182// TODO: This is a temporary solution. VK should be able to specify which AIRs are required. Once
183// that is implemented, this function can be removed.
184pub fn assert_required_air_for_app_vm_present<C: Config>(
185    builder: &mut Builder<C>,
186    proof: &StarkProofVariable<C>,
187) {
188    let program_air = builder.get(&proof.per_air, PROGRAM_AIR_ID);
189    builder.assert_usize_eq(program_air.air_id, RVar::from(PROGRAM_AIR_ID));
190    let connector_air = builder.get(&proof.per_air, CONNECTOR_AIR_ID);
191    builder.assert_usize_eq(connector_air.air_id, RVar::from(CONNECTOR_AIR_ID));
192    let public_values_air = builder.get(&proof.per_air, MERKLE_AIR_ID);
193    builder.assert_usize_eq(public_values_air.air_id, RVar::from(MERKLE_AIR_ID));
194}
openvm_continuations/verifier/common/mod.rs

openvm_continuations/verifier/common/
mod.rs
