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::FieldAlgebra, p3_util::log2_strict_usize,
15        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                let proof_connector_pvs = get_connector_pvs(builder, &proof);
83                assert_or_assign_connector_pvs(builder, &pvs.connector, i, &proof_connector_pvs);
84
85                let proof_memory_pvs = get_memory_pvs(builder, &proof);
86                assert_or_assign_memory_pvs(builder, &pvs.memory, i, &proof_memory_pvs);
87            });
88            builder.cycle_tracker_end("VerifyProofs");
89            builder.cycle_tracker_start("ExtractPublicValuesCommit");
90            let is_terminate = builder.cast_felt_to_var(pvs.connector.is_terminate);
91            builder.if_eq(is_terminate, F::ONE).then(|builder| {
92                let (pv_commit, expected_memory_root) =
93                    self.verify_user_public_values_root(builder);
94                builder.assert_eq::<[_; DIGEST_SIZE]>(pvs.memory.final_root, expected_memory_root);
95                builder.assign(&pvs.public_values_commit, pv_commit);
96            });
97            for pv in pvs.flatten() {
98                builder.commit_public_value(pv);
99            }
100            builder.cycle_tracker_end("ExtractPublicValuesCommit");
101
102            builder.halt();
103        }
104
105        builder.compile_isa_with_options(self.compiler_options)
106    }
107
108    /// Read the public values root proof from the input stream and verify it.
109    /// This verification must be consistent `openvm_circuit::system::memory::tree::public_values`.
110    /// Returns the public values commit and the corresponding memory state root.
111    fn verify_user_public_values_root(
112        &self,
113        builder: &mut Builder<C>,
114    ) -> ([Felt<F>; DIGEST_SIZE], [Felt<F>; DIGEST_SIZE]) {
115        let memory_dimensions = self.app_system_config.memory_config.memory_dimensions();
116        let pv_as = PUBLIC_VALUES_ADDRESS_SPACE_OFFSET + ADDR_SPACE_OFFSET;
117        let pv_start_idx = memory_dimensions.label_to_index((pv_as, 0));
118        let pv_height = log2_strict_usize(self.app_system_config.num_public_values / DIGEST_SIZE);
119        let proof_len = memory_dimensions.overall_height() - pv_height;
120        let idx_prefix = pv_start_idx >> pv_height;
121
122        // Read the public values root proof from the input stream.
123        let root_proof = UserPublicValuesRootProof::<F>::read(builder);
124        builder.assert_eq::<Usize<_>>(root_proof.sibling_hashes.len(), Usize::from(proof_len));
125        let mut curr_commit = root_proof.public_values_commit;
126        // Share the same state array to avoid unnecessary allocations.
127        let compressor = VariableP2Compressor::new(builder);
128        for i in 0..proof_len {
129            let sibling_hash = builder.get(&root_proof.sibling_hashes, i);
130            let (l_hash, r_hash) = if idx_prefix & (1 << i) != 0 {
131                (sibling_hash, curr_commit)
132            } else {
133                (curr_commit, sibling_hash)
134            };
135            curr_commit = compressor.compress(builder, &l_hash, &r_hash);
136        }
137        (root_proof.public_values_commit, curr_commit)
138    }
139}