-
Notifications
You must be signed in to change notification settings - Fork 26
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Leaf verifier program verifies public values root
- Loading branch information
1 parent
5025033
commit 8590509
Showing
11 changed files
with
354 additions
and
72 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,90 @@ | ||
| use std::{array, borrow::BorrowMut}; | ||
|
|
||
| use ax_stark_sdk::ax_stark_backend::{ | ||
| config::{Com, StarkGenericConfig, Val}, | ||
| p3_field::PrimeField32, | ||
| prover::types::Proof, | ||
| }; | ||
| use axvm_circuit::{ | ||
| circuit_derive::AlignedBorrow, | ||
| system::{ | ||
| connector::VmConnectorPvs, | ||
| memory::{merkle::MemoryMerklePvs, tree::public_values::UserPublicValuesProof}, | ||
| }, | ||
| }; | ||
| use axvm_native_compiler::ir::{Builder, Config, Felt, DIGEST_SIZE}; | ||
| use derivative::Derivative; | ||
| use serde::{Deserialize, Serialize}; | ||
|
|
||
| #[derive(Debug, AlignedBorrow)] | ||
| #[repr(C)] | ||
| pub struct LeafVmVerifierPvs<T> { | ||
| pub app_commit: [T; DIGEST_SIZE], | ||
| pub connector: VmConnectorPvs<T>, | ||
| pub memory: MemoryMerklePvs<T, DIGEST_SIZE>, | ||
| pub public_values_commit: [T; DIGEST_SIZE], | ||
| } | ||
|
|
||
| /// Input for the leaf VM verifier. | ||
| #[derive(Serialize, Deserialize, Derivative)] | ||
| #[serde(bound = "")] | ||
| #[derivative(Clone(bound = "Com<SC>: Clone"))] | ||
| pub struct LeafVmVerifierInput<SC: StarkGenericConfig> { | ||
| /// The proofs of the execution segments in the execution order. | ||
| pub proofs: Vec<Proof<SC>>, | ||
| /// The public values root proof. Leaf VM verifier only needs this when verifying the last | ||
| /// segment. | ||
| pub public_values_root_proof: Option<UserPublicValuesRootProof<Val<SC>>>, | ||
| } | ||
|
|
||
| /// Proof that the merkle root of public values is in the memory state. Can be extracted from | ||
| /// `axvm-circuit::system::memory::public_values::UserPublicValuesProof`. | ||
| #[derive(Serialize, Deserialize, Clone, Debug)] | ||
| pub struct UserPublicValuesRootProof<F> { | ||
| /// Sibling hashes for proving the merkle root of public values. For a specific VM, the path | ||
| /// is constant. So we don't need the boolean which indicates if a node is a left child or right | ||
| /// child. | ||
| pub sibling_hashes: Vec<[F; DIGEST_SIZE]>, | ||
| pub public_values_commit: [F; DIGEST_SIZE], | ||
| } | ||
|
|
||
| impl<F: PrimeField32> LeafVmVerifierPvs<Felt<F>> { | ||
| pub(crate) fn uninit<C: Config<F = F>>(builder: &mut Builder<C>) -> Self { | ||
| Self { | ||
| app_commit: array::from_fn(|_| builder.uninit()), | ||
| connector: VmConnectorPvs { | ||
| initial_pc: builder.uninit(), | ||
| final_pc: builder.uninit(), | ||
| exit_code: builder.uninit(), | ||
| is_terminate: builder.uninit(), | ||
| }, | ||
| memory: MemoryMerklePvs { | ||
| initial_root: array::from_fn(|_| builder.uninit()), | ||
| final_root: array::from_fn(|_| builder.uninit()), | ||
| }, | ||
| public_values_commit: array::from_fn(|_| builder.uninit()), | ||
| } | ||
| } | ||
| } | ||
|
|
||
| impl<F: Default + Clone> LeafVmVerifierPvs<Felt<F>> { | ||
| pub fn flatten(self) -> Vec<Felt<F>> { | ||
| let mut v = vec![Felt(0, Default::default()); LeafVmVerifierPvs::<u8>::width()]; | ||
| *v.as_mut_slice().borrow_mut() = self; | ||
| v | ||
| } | ||
| } | ||
|
|
||
| impl<F: Clone> UserPublicValuesRootProof<F> { | ||
| pub fn extract(pvs_proof: &UserPublicValuesProof<{ DIGEST_SIZE }, F>) -> Self { | ||
| Self { | ||
| sibling_hashes: pvs_proof | ||
| .proof | ||
| .clone() | ||
| .into_iter() | ||
| .map(|(_, hash)| hash) | ||
| .collect(), | ||
| public_values_commit: pvs_proof.public_values_commit.clone(), | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| use std::array; | ||
|
|
||
| use ax_stark_sdk::ax_stark_backend::{ | ||
| config::{StarkGenericConfig, Val}, | ||
| p3_field::AbstractField, | ||
| prover::types::Proof, | ||
| }; | ||
| use axvm_native_compiler::prelude::*; | ||
| use axvm_recursion::{ | ||
| hints::{Hintable, InnerVal}, | ||
| types::InnerConfig, | ||
| }; | ||
|
|
||
| use crate::verifier::leaf::types::{LeafVmVerifierInput, UserPublicValuesRootProof}; | ||
|
|
||
| #[derive(DslVariable, Clone)] | ||
| pub struct UserPublicValuesRootProofVariable<const CHUNK: usize, C: Config> { | ||
| /// Sibling hashes for proving the merkle root of public values. For a specific VM, the path | ||
| /// is constant. So we don't need the boolean which indicates if a node is a left child or right | ||
| /// child. | ||
| pub sibling_hashes: Array<C, [Felt<C::F>; CHUNK]>, | ||
| pub public_values_commit: [Felt<C::F>; CHUNK], | ||
| } | ||
|
|
||
| type C = InnerConfig; | ||
| type F = InnerVal; | ||
|
|
||
| impl<SC: StarkGenericConfig> LeafVmVerifierInput<SC> { | ||
| pub fn write_to_stream<C: Config<N = Val<SC>>>(&self) -> Vec<Vec<Val<SC>>> | ||
| where | ||
| Vec<Proof<SC>>: Hintable<C>, | ||
| UserPublicValuesRootProof<Val<SC>>: Hintable<C>, | ||
| { | ||
| let mut ret = Hintable::<C>::write(&self.proofs); | ||
| if let Some(pvs_root_proof) = &self.public_values_root_proof { | ||
| ret.extend(Hintable::<C>::write(pvs_root_proof)); | ||
| } | ||
| ret | ||
| } | ||
| } | ||
|
|
||
| impl Hintable<C> for UserPublicValuesRootProof<F> { | ||
| type HintVariable = UserPublicValuesRootProofVariable<{ DIGEST_SIZE }, C>; | ||
| fn read(builder: &mut Builder<C>) -> Self::HintVariable { | ||
| let len = builder.hint_var(); | ||
| let sibling_hashes = builder.array(len); | ||
| builder.range(0, len).for_each(|i, builder| { | ||
| // FIXME: add hint support for slices. | ||
| let hash = array::from_fn(|_| builder.hint_felt()); | ||
| builder.set_value(&sibling_hashes, i, hash); | ||
| }); | ||
| let public_values_commit = array::from_fn(|_| builder.hint_felt()); | ||
| Self::HintVariable { | ||
| sibling_hashes, | ||
| public_values_commit, | ||
| } | ||
| } | ||
| fn write(&self) -> Vec<Vec<<C as Config>::N>> { | ||
| let len = <<C as Config>::N>::from_canonical_usize(self.sibling_hashes.len()); | ||
| let mut stream = len.write(); | ||
| stream.extend(self.sibling_hashes.iter().flat_map(write_field_slice)); | ||
| stream.extend(write_field_slice(&self.public_values_commit)); | ||
| stream | ||
| } | ||
| } | ||
|
|
||
| fn write_field_slice(arr: &[F; DIGEST_SIZE]) -> Vec<Vec<<C as Config>::N>> { | ||
| arr.iter().flat_map(|x| x.write()).collect() | ||
| } |
Oops, something went wrong.