openvm_continuations/verifier/leaf/
mod.rs

1use openvm_circuit::{
2    arch::{instructions::program::Program, SystemConfig, ADDR_SPACE_OFFSET},
3    system::memory::merkle::public_values::PUBLIC_VALUES_ADDRESS_SPACE_OFFSET,
4};
5use openvm_native_compiler::{conversion::CompilerOptions, prelude::*};
6use openvm_native_recursion::{
7    challenger::duplex::DuplexChallengerVariable, fri::TwoAdicFriPcsVariable, hints::Hintable,
8    stark::StarkVerifier, types::new_from_inner_multi_vk, utils::const_fri_config,
9    vars::StarkProofVariable,
10};
11use openvm_stark_sdk::{
12    config::{baby_bear_poseidon2::BabyBearPoseidon2Config, FriParameters},
13    openvm_stark_backend::{
14        keygen::types::MultiStarkVerifyingKey, p3_field::PrimeCharacteristicRing,
15        p3_util::log2_strict_usize, proof::Proof,
16    },
17};
18
19use crate::{
20    verifier::{
21        common::{
22            assert_or_assign_connector_pvs, assert_or_assign_memory_pvs,
23            assert_required_air_for_app_vm_present, get_connector_pvs, get_memory_pvs,
24            get_program_commit, types::VmVerifierPvs,
25        },
26        leaf::types::UserPublicValuesRootProof,
27        utils::VariableP2Compressor,
28    },
29    C, F,
30};
31
32pub mod types;
33mod vars;
34
35/// Config to generate leaf VM verifier program.
36pub struct LeafVmVerifierConfig {
37    pub app_fri_params: FriParameters,
38    pub app_system_config: SystemConfig,
39    pub compiler_options: CompilerOptions,
40}
41
42impl LeafVmVerifierConfig {
43    pub fn build_program(
44        &self,
45        app_vm_vk: &MultiStarkVerifyingKey<BabyBearPoseidon2Config>,
46    ) -> Program<F> {
47        let m_advice = new_from_inner_multi_vk(app_vm_vk);
48        let mut builder = Builder::<C>::default();
49
50        {
51            builder.cycle_tracker_start("InitializePcsConst");
52            let pcs = TwoAdicFriPcsVariable {
53                config: const_fri_config(&mut builder, &self.app_fri_params),
54            };
55            builder.cycle_tracker_end("InitializePcsConst");
56            builder.cycle_tracker_start("ReadProofsFromInput");
57            let proofs: Array<C, StarkProofVariable<_>> =
58                <Vec<Proof<BabyBearPoseidon2Config>> as Hintable<C>>::read(&mut builder);
59            // At least 1 proof should be provided.
60            builder.assert_nonzero(&proofs.len());
61            builder.cycle_tracker_end("ReadProofsFromInput");
62
63            builder.cycle_tracker_start("VerifyProofs");
64            let pvs = VmVerifierPvs::<Felt<F>>::uninit(&mut builder);
65            builder.range(0, proofs.len()).for_each(|i_vec, builder| {
66                let i = i_vec[0];
67                let proof = builder.get(&proofs, i);
68                assert_required_air_for_app_vm_present(builder, &proof);
69                StarkVerifier::verify::<DuplexChallengerVariable<C>>(
70                    builder, &pcs, &m_advice, &proof,
71                );
72                {
73                    let commit = get_program_commit(builder, &proof);
74                    builder.if_eq(i, RVar::zero()).then_or_else(
75                        |builder| {
76                            builder.assign(&pvs.app_commit, commit);
77                        },
78                        |builder| builder.assert_eq::<[_; DIGEST_SIZE]>(pvs.app_commit, commit),
79                    );
80                }
81
82                // SAFETY: `assert_required_air_for_app_vm_present` has already ensured
83                // `CONNECTOR_AIR_ID < proof.per_air.len()`.
84                let proof_connector_pvs = get_connector_pvs(builder, &proof);
85                assert_or_assign_connector_pvs(builder, &pvs.connector, i, &proof_connector_pvs);
86
87                // SAFETY: `assert_required_air_for_app_vm_present` has already ensured
88                // `MERKLE_AIR_ID < proof.per_air.len()`.
89                let proof_memory_pvs = get_memory_pvs(builder, &proof);
90                assert_or_assign_memory_pvs(builder, &pvs.memory, i, &proof_memory_pvs);
91            });
92            builder.cycle_tracker_end("VerifyProofs");
93            builder.cycle_tracker_start("ExtractPublicValuesCommit");
94            let is_terminate = builder.cast_felt_to_var(pvs.connector.is_terminate);
95            builder.if_eq(is_terminate, F::ONE).then(|builder| {
96                let (pv_commit, expected_memory_root) =
97                    self.verify_user_public_values_root(builder);
98                builder.assert_eq::<[_; DIGEST_SIZE]>(pvs.memory.final_root, expected_memory_root);
99                builder.assign(&pvs.public_values_commit, pv_commit);
100            });
101            for pv in pvs.flatten() {
102                builder.commit_public_value(pv);
103            }
104            builder.cycle_tracker_end("ExtractPublicValuesCommit");
105
106            builder.halt();
107        }
108
109        builder.compile_isa_with_options(self.compiler_options)
110    }
111
112    /// Read the public values root proof from the input stream and verify it.
113    /// This verification must be consistent `openvm_circuit::system::memory::tree::public_values`.
114    /// Returns the public values commit and the corresponding memory state root.
115    fn verify_user_public_values_root(
116        &self,
117        builder: &mut Builder<C>,
118    ) -> ([Felt<F>; DIGEST_SIZE], [Felt<F>; DIGEST_SIZE]) {
119        let memory_dimensions = self.app_system_config.memory_config.memory_dimensions();
120        let pv_as = PUBLIC_VALUES_ADDRESS_SPACE_OFFSET + ADDR_SPACE_OFFSET;
121        let pv_start_idx = memory_dimensions.label_to_index((pv_as, 0));
122        let pv_height = log2_strict_usize(self.app_system_config.num_public_values / DIGEST_SIZE);
123        let proof_len = memory_dimensions.overall_height() - pv_height;
124        let idx_prefix = pv_start_idx >> pv_height;
125
126        // Read the public values root proof from the input stream.
127        let root_proof = UserPublicValuesRootProof::<F>::read(builder);
128        builder.assert_eq::<Usize<_>>(root_proof.sibling_hashes.len(), Usize::from(proof_len));
129        let mut curr_commit = root_proof.public_values_commit;
130        // Share the same state array to avoid unnecessary allocations.
131        let compressor = VariableP2Compressor::new(builder);
132        for i in 0..proof_len {
133            let sibling_hash = builder.get(&root_proof.sibling_hashes, i);
134            let (l_hash, r_hash) = if idx_prefix & (1 << i) != 0 {
135                (sibling_hash, curr_commit)
136            } else {
137                (curr_commit, sibling_hash)
138            };
139            curr_commit = compressor.compress(builder, &l_hash, &r_hash);
140        }
141        (root_proof.public_values_commit, curr_commit)
142    }
143}
openvm_continuations/verifier/leaf/mod.rs

openvm_continuations/verifier/leaf/
mod.rs
