From b9fbdeaa8a97ec80d07a627806945529daa11d99 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Thu, 11 Dec 2025 15:59:12 -0500 Subject: [PATCH 01/12] Structure new pv [skip ci] --- ceno_recursion/src/aggregation/types.rs | 84 ++++++++++++++----------- 1 file changed, 49 insertions(+), 35 deletions(-) diff --git a/ceno_recursion/src/aggregation/types.rs b/ceno_recursion/src/aggregation/types.rs index be88a6fb8..56ab2b69a 100644 --- a/ceno_recursion/src/aggregation/types.rs +++ b/ceno_recursion/src/aggregation/types.rs @@ -1,38 +1,52 @@ -// TODO: enable this -// #[derive(Debug, Clone, AlignedBorrow)] -// pub struct ContinuationPvs { -// pub sum: SepticPoint, -// } -// impl ContinuationPvs> { -// pub fn uninit(builder: &mut Builder) -> Self { -// todo!() -// } -// } +use openvm_continuations::F; +use ceno_zkvm::scheme::{constants::SEPTIC_EXTENSION_DEGREE, septic_curve::SepticPoint}; +use openvm_circuit::system::connector::VmConnectorPvs; +use crate::zkvm_verifier::binding::{SepticPointVariable, SepticExtensionVariable}; +use openvm_native_compiler::{ + prelude::*, + ir::{Array, Builder, Config, DIGEST_SIZE, Felt, Variable}, +}; +use std::array; -// #[derive(Debug, Clone, AlignedBorrow)] -// #[repr(C)] -// pub struct VmVerifierPvs { -// /// The merged execution state of all the segments this circuit aggregates. -// pub connector: VmConnectorPvs, -// /// The state before/after all the segments this circuit aggregates. -// // (TODO) pub shard_ram_connector: ContinuationPvs, -// /// The merkle root of all public values. This is only meaningful when the last segment is -// /// aggregated by this circuit. -// pub public_values_commit: [T; DIGEST_SIZE], -// } +#[derive(Clone)] +pub struct ContinuationPvs { + pub xy: [Felt; SEPTIC_EXTENSION_DEGREE * 2], + pub is_infinity: Usize, +} -// impl VmVerifierPvs> { -// pub fn uninit(builder: &mut Builder) -> Self { -// VmVerifierPvs { -// connector: VmConnectorPvs { -// initial_pc: builder.uninit(), -// final_pc: builder.uninit(), -// exit_code: builder.uninit(), -// is_terminate: builder.uninit(), -// }, -// // shard_ram_connector: builder.uninit(), -// public_values_commit: array::from_fn(|_| builder.uninit()), -// } -// } -// } +impl ContinuationPvs { + pub fn uninit(builder: &mut Builder) -> Self { + Self { + xy: array::from_fn(|_| builder.uninit()), + is_infinity: Usize::uninit(builder), + } + } +} + +#[derive(Clone)] +#[repr(C)] +pub struct VmVerifierPvs { + /// The merged execution state of all the segments this circuit aggregates. + pub connector: VmConnectorPvs>, + /// The state before/after all the segments this circuit aggregates. + pub shard_ram_connector: ContinuationPvs, + /// The merkle root of all public values. This is only meaningful when the last segment is + /// aggregated by this circuit. + pub public_values_commit: [Felt; DIGEST_SIZE], +} + +impl VmVerifierPvs { + pub fn uninit(builder: &mut Builder) -> Self { + VmVerifierPvs { + connector: VmConnectorPvs { + initial_pc: builder.uninit(), + final_pc: builder.uninit(), + exit_code: builder.uninit(), + is_terminate: builder.uninit(), + }, + shard_ram_connector: ContinuationPvs::uninit(builder), + public_values_commit: array::from_fn(|_| builder.uninit()), + } + } +} From 0294ab71e795843fd613db2b45e6c94f1149b7db Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 14 Dec 2025 16:20:27 -0500 Subject: [PATCH 02/12] pv substitution --- ceno_recursion/src/aggregation/internal.rs | 24 +++--- ceno_recursion/src/aggregation/mod.rs | 15 ++-- ceno_recursion/src/aggregation/types.rs | 98 ++++++++++++++++++---- 3 files changed, 104 insertions(+), 33 deletions(-) diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index bd494a0e9..2a207ad1e 100644 --- a/ceno_recursion/src/aggregation/internal.rs +++ b/ceno_recursion/src/aggregation/internal.rs @@ -24,14 +24,13 @@ use p3::field::FieldAlgebra; use openvm_continuations::verifier::{ common::{ assert_or_assign_connector_pvs, assert_required_air_for_agg_vm_present, - assert_single_segment_vm_exit_successfully, get_program_commit, types::VmVerifierPvs, - }, - internal::{ - types::{InternalVmVerifierExtraPvs, InternalVmVerifierInput, InternalVmVerifierPvs}, - vars::InternalVmVerifierInputVariable, + assert_single_segment_vm_exit_successfully, get_program_commit, }, }; use openvm_native_recursion::hints::Hintable; +use openvm_continuations::verifier::internal::vars::InternalVmVerifierInputVariable; +use crate::aggregation::InternalVmVerifierInput; +use crate::aggregation::types::{InternalVmVerifierPvs, InternalVmVerifierExtraPvs, VmVerifierPvs}; use openvm_continuations::{C, F}; use openvm_native_recursion::types::new_from_inner_multi_vk; @@ -101,17 +100,21 @@ impl NonLeafVerifierVariables { builder.if_eq(i, RVar::zero()).then_or_else( |builder| { - builder.assign(&pvs.app_commit, proof_vm_pvs.vm_verifier_pvs.app_commit); + // _debug + // builder.assign(&pvs.app_commit, proof_vm_pvs.vm_verifier_pvs.app_commit); + builder.assign( &leaf_verifier_commit, proof_vm_pvs.extra_pvs.leaf_verifier_commit, ); }, |builder| { - builder.assert_eq::<[_; DIGEST_SIZE]>( - pvs.app_commit, - proof_vm_pvs.vm_verifier_pvs.app_commit, - ); + // _debug + // builder.assert_eq::<[_; DIGEST_SIZE]>( + // pvs.app_commit, + // proof_vm_pvs.vm_verifier_pvs.app_commit, + // ); + builder.assert_eq::<[_; DIGEST_SIZE]>( leaf_verifier_commit, proof_vm_pvs.extra_pvs.leaf_verifier_commit, @@ -301,6 +304,7 @@ impl InternalVmVerifierConfig { internal_pcs, internal_advice, }; + builder.cycle_tracker_start("VerifyProofs"); let (vm_verifier_pvs, leaf_verifier_commit) = non_leaf_verifier.verify_internal_or_leaf_verifier_proofs(&mut builder, &proofs); diff --git a/ceno_recursion/src/aggregation/mod.rs b/ceno_recursion/src/aggregation/mod.rs index 729b774a5..3086fea3b 100644 --- a/ceno_recursion/src/aggregation/mod.rs +++ b/ceno_recursion/src/aggregation/mod.rs @@ -25,8 +25,7 @@ use internal::InternalVmVerifierConfig; use openvm_continuations::{ C, verifier::{ - common::types::VmVerifierPvs, - internal::types::{InternalVmVerifierInput, InternalVmVerifierPvs, VmStarkProof}, + internal::types::{InternalVmVerifierInput, VmStarkProof}, root::types::RootVmVerifierInput, }, }; @@ -81,6 +80,7 @@ use openvm_native_compiler::{ use openvm_sdk::util::check_max_constraint_degrees; use openvm_stark_backend::proof::Proof; use openvm_stark_sdk::config::baby_bear_poseidon2_root::BabyBearPoseidon2RootEngine; +use crate::aggregation::types::{VmVerifierPvs, InternalVmVerifierPvs}; mod internal; mod root; @@ -454,9 +454,9 @@ impl CenoLeafVmVerifierConfig { builder.cycle_tracker_start("PV Operations"); // TODO: define our own VmVerifierPvs - for i in 0..DIGEST_SIZE { - builder.assign(&stark_pvs.app_commit[i], F::ZERO); - } + // for i in 0..DIGEST_SIZE { + // builder.assign(&stark_pvs.app_commit[i], F::ZERO); + // } let pv = &raw_pi; let init_pc = { @@ -504,7 +504,6 @@ impl CenoLeafVmVerifierConfig { // ); // builder.assign(&prev_pc, end_pc); // }); - // }); for pv in stark_pvs.flatten() { @@ -611,6 +610,7 @@ pub(crate) fn chunk_ceno_leaf_proof_inputs( ret } +/* // Source from OpenVm SDK::verify_e2e_stark_proof with abridged key // See: https://github.com/openvm-org/openvm pub fn verify_e2e_stark_proof( @@ -708,6 +708,7 @@ pub fn verify_e2e_stark_proof( // } Ok(app_commit) } +*/ /// Build Ceno's zkVM verifier program from vk in OpenVM's eDSL pub fn build_zkvm_verifier_program( @@ -843,7 +844,7 @@ mod tests { } #[test] - #[ignore = "need to generate proof first"] + // #[ignore = "need to generate proof first"] pub fn test_aggregation() { let stack_size = 256 * 1024 * 1024; // 64 MB diff --git a/ceno_recursion/src/aggregation/types.rs b/ceno_recursion/src/aggregation/types.rs index 56ab2b69a..dd633b824 100644 --- a/ceno_recursion/src/aggregation/types.rs +++ b/ceno_recursion/src/aggregation/types.rs @@ -1,43 +1,47 @@ use openvm_continuations::F; use ceno_zkvm::scheme::{constants::SEPTIC_EXTENSION_DEGREE, septic_curve::SepticPoint}; -use openvm_circuit::system::connector::VmConnectorPvs; +use openvm_circuit::{circuit_derive::AlignedBorrow, system::connector::VmConnectorPvs}; +use p3::field::PrimeField32; use crate::zkvm_verifier::binding::{SepticPointVariable, SepticExtensionVariable}; use openvm_native_compiler::{ prelude::*, ir::{Array, Builder, Config, DIGEST_SIZE, Felt, Variable}, }; use std::array; +use std::borrow::BorrowMut; -#[derive(Clone)] -pub struct ContinuationPvs { - pub xy: [Felt; SEPTIC_EXTENSION_DEGREE * 2], - pub is_infinity: Usize, +#[derive(Clone, Copy, AlignedBorrow)] +pub struct ContinuationPvs { + pub x: [T; SEPTIC_EXTENSION_DEGREE], + pub y: [T; SEPTIC_EXTENSION_DEGREE], + pub is_infinity: T, } -impl ContinuationPvs { - pub fn uninit(builder: &mut Builder) -> Self { +impl ContinuationPvs> { + pub fn uninit>(builder: &mut Builder) -> Self { Self { - xy: array::from_fn(|_| builder.uninit()), - is_infinity: Usize::uninit(builder), + x: array::from_fn(|_| builder.uninit()), + y: array::from_fn(|_| builder.uninit()), + is_infinity: Felt::uninit(builder), } } } -#[derive(Clone)] +#[derive(Clone, Copy, AlignedBorrow)] #[repr(C)] -pub struct VmVerifierPvs { +pub struct VmVerifierPvs { /// The merged execution state of all the segments this circuit aggregates. - pub connector: VmConnectorPvs>, + pub connector: VmConnectorPvs, /// The state before/after all the segments this circuit aggregates. - pub shard_ram_connector: ContinuationPvs, + pub shard_ram_connector: ContinuationPvs, /// The merkle root of all public values. This is only meaningful when the last segment is /// aggregated by this circuit. - pub public_values_commit: [Felt; DIGEST_SIZE], + pub public_values_commit: [T; DIGEST_SIZE], } -impl VmVerifierPvs { - pub fn uninit(builder: &mut Builder) -> Self { +impl VmVerifierPvs> { + pub fn uninit>(builder: &mut Builder) -> Self { VmVerifierPvs { connector: VmConnectorPvs { initial_pc: builder.uninit(), @@ -50,3 +54,65 @@ impl VmVerifierPvs { } } } + +impl VmVerifierPvs> { + pub fn flatten(self) -> Vec> { + let mut v = vec![Felt(0, Default::default()); VmVerifierPvs::::width()]; + *v.as_mut_slice().borrow_mut() = self; + v + } +} + +/// Aggregated state of all segments +#[derive(Clone, Copy, AlignedBorrow)] +#[repr(C)] +pub struct InternalVmVerifierPvs { + pub vm_verifier_pvs: VmVerifierPvs, + pub extra_pvs: InternalVmVerifierExtraPvs, +} + +/// Extra PVs for internal VM verifier except VmVerifierPvs. +#[derive(Clone, Copy, AlignedBorrow)] +#[repr(C)] +pub struct InternalVmVerifierExtraPvs { + /// The commitment of the leaf verifier program. + pub leaf_verifier_commit: [T; DIGEST_SIZE], + /// For recursion verification, a program need its own commitment, but its own commitment + /// cannot be hardcoded inside the program itself. So the commitment has to be read from + /// external and be committed. + pub internal_program_commit: [T; DIGEST_SIZE], +} + +impl InternalVmVerifierPvs> { + pub fn uninit>(builder: &mut Builder) -> Self { + Self { + vm_verifier_pvs: VmVerifierPvs::>::uninit(builder), + extra_pvs: InternalVmVerifierExtraPvs::>::uninit(builder), + } + } +} + +impl InternalVmVerifierPvs> { + pub fn flatten(self) -> Vec> { + let mut v = vec![Felt(0, Default::default()); InternalVmVerifierPvs::::width()]; + *v.as_mut_slice().borrow_mut() = self; + v + } +} + +impl InternalVmVerifierExtraPvs> { + pub fn uninit>(builder: &mut Builder) -> Self { + Self { + leaf_verifier_commit: array::from_fn(|_| builder.uninit()), + internal_program_commit: array::from_fn(|_| builder.uninit()), + } + } +} + +impl InternalVmVerifierExtraPvs> { + pub fn flatten(self) -> Vec> { + let mut v = vec![Felt(0, Default::default()); InternalVmVerifierExtraPvs::::width()]; + *v.as_mut_slice().borrow_mut() = self; + v + } +} From d23dff56703233245749e730a7969bcff357012c Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 14 Dec 2025 16:51:04 -0500 Subject: [PATCH 03/12] assig ec --- ceno_recursion/src/aggregation/mod.rs | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/ceno_recursion/src/aggregation/mod.rs b/ceno_recursion/src/aggregation/mod.rs index 3086fea3b..43d681451 100644 --- a/ceno_recursion/src/aggregation/mod.rs +++ b/ceno_recursion/src/aggregation/mod.rs @@ -7,7 +7,7 @@ use crate::{ }; use ceno_zkvm::{ instructions::riscv::constants::{END_PC_IDX, EXIT_CODE_IDX, INIT_PC_IDX}, - scheme::ZKVMProof, + scheme::{ZKVMProof, constants::SEPTIC_EXTENSION_DEGREE}, structs::ZKVMVerifyingKey, }; use ff_ext::BabyBearExt4; @@ -448,16 +448,10 @@ impl CenoLeafVmVerifierConfig { builder.cycle_tracker_start("Verify Ceno ZKVM Proof"); let zkvm_proof = ceno_leaf_input.proof; let raw_pi = zkvm_proof.raw_pi.clone(); - let _calculated_shard_ec_sum = verify_zkvm_proof(&mut builder, zkvm_proof, &self.vk); + let shard_ec_sum = verify_zkvm_proof(&mut builder, zkvm_proof, &self.vk); builder.cycle_tracker_end("Verify Ceno ZKVM Proof"); builder.cycle_tracker_start("PV Operations"); - - // TODO: define our own VmVerifierPvs - // for i in 0..DIGEST_SIZE { - // builder.assign(&stark_pvs.app_commit[i], F::ZERO); - // } - let pv = &raw_pi; let init_pc = { let arr = builder.get(pv, INIT_PC_IDX); @@ -475,7 +469,22 @@ impl CenoLeafVmVerifierConfig { builder.assign(&stark_pvs.connector.final_pc, end_pc); builder.assign(&stark_pvs.connector.exit_code, exit_code); - // TODO: assign shard_ec_sum to stark_pvs.shard_ec_sum + for i in 0..SEPTIC_EXTENSION_DEGREE { + let x_ext = builder.get(&shard_ec_sum.x.vs, i); + let y_ext = builder.get(&shard_ec_sum.y.vs, i); + let x_fs = builder.ext2felt(x_ext); + let y_fs = builder.ext2felt(y_ext); + let x = builder.get(&x_fs, 0); + let y = builder.get(&y_fs, 0); + + builder.assign(&stark_pvs.shard_ram_connector.x[i], x); + builder.assign(&stark_pvs.shard_ram_connector.y[i], y); + } + builder.if_eq(shard_ec_sum.is_infinity, Usize::from(1)).then_or_else(|builder| { + builder.assign(&stark_pvs.shard_ram_connector.is_infinity, F::ONE); + }, |builder| { + builder.assign(&stark_pvs.shard_ram_connector.is_infinity, F::ZERO); + }); // builder // .if_eq(ceno_leaf_input.is_last, Usize::from(1)) From ab127cbecad8d230ef29af25327e43c25917a032 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 14 Dec 2025 17:58:43 -0500 Subject: [PATCH 04/12] aggregate ec --- ceno_recursion/src/aggregation/internal.rs | 125 ++++++++++----------- 1 file changed, 57 insertions(+), 68 deletions(-) diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index 2a207ad1e..47ebd10a1 100644 --- a/ceno_recursion/src/aggregation/internal.rs +++ b/ceno_recursion/src/aggregation/internal.rs @@ -3,12 +3,13 @@ /// https://github.com/openvm-org/openvm/blob/main/crates/continuations/src/verifier/common/non_leaf.rs use std::{array, borrow::Borrow}; +use ceno_zkvm::scheme::constants::SEPTIC_EXTENSION_DEGREE; use openvm_circuit::arch::PUBLIC_VALUES_AIR_ID; use openvm_instructions::program::Program; use openvm_native_compiler::{ + prelude::*, conversion::CompilerOptions, - ir::{Array, Builder, Config, DIGEST_SIZE, Felt, RVar}, - prelude::Var, + ir::{Array, Builder, Config, DIGEST_SIZE, Felt, RVar, Usize}, }; use openvm_native_recursion::{ challenger::duplex::DuplexChallengerVariable, fri::TwoAdicFriPcsVariable, stark::StarkVerifier, @@ -29,8 +30,10 @@ use openvm_continuations::verifier::{ }; use openvm_native_recursion::hints::Hintable; use openvm_continuations::verifier::internal::vars::InternalVmVerifierInputVariable; -use crate::aggregation::InternalVmVerifierInput; +use crate::{aggregation::InternalVmVerifierInput, arithmetics::_print_ext_arr, zkvm_verifier::verifier::add_septic_points_in_place}; use crate::aggregation::types::{InternalVmVerifierPvs, InternalVmVerifierExtraPvs, VmVerifierPvs}; +use crate::zkvm_verifier::binding::SepticPointVariable; +use crate::zkvm_verifier::binding::SepticExtensionVariable; use openvm_continuations::{C, F}; use openvm_native_recursion::types::new_from_inner_multi_vk; @@ -90,6 +93,16 @@ impl NonLeafVerifierVariables { let pvs = VmVerifierPvs::>::uninit(builder); let leaf_verifier_commit = array::from_fn(|_| builder.uninit()); + let ec_sum = SepticPointVariable { + x: SepticExtensionVariable { + vs: builder.dyn_array(7), + }, + y: SepticExtensionVariable { + vs: builder.dyn_array(7), + }, + is_infinity: Usize::uninit(builder), + }; + builder.range(0, proofs.len()).for_each(|i_vec, builder| { let i = i_vec[0]; let proof = builder.get(proofs, i); @@ -98,10 +111,23 @@ impl NonLeafVerifierVariables { assert_single_segment_vm_exit_successfully(builder, &proof); + let zero_f: Felt = builder.constant(C::F::ZERO); builder.if_eq(i, RVar::zero()).then_or_else( |builder| { // _debug // builder.assign(&pvs.app_commit, proof_vm_pvs.vm_verifier_pvs.app_commit); + + for i in 0..SEPTIC_EXTENSION_DEGREE { + let x = Ext::uninit(builder); + builder.assign(&x, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.x[i]); + let y = Ext::uninit(builder); + builder.assign(&y, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.y[i]); + + builder.set(&ec_sum.x.vs, i, x); + builder.set(&ec_sum.y.vs, i, y); + } + let inf = Usize::Var(builder.cast_felt_to_var(proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.is_infinity)); + builder.assign(&ec_sum.is_infinity, inf); builder.assign( &leaf_verifier_commit, @@ -114,13 +140,36 @@ impl NonLeafVerifierVariables { // pvs.app_commit, // proof_vm_pvs.vm_verifier_pvs.app_commit, // ); - + + let right = SepticPointVariable { + x: SepticExtensionVariable { + vs: builder.dyn_array(7), + }, + y: SepticExtensionVariable { + vs: builder.dyn_array(7), + }, + is_infinity: Usize::uninit(builder), + }; + for i in 0..SEPTIC_EXTENSION_DEGREE { + let x = Ext::uninit(builder); + builder.assign(&x, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.x[i]); + let y = Ext::uninit(builder); + builder.assign(&y, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.y[i]); + + builder.set(&right.x.vs, i, x); + builder.set(&right.y.vs, i, y); + } + let inf = Usize::Var(builder.cast_felt_to_var(proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.is_infinity)); + builder.assign(&right.is_infinity, inf); + add_septic_points_in_place(builder, &ec_sum, &right); + builder.assert_eq::<[_; DIGEST_SIZE]>( leaf_verifier_commit, proof_vm_pvs.extra_pvs.leaf_verifier_commit, ); }, ); + assert_or_assign_connector_pvs( builder, &pvs.connector, @@ -128,72 +177,12 @@ impl NonLeafVerifierVariables { &proof_vm_pvs.vm_verifier_pvs.connector, ); - // TODO: sum shard ram ec point in each proof - // // EC sum verification - // let expected_last_shard_id = Usize::uninit(builder); - // builder.assign(&expected_last_shard_id, pv.len() - Usize::from(1)); - - // let shard_id_fs = builder.get(&shard_raw_pi, SHARD_ID_IDX); - // let shard_id_f = builder.get(&shard_id_fs, 0); - // let shard_id = Usize::Var(builder.cast_felt_to_var(shard_id_f)); - // builder.assert_usize_eq(expected_last_shard_id, shard_id); - - // let ec_sum = SepticPointVariable { - // x: SepticExtensionVariable { - // vs: builder.dyn_array(7), - // }, - // y: SepticExtensionVariable { - // vs: builder.dyn_array(7), - // }, - // is_infinity: Usize::uninit(builder), - // }; - // builder.assign(&ec_sum.is_infinity, Usize::from(1)); - - // builder.range(0, pv.len()).for_each(|idx_vec, builder| { - // let shard_pv = builder.get(&pv, idx_vec[0]); - // let x = SepticExtensionVariable { - // vs: shard_pv.slice( - // builder, - // SHARD_RW_SUM_IDX, - // SHARD_RW_SUM_IDX + SEPTIC_EXTENSION_DEGREE, - // ), - // }; - // let y = SepticExtensionVariable { - // vs: shard_pv.slice( - // builder, - // SHARD_RW_SUM_IDX + SEPTIC_EXTENSION_DEGREE, - // SHARD_RW_SUM_IDX + 2 * SEPTIC_EXTENSION_DEGREE, - // ), - // }; - // let shard_ec = SepticPointVariable { - // x: x.clone(), - // y: y.clone(), - // is_infinity: Usize::uninit(builder), - // }; - // let is_x_zero = x.is_zero(builder); - // let is_y_zero = y.is_zero(builder); - // builder.if_eq(is_x_zero, Usize::from(1)).then_or_else( - // |builder| { - // builder - // .if_eq(is_y_zero.clone(), Usize::from(1)) - // .then_or_else( - // |builder| { - // builder.assign(&shard_ec.is_infinity, Usize::from(1)); - // }, - // |builder| { - // builder.assign(&shard_ec.is_infinity, Usize::from(0)); - // }, - // ); - // }, - // |builder| { - // builder.assign(&shard_ec.is_infinity, Usize::from(0)); - // }, - // ); + // _debug + builder.print_debug(606); + _print_ext_arr(builder, &ec_sum.x.vs); + _print_ext_arr(builder, &ec_sum.y.vs); - // add_septic_points_in_place(builder, &ec_sum, &shard_ec); - // }); - // add_septic_points_in_place(builder, &ec_sum, &calculated_shard_ec_sum); // This is only needed when `is_terminate` but branching here won't save much, so we // always assign it. From 86273135db8a467d6c26011ee885b5d70ac19669 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 14 Dec 2025 19:44:40 -0500 Subject: [PATCH 05/12] calculate ec --- ceno_recursion/src/aggregation/internal.rs | 31 +++++++++++----------- ceno_recursion/src/aggregation/root.rs | 15 ++++++++++- 2 files changed, 29 insertions(+), 17 deletions(-) diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index 47ebd10a1..a45c87204 100644 --- a/ceno_recursion/src/aggregation/internal.rs +++ b/ceno_recursion/src/aggregation/internal.rs @@ -110,13 +110,8 @@ impl NonLeafVerifierVariables { let proof_vm_pvs = self.verify_internal_or_leaf_verifier_proof(builder, &proof); assert_single_segment_vm_exit_successfully(builder, &proof); - - let zero_f: Felt = builder.constant(C::F::ZERO); builder.if_eq(i, RVar::zero()).then_or_else( |builder| { - // _debug - // builder.assign(&pvs.app_commit, proof_vm_pvs.vm_verifier_pvs.app_commit); - for i in 0..SEPTIC_EXTENSION_DEGREE { let x = Ext::uninit(builder); builder.assign(&x, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.x[i]); @@ -135,12 +130,6 @@ impl NonLeafVerifierVariables { ); }, |builder| { - // _debug - // builder.assert_eq::<[_; DIGEST_SIZE]>( - // pvs.app_commit, - // proof_vm_pvs.vm_verifier_pvs.app_commit, - // ); - let right = SepticPointVariable { x: SepticExtensionVariable { vs: builder.dyn_array(7), @@ -177,12 +166,22 @@ impl NonLeafVerifierVariables { &proof_vm_pvs.vm_verifier_pvs.connector, ); - // _debug - builder.print_debug(606); - _print_ext_arr(builder, &ec_sum.x.vs); - _print_ext_arr(builder, &ec_sum.y.vs); - + for i in 0..SEPTIC_EXTENSION_DEGREE { + let x_ext = builder.get(&ec_sum.x.vs, i); + let y_ext = builder.get(&ec_sum.y.vs, i); + let x_fs = builder.ext2felt(x_ext); + let y_fs = builder.ext2felt(y_ext); + let x = builder.get(&x_fs, 0); + let y = builder.get(&y_fs, 0); + builder.assign(&pvs.shard_ram_connector.x[i], x); + builder.assign(&pvs.shard_ram_connector.y[i], y); + } + builder.if_eq(ec_sum.is_infinity.clone(), Usize::from(1)).then_or_else(|builder| { + builder.assign(&pvs.shard_ram_connector.is_infinity, C::F::ONE); + }, |builder| { + builder.assign(&pvs.shard_ram_connector.is_infinity, C::F::ZERO); + }); // This is only needed when `is_terminate` but branching here won't save much, so we // always assign it. diff --git a/ceno_recursion/src/aggregation/root.rs b/ceno_recursion/src/aggregation/root.rs index ddc0e9b1c..6e10a3a4e 100644 --- a/ceno_recursion/src/aggregation/root.rs +++ b/ceno_recursion/src/aggregation/root.rs @@ -5,6 +5,7 @@ // builder.assert_usize_eq(is_sum_x_zero, Usize::from(1)); // builder.assert_usize_eq(is_sum_y_zero, Usize::from(1)); +use ceno_zkvm::scheme::constants::SEPTIC_EXTENSION_DEGREE; use openvm_continuations::{C, F, SC}; use openvm_instructions::program::Program; use openvm_native_compiler::{ @@ -27,6 +28,7 @@ use openvm_stark_sdk::openvm_stark_backend::{ proof::Proof, }; use serde::{Deserialize, Serialize}; +use p3::field::FieldAlgebra; #[derive(Serialize, Deserialize)] pub struct CenoRootVmVerifierInput { @@ -121,10 +123,21 @@ impl CenoRootVmVerifierConfig { internal_pcs, internal_advice, }; - let (_merged_pvs, _expected_leaf_commit) = + let (merged_pvs, _expected_leaf_commit) = non_leaf_verifier.verify_internal_or_leaf_verifier_proofs(&mut builder, &proofs); builder.cycle_tracker_end("VerifyProofs"); + // Assert final ec sum is zero + /* _debug + let one: Felt<_> = builder.constant(::F::ZERO); + for i in 0..SEPTIC_EXTENSION_DEGREE { + builder.assert_felt_eq(merged_pvs.shard_ram_connector.x[i], one); + builder.assert_felt_eq(merged_pvs.shard_ram_connector.y[i], one); + } + builder.assign(&f, ::F::ONE); + builder.assert_felt_eq(merged_pvs.shard_ram_connector.is_infinity, f); + */ + /* _todo: Change merged pv operations, including checking final ec sum is infinity // App Program should terminate builder.assert_felt_eq(merged_pvs.connector.is_terminate, F::ONE); From 8c95931cef795d65d4e38524e7d2f29d4b0ea526 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 14 Dec 2025 19:47:30 -0500 Subject: [PATCH 06/12] fmt clippy --- ceno_recursion/src/aggregation/internal.rs | 45 ++-- ceno_recursion/src/aggregation/mod.rs | 228 ++++++++++----------- ceno_recursion/src/aggregation/root.rs | 11 +- ceno_recursion/src/aggregation/types.rs | 13 +- 4 files changed, 143 insertions(+), 154 deletions(-) diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index a45c87204..1cc87f20f 100644 --- a/ceno_recursion/src/aggregation/internal.rs +++ b/ceno_recursion/src/aggregation/internal.rs @@ -7,9 +7,9 @@ use ceno_zkvm::scheme::constants::SEPTIC_EXTENSION_DEGREE; use openvm_circuit::arch::PUBLIC_VALUES_AIR_ID; use openvm_instructions::program::Program; use openvm_native_compiler::{ - prelude::*, conversion::CompilerOptions, ir::{Array, Builder, Config, DIGEST_SIZE, Felt, RVar, Usize}, + prelude::*, }; use openvm_native_recursion::{ challenger::duplex::DuplexChallengerVariable, fri::TwoAdicFriPcsVariable, stark::StarkVerifier, @@ -22,18 +22,24 @@ use openvm_stark_sdk::{ }; use p3::field::FieldAlgebra; +use crate::{ + aggregation::{ + InternalVmVerifierInput, + types::{InternalVmVerifierExtraPvs, InternalVmVerifierPvs, VmVerifierPvs}, + }, + zkvm_verifier::{ + binding::{SepticExtensionVariable, SepticPointVariable}, + verifier::add_septic_points_in_place, + }, +}; use openvm_continuations::verifier::{ common::{ assert_or_assign_connector_pvs, assert_required_air_for_agg_vm_present, assert_single_segment_vm_exit_successfully, get_program_commit, }, + internal::vars::InternalVmVerifierInputVariable, }; use openvm_native_recursion::hints::Hintable; -use openvm_continuations::verifier::internal::vars::InternalVmVerifierInputVariable; -use crate::{aggregation::InternalVmVerifierInput, arithmetics::_print_ext_arr, zkvm_verifier::verifier::add_septic_points_in_place}; -use crate::aggregation::types::{InternalVmVerifierPvs, InternalVmVerifierExtraPvs, VmVerifierPvs}; -use crate::zkvm_verifier::binding::SepticPointVariable; -use crate::zkvm_verifier::binding::SepticExtensionVariable; use openvm_continuations::{C, F}; use openvm_native_recursion::types::new_from_inner_multi_vk; @@ -121,7 +127,9 @@ impl NonLeafVerifierVariables { builder.set(&ec_sum.x.vs, i, x); builder.set(&ec_sum.y.vs, i, y); } - let inf = Usize::Var(builder.cast_felt_to_var(proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.is_infinity)); + let inf = Usize::Var(builder.cast_felt_to_var( + proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.is_infinity, + )); builder.assign(&ec_sum.is_infinity, inf); builder.assign( @@ -144,11 +152,13 @@ impl NonLeafVerifierVariables { builder.assign(&x, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.x[i]); let y = Ext::uninit(builder); builder.assign(&y, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.y[i]); - + builder.set(&right.x.vs, i, x); builder.set(&right.y.vs, i, y); } - let inf = Usize::Var(builder.cast_felt_to_var(proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.is_infinity)); + let inf = Usize::Var(builder.cast_felt_to_var( + proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.is_infinity, + )); builder.assign(&right.is_infinity, inf); add_septic_points_in_place(builder, &ec_sum, &right); @@ -177,11 +187,16 @@ impl NonLeafVerifierVariables { builder.assign(&pvs.shard_ram_connector.x[i], x); builder.assign(&pvs.shard_ram_connector.y[i], y); } - builder.if_eq(ec_sum.is_infinity.clone(), Usize::from(1)).then_or_else(|builder| { - builder.assign(&pvs.shard_ram_connector.is_infinity, C::F::ONE); - }, |builder| { - builder.assign(&pvs.shard_ram_connector.is_infinity, C::F::ZERO); - }); + builder + .if_eq(ec_sum.is_infinity.clone(), Usize::from(1)) + .then_or_else( + |builder| { + builder.assign(&pvs.shard_ram_connector.is_infinity, C::F::ONE); + }, + |builder| { + builder.assign(&pvs.shard_ram_connector.is_infinity, C::F::ZERO); + }, + ); // This is only needed when `is_terminate` but branching here won't save much, so we // always assign it. @@ -292,7 +307,7 @@ impl InternalVmVerifierConfig { internal_pcs, internal_advice, }; - + builder.cycle_tracker_start("VerifyProofs"); let (vm_verifier_pvs, leaf_verifier_commit) = non_leaf_verifier.verify_internal_or_leaf_verifier_proofs(&mut builder, &proofs); diff --git a/ceno_recursion/src/aggregation/mod.rs b/ceno_recursion/src/aggregation/mod.rs index 43d681451..b11e65b72 100644 --- a/ceno_recursion/src/aggregation/mod.rs +++ b/ceno_recursion/src/aggregation/mod.rs @@ -24,10 +24,7 @@ use openvm_stark_backend::config::{PcsProverData, Val}; use internal::InternalVmVerifierConfig; use openvm_continuations::{ C, - verifier::{ - internal::types::{InternalVmVerifierInput, VmStarkProof}, - root::types::RootVmVerifierInput, - }, + verifier::{internal::types::InternalVmVerifierInput, root::types::RootVmVerifierInput}, }; #[cfg(feature = "gpu")] use openvm_cuda_backend::engine::GpuBabyBearPoseidon2Engine as BabyBearPoseidon2Engine; @@ -40,7 +37,6 @@ use openvm_native_compiler::{ use openvm_native_recursion::hints::Hintable; use openvm_sdk::{ SC, - commit::AppExecutionCommit, config::DEFAULT_NUM_CHILDREN_INTERNAL, prover::vm::{new_local_prover, types::VmProvingKey}, }; @@ -57,21 +53,13 @@ use openvm_stark_sdk::{ }, engine::StarkFriEngine, openvm_stark_backend::keygen::types::MultiStarkVerifyingKey, - p3_bn254_fr::Bn254Fr, }; use p3::field::FieldAlgebra; use serde::{Deserialize, Serialize}; -use std::{borrow::Borrow, sync::Arc, time::Instant}; +use std::{sync::Arc, time::Instant}; pub type RecPcs = Basefold; -use openvm_circuit::{ - arch::{ - CONNECTOR_AIR_ID, PROGRAM_AIR_ID, PROGRAM_CACHED_TRACE_INDEX, PUBLIC_VALUES_AIR_ID, - SingleSegmentVmProver, - hasher::{Hasher, poseidon2::vm_poseidon2_hasher}, - instructions::exe::VmExe, - }, - system::{memory::CHUNK, program::trace::compute_exe_commit}, -}; +use crate::aggregation::types::{InternalVmVerifierPvs, VmVerifierPvs}; +use openvm_circuit::arch::{PUBLIC_VALUES_AIR_ID, SingleSegmentVmProver, instructions::exe::VmExe}; use openvm_continuations::RootSC; use openvm_native_compiler::{ asm::AsmConfig, @@ -80,7 +68,6 @@ use openvm_native_compiler::{ use openvm_sdk::util::check_max_constraint_degrees; use openvm_stark_backend::proof::Proof; use openvm_stark_sdk::config::baby_bear_poseidon2_root::BabyBearPoseidon2RootEngine; -use crate::aggregation::types::{VmVerifierPvs, InternalVmVerifierPvs}; mod internal; mod root; @@ -480,11 +467,16 @@ impl CenoLeafVmVerifierConfig { builder.assign(&stark_pvs.shard_ram_connector.x[i], x); builder.assign(&stark_pvs.shard_ram_connector.y[i], y); } - builder.if_eq(shard_ec_sum.is_infinity, Usize::from(1)).then_or_else(|builder| { - builder.assign(&stark_pvs.shard_ram_connector.is_infinity, F::ONE); - }, |builder| { - builder.assign(&stark_pvs.shard_ram_connector.is_infinity, F::ZERO); - }); + builder + .if_eq(shard_ec_sum.is_infinity, Usize::from(1)) + .then_or_else( + |builder| { + builder.assign(&stark_pvs.shard_ram_connector.is_infinity, F::ONE); + }, + |builder| { + builder.assign(&stark_pvs.shard_ram_connector.is_infinity, F::ZERO); + }, + ); // builder // .if_eq(ceno_leaf_input.is_last, Usize::from(1)) @@ -619,105 +611,103 @@ pub(crate) fn chunk_ceno_leaf_proof_inputs( ret } -/* // Source from OpenVm SDK::verify_e2e_stark_proof with abridged key // See: https://github.com/openvm-org/openvm -pub fn verify_e2e_stark_proof( - k: &CenoRecursionVerifierKeys, - proof: &VmStarkProof, - _expected_exe_commit: &Bn254Fr, - _expected_vm_commit: &Bn254Fr, -) -> Result { - if proof.inner.per_air.len() < 3 { - return Err("Invalid number of AIRs: expected at least 3".into()); - } else if proof.inner.per_air[0].air_id != PROGRAM_AIR_ID { - return Err("Missing program AIR".into()); - } else if proof.inner.per_air[1].air_id != CONNECTOR_AIR_ID { - return Err("Missing connector AIR".into()); - } else if proof.inner.per_air[2].air_id != PUBLIC_VALUES_AIR_ID { - return Err("Missing public values AIR".into()); - } - let public_values_air_proof_data = &proof.inner.per_air[2]; - - let program_commit = proof.inner.commitments.main_trace[PROGRAM_CACHED_TRACE_INDEX].as_ref(); - let internal_commit: &[_; CHUNK] = &k.internal_commit.into(); - - let (vm_vk, fri_params, vm_commit) = if program_commit == internal_commit { - let internal_pvs: &InternalVmVerifierPvs<_> = public_values_air_proof_data - .public_values - .as_slice() - .borrow(); - if internal_commit != &internal_pvs.extra_pvs.internal_program_commit { - return Err(format!( - "Invalid internal program commit: expected {:?}, got {:?}", - internal_commit, internal_pvs.extra_pvs.internal_program_commit - )); - } - ( - &k.internal_vm_vk, - k.internal_fri_params, - internal_pvs.extra_pvs.leaf_verifier_commit, - ) - } else { - (&k.leaf_vm_vk, k.leaf_fri_params, *program_commit) - }; - let e = BabyBearPoseidon2Engine::new(fri_params); - e.verify(vm_vk, &proof.inner) - .expect("stark e2e proof verification should pass"); - - let pvs: &VmVerifierPvs<_> = - public_values_air_proof_data.public_values[..VmVerifierPvs::::width()].borrow(); - - // _debug: AIR ordering - // if let Some(exit_code) = pvs.connector.exit_code() { - // if exit_code != 0 { - // return Err(format!( - // "Invalid exit code: expected 0, got {}", - // exit_code - // )); - // } - // } else { - // return Err(format!("Program did not terminate")); - // } - - let hasher = vm_poseidon2_hasher(); - let _public_values_root = hasher.merkle_root(&proof.user_public_values); - // _debug: Public value commitment - // if public_values_root != pvs.public_values_commit { - // return Err(format!( - // "Invalid public values root: expected {:?}, got {:?}", - // pvs.public_values_commit, - // public_values_root - // )); - // } - - let exe_commit = compute_exe_commit( - &hasher, - &pvs.app_commit, - &pvs.memory.initial_root, - pvs.connector.initial_pc, - ); - let app_commit = AppExecutionCommit::from_field_commit(exe_commit, vm_commit); - let _exe_commit_bn254 = app_commit.app_exe_commit.to_bn254(); - let _vm_commit_bn254 = app_commit.app_vm_commit.to_bn254(); - - // _debug: execution commit checks - // if exe_commit_bn254 != *expected_exe_commit { - // return Err(eyre::eyre!( - // "Invalid app exe commit: expected {:?}, got {:?}", - // expected_exe_commit, - // exe_commit_bn254 - // )); - // } else if vm_commit_bn254 != *expected_vm_commit { - // return Err(eyre::eyre!( - // "Invalid app vm commit: expected {:?}, got {:?}", - // expected_vm_commit, - // vm_commit_bn254 - // )); - // } - Ok(app_commit) -} -*/ +// pub fn verify_e2e_stark_proof( +// k: &CenoRecursionVerifierKeys, +// proof: &VmStarkProof, +// _expected_exe_commit: &Bn254Fr, +// _expected_vm_commit: &Bn254Fr, +// ) -> Result { +// if proof.inner.per_air.len() < 3 { +// return Err("Invalid number of AIRs: expected at least 3".into()); +// } else if proof.inner.per_air[0].air_id != PROGRAM_AIR_ID { +// return Err("Missing program AIR".into()); +// } else if proof.inner.per_air[1].air_id != CONNECTOR_AIR_ID { +// return Err("Missing connector AIR".into()); +// } else if proof.inner.per_air[2].air_id != PUBLIC_VALUES_AIR_ID { +// return Err("Missing public values AIR".into()); +// } +// let public_values_air_proof_data = &proof.inner.per_air[2]; +// +// let program_commit = proof.inner.commitments.main_trace[PROGRAM_CACHED_TRACE_INDEX].as_ref(); +// let internal_commit: &[_; CHUNK] = &k.internal_commit.into(); +// +// let (vm_vk, fri_params, vm_commit) = if program_commit == internal_commit { +// let internal_pvs: &InternalVmVerifierPvs<_> = public_values_air_proof_data +// .public_values +// .as_slice() +// .borrow(); +// if internal_commit != &internal_pvs.extra_pvs.internal_program_commit { +// return Err(format!( +// "Invalid internal program commit: expected {:?}, got {:?}", +// internal_commit, internal_pvs.extra_pvs.internal_program_commit +// )); +// } +// ( +// &k.internal_vm_vk, +// k.internal_fri_params, +// internal_pvs.extra_pvs.leaf_verifier_commit, +// ) +// } else { +// (&k.leaf_vm_vk, k.leaf_fri_params, *program_commit) +// }; +// let e = BabyBearPoseidon2Engine::new(fri_params); +// e.verify(vm_vk, &proof.inner) +// .expect("stark e2e proof verification should pass"); +// +// let pvs: &VmVerifierPvs<_> = +// public_values_air_proof_data.public_values[..VmVerifierPvs::::width()].borrow(); +// +// _debug: AIR ordering +// if let Some(exit_code) = pvs.connector.exit_code() { +// if exit_code != 0 { +// return Err(format!( +// "Invalid exit code: expected 0, got {}", +// exit_code +// )); +// } +// } else { +// return Err(format!("Program did not terminate")); +// } +// +// let hasher = vm_poseidon2_hasher(); +// let _public_values_root = hasher.merkle_root(&proof.user_public_values); +// _debug: Public value commitment +// if public_values_root != pvs.public_values_commit { +// return Err(format!( +// "Invalid public values root: expected {:?}, got {:?}", +// pvs.public_values_commit, +// public_values_root +// )); +// } +// +// let exe_commit = compute_exe_commit( +// &hasher, +// &pvs.app_commit, +// &pvs.memory.initial_root, +// pvs.connector.initial_pc, +// ); +// let app_commit = AppExecutionCommit::from_field_commit(exe_commit, vm_commit); +// let _exe_commit_bn254 = app_commit.app_exe_commit.to_bn254(); +// let _vm_commit_bn254 = app_commit.app_vm_commit.to_bn254(); +// +// _debug: execution commit checks +// if exe_commit_bn254 != *expected_exe_commit { +// return Err(eyre::eyre!( +// "Invalid app exe commit: expected {:?}, got {:?}", +// expected_exe_commit, +// exe_commit_bn254 +// )); +// } else if vm_commit_bn254 != *expected_vm_commit { +// return Err(eyre::eyre!( +// "Invalid app vm commit: expected {:?}, got {:?}", +// expected_vm_commit, +// vm_commit_bn254 +// )); +// } +// Ok(app_commit) +// } /// Build Ceno's zkVM verifier program from vk in OpenVM's eDSL pub fn build_zkvm_verifier_program( diff --git a/ceno_recursion/src/aggregation/root.rs b/ceno_recursion/src/aggregation/root.rs index 6e10a3a4e..6e6615022 100644 --- a/ceno_recursion/src/aggregation/root.rs +++ b/ceno_recursion/src/aggregation/root.rs @@ -1,11 +1,3 @@ -// TODO: assert that the shard ram ec point is `PointAtInfinity` - -// let is_sum_x_zero = ec_sum.x.is_zero(builder); -// let is_sum_y_zero = ec_sum.y.is_zero(builder); -// builder.assert_usize_eq(is_sum_x_zero, Usize::from(1)); -// builder.assert_usize_eq(is_sum_y_zero, Usize::from(1)); - -use ceno_zkvm::scheme::constants::SEPTIC_EXTENSION_DEGREE; use openvm_continuations::{C, F, SC}; use openvm_instructions::program::Program; use openvm_native_compiler::{ @@ -28,7 +20,6 @@ use openvm_stark_sdk::openvm_stark_backend::{ proof::Proof, }; use serde::{Deserialize, Serialize}; -use p3::field::FieldAlgebra; #[derive(Serialize, Deserialize)] pub struct CenoRootVmVerifierInput { @@ -123,7 +114,7 @@ impl CenoRootVmVerifierConfig { internal_pcs, internal_advice, }; - let (merged_pvs, _expected_leaf_commit) = + let (_merged_pvs, _expected_leaf_commit) = non_leaf_verifier.verify_internal_or_leaf_verifier_proofs(&mut builder, &proofs); builder.cycle_tracker_end("VerifyProofs"); diff --git a/ceno_recursion/src/aggregation/types.rs b/ceno_recursion/src/aggregation/types.rs index dd633b824..cf244aec2 100644 --- a/ceno_recursion/src/aggregation/types.rs +++ b/ceno_recursion/src/aggregation/types.rs @@ -1,15 +1,8 @@ - -use openvm_continuations::F; -use ceno_zkvm::scheme::{constants::SEPTIC_EXTENSION_DEGREE, septic_curve::SepticPoint}; +use ceno_zkvm::scheme::constants::SEPTIC_EXTENSION_DEGREE; use openvm_circuit::{circuit_derive::AlignedBorrow, system::connector::VmConnectorPvs}; +use openvm_native_compiler::ir::{Builder, Config, DIGEST_SIZE, Felt, Variable}; use p3::field::PrimeField32; -use crate::zkvm_verifier::binding::{SepticPointVariable, SepticExtensionVariable}; -use openvm_native_compiler::{ - prelude::*, - ir::{Array, Builder, Config, DIGEST_SIZE, Felt, Variable}, -}; -use std::array; -use std::borrow::BorrowMut; +use std::{array, borrow::BorrowMut}; #[derive(Clone, Copy, AlignedBorrow)] pub struct ContinuationPvs { From 9daf4976721f6f50db1000a3f4608553cfd9e4ef Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 14 Dec 2025 20:18:15 -0500 Subject: [PATCH 07/12] remove test --- ceno_recursion/src/aggregation/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_recursion/src/aggregation/mod.rs b/ceno_recursion/src/aggregation/mod.rs index b11e65b72..dd9704601 100644 --- a/ceno_recursion/src/aggregation/mod.rs +++ b/ceno_recursion/src/aggregation/mod.rs @@ -843,7 +843,7 @@ mod tests { } #[test] - // #[ignore = "need to generate proof first"] + #[ignore = "need to generate proof first"] pub fn test_aggregation() { let stack_size = 256 * 1024 * 1024; // 64 MB From 02ff8b2435b04f65b740cdcf28bca2e3550d856c Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Sun, 14 Dec 2025 20:45:26 -0500 Subject: [PATCH 08/12] local debug flags: --- ceno_recursion/src/aggregation/internal.rs | 26 +++++++++++++++++--- ceno_recursion/src/aggregation/mod.rs | 2 +- ceno_recursion/src/zkvm_verifier/verifier.rs | 10 ++++++-- 3 files changed, 32 insertions(+), 6 deletions(-) diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index 1cc87f20f..444cfe3e8 100644 --- a/ceno_recursion/src/aggregation/internal.rs +++ b/ceno_recursion/src/aggregation/internal.rs @@ -26,11 +26,10 @@ use crate::{ aggregation::{ InternalVmVerifierInput, types::{InternalVmVerifierExtraPvs, InternalVmVerifierPvs, VmVerifierPvs}, - }, - zkvm_verifier::{ + }, arithmetics::_print_ext_arr, zkvm_verifier::{ binding::{SepticExtensionVariable, SepticPointVariable}, verifier::add_septic_points_in_place, - }, + } }; use openvm_continuations::verifier::{ common::{ @@ -136,6 +135,13 @@ impl NonLeafVerifierVariables { &leaf_verifier_commit, proof_vm_pvs.extra_pvs.leaf_verifier_commit, ); + + + // _debug + builder.print_debug(101); + _print_ext_arr(builder, &ec_sum.x.vs); + _print_ext_arr(builder, &ec_sum.y.vs); + }, |builder| { let right = SepticPointVariable { @@ -147,6 +153,7 @@ impl NonLeafVerifierVariables { }, is_infinity: Usize::uninit(builder), }; + for i in 0..SEPTIC_EXTENSION_DEGREE { let x = Ext::uninit(builder); builder.assign(&x, proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.x[i]); @@ -160,8 +167,21 @@ impl NonLeafVerifierVariables { proof_vm_pvs.vm_verifier_pvs.shard_ram_connector.is_infinity, )); builder.assign(&right.is_infinity, inf); + + // _debug + builder.print_debug(102); + _print_ext_arr(builder, &right.x.vs); + _print_ext_arr(builder, &right.y.vs); + + add_septic_points_in_place(builder, &ec_sum, &right); + // _debug + builder.print_debug(103); + _print_ext_arr(builder, &ec_sum.x.vs); + _print_ext_arr(builder, &ec_sum.y.vs); + + builder.assert_eq::<[_; DIGEST_SIZE]>( leaf_verifier_commit, proof_vm_pvs.extra_pvs.leaf_verifier_commit, diff --git a/ceno_recursion/src/aggregation/mod.rs b/ceno_recursion/src/aggregation/mod.rs index dd9704601..b11e65b72 100644 --- a/ceno_recursion/src/aggregation/mod.rs +++ b/ceno_recursion/src/aggregation/mod.rs @@ -843,7 +843,7 @@ mod tests { } #[test] - #[ignore = "need to generate proof first"] + // #[ignore = "need to generate proof first"] pub fn test_aggregation() { let stack_size = 256 * 1024 * 1024; // 64 MB diff --git a/ceno_recursion/src/zkvm_verifier/verifier.rs b/ceno_recursion/src/zkvm_verifier/verifier.rs index 248447e4f..33bd1ad2d 100644 --- a/ceno_recursion/src/zkvm_verifier/verifier.rs +++ b/ceno_recursion/src/zkvm_verifier/verifier.rs @@ -4,8 +4,7 @@ use super::binding::{ }; use crate::{ arithmetics::{ - PolyEvaluator, UniPolyExtrapolator, assert_ext_arr_eq, challenger_multi_observe, eq_eval, - eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse, + _print_ext_arr, PolyEvaluator, UniPolyExtrapolator, assert_ext_arr_eq, challenger_multi_observe, eq_eval, eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse }, basefold_verifier::{ basefold::{BasefoldCommitmentVariable, RoundOpeningVariable, RoundVariable}, @@ -499,6 +498,13 @@ pub fn verify_zkvm_proof>( let zero: Ext = builder.constant(C::EF::ZERO); builder.assert_ext_eq(logup_sum, zero); + + // _debug + builder.print_debug(99); + _print_ext_arr(builder, &shard_ec_sum.x.vs); + _print_ext_arr(builder, &shard_ec_sum.y.vs); + + shard_ec_sum } From 715d799b9e2932dd868dc4dc70d0319a8a55982e Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Mon, 15 Dec 2025 17:52:22 -0500 Subject: [PATCH 09/12] correct ec sum --- ceno_recursion/src/aggregation/internal.rs | 21 +------- ceno_recursion/src/zkvm_verifier/binding.rs | 23 ++++++++- ceno_recursion/src/zkvm_verifier/verifier.rs | 50 +++++++------------- ceno_zkvm/src/scheme/septic_curve.rs | 1 - ceno_zkvm/src/scheme/verifier.rs | 6 --- 5 files changed, 39 insertions(+), 62 deletions(-) diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index 444cfe3e8..4d885819e 100644 --- a/ceno_recursion/src/aggregation/internal.rs +++ b/ceno_recursion/src/aggregation/internal.rs @@ -26,7 +26,7 @@ use crate::{ aggregation::{ InternalVmVerifierInput, types::{InternalVmVerifierExtraPvs, InternalVmVerifierPvs, VmVerifierPvs}, - }, arithmetics::_print_ext_arr, zkvm_verifier::{ + }, zkvm_verifier::{ binding::{SepticExtensionVariable, SepticPointVariable}, verifier::add_septic_points_in_place, } @@ -135,13 +135,6 @@ impl NonLeafVerifierVariables { &leaf_verifier_commit, proof_vm_pvs.extra_pvs.leaf_verifier_commit, ); - - - // _debug - builder.print_debug(101); - _print_ext_arr(builder, &ec_sum.x.vs); - _print_ext_arr(builder, &ec_sum.y.vs); - }, |builder| { let right = SepticPointVariable { @@ -168,20 +161,8 @@ impl NonLeafVerifierVariables { )); builder.assign(&right.is_infinity, inf); - // _debug - builder.print_debug(102); - _print_ext_arr(builder, &right.x.vs); - _print_ext_arr(builder, &right.y.vs); - - add_septic_points_in_place(builder, &ec_sum, &right); - // _debug - builder.print_debug(103); - _print_ext_arr(builder, &ec_sum.x.vs); - _print_ext_arr(builder, &ec_sum.y.vs); - - builder.assert_eq::<[_; DIGEST_SIZE]>( leaf_verifier_commit, proof_vm_pvs.extra_pvs.leaf_verifier_commit, diff --git a/ceno_recursion/src/zkvm_verifier/binding.rs b/ceno_recursion/src/zkvm_verifier/binding.rs index fe12ca613..c74c8af8b 100644 --- a/ceno_recursion/src/zkvm_verifier/binding.rs +++ b/ceno_recursion/src/zkvm_verifier/binding.rs @@ -9,7 +9,7 @@ use crate::{ }, }; use ceno_zkvm::{ - scheme::{ZKVMChipProof, ZKVMProof}, + scheme::{ZKVMChipProof, ZKVMProof, constants::SEPTIC_EXTENSION_DEGREE}, structs::{EccQuarkProof, TowerProofs}, }; use gkr_iop::gkr::{GKRProof, layer::sumcheck_layer::LayerProof}; @@ -755,6 +755,27 @@ pub struct SepticPointVariable { pub is_infinity: Usize, } +impl SepticPointVariable { + pub fn zero(builder: &mut Builder) -> Self { + let r = SepticPointVariable { + x: SepticExtensionVariable { + vs: builder.dyn_array(7), + }, + y: SepticExtensionVariable { + vs: builder.dyn_array(7), + }, + is_infinity: Usize::uninit(builder), + }; + let z: Ext = builder.constant(C::EF::ZERO); + for i in 0..SEPTIC_EXTENSION_DEGREE { + builder.set(&r.x.vs, i, z); + builder.set(&r.y.vs, i, z); + } + builder.assign(&r.is_infinity, Usize::from(1)); + r + } +} + pub struct EccQuarkProofInput { pub zerocheck_proof: IOPProof, pub num_instances: usize, diff --git a/ceno_recursion/src/zkvm_verifier/verifier.rs b/ceno_recursion/src/zkvm_verifier/verifier.rs index 33bd1ad2d..0f911b58c 100644 --- a/ceno_recursion/src/zkvm_verifier/verifier.rs +++ b/ceno_recursion/src/zkvm_verifier/verifier.rs @@ -223,15 +223,7 @@ pub fn verify_zkvm_proof>( builder.dyn_array(zkvm_proof_input.chip_proofs.len()); let fixed_openings: Array> = builder.dyn_array(zkvm_proof_input.chip_proofs.len()); - let shard_ec_sum = SepticPointVariable { - x: SepticExtensionVariable { - vs: builder.dyn_array(7), - }, - y: SepticExtensionVariable { - vs: builder.dyn_array(7), - }, - is_infinity: Usize::uninit(builder), - }; + let shard_ec_sum = SepticPointVariable::zero(builder); let num_chips_verified: Usize = builder.eval(C::N::ZERO); let num_chips_have_fixed: Usize = builder.eval(C::N::ZERO); @@ -498,13 +490,6 @@ pub fn verify_zkvm_proof>( let zero: Ext = builder.constant(C::EF::ZERO); builder.assert_ext_eq(logup_sum, zero); - - // _debug - builder.print_debug(99); - _print_ext_arr(builder, &shard_ec_sum.x.vs); - _print_ext_arr(builder, &shard_ec_sum.y.vs); - - shard_ec_sum } @@ -550,17 +535,8 @@ pub fn verify_chip_proof( &num_var_with_rotation, log2_num_instances.clone() + Usize::from(composed_cs.rotation_vars().unwrap_or(0)), ); - - let shard_ec_sum = SepticPointVariable { - x: SepticExtensionVariable { - vs: builder.dyn_array(7), - }, - y: SepticExtensionVariable { - vs: builder.dyn_array(7), - }, - is_infinity: Usize::uninit(builder), - }; - + let shard_ec_sum = SepticPointVariable::zero(builder); + if composed_cs.has_ecc_ops() { builder.assert_nonzero(&chip_proof.has_ecc_proof); let ecc_proof = &chip_proof.ecc_proof; @@ -1880,7 +1856,11 @@ pub fn septic_ext_squared( builder: &mut Builder, a: &SepticExtensionVariable, ) -> SepticExtensionVariable { + let z: Ext = builder.constant(C::EF::ZERO); let r: Array> = builder.dyn_array(SEPTIC_EXTENSION_DEGREE); + for i in 0..SEPTIC_EXTENSION_DEGREE { + builder.set(&r, i, z); + } let two_ext: Ext = builder.constant(C::EF::TWO); let five_ext: Ext = builder.constant(C::EF::from_canonical_u32(5)); @@ -1959,12 +1939,16 @@ pub fn septic_ext_mul( a: &SepticExtensionVariable, b: &SepticExtensionVariable, ) -> SepticExtensionVariable { - let r: Array> = builder.dyn_array(SEPTIC_EXTENSION_DEGREE); + let z: Ext = builder.constant(C::EF::ZERO); + let r: Array> = builder.dyn_array(7); + for i in 0..7 { + builder.set(&r, i, z); + } let two_ext: Ext = builder.constant(C::EF::TWO); let five_ext: Ext = builder.constant(C::EF::from_canonical_u32(5)); - for i in 0..SEPTIC_EXTENSION_DEGREE { - for j in 0..SEPTIC_EXTENSION_DEGREE { + for i in 0..7 { + for j in 0..7 { let mut index = i + j; let a_term = builder.get(&a.vs, i); @@ -2210,10 +2194,8 @@ pub fn add_septic_points_in_place( let y_sum = septic_ext_add(builder, &right.y, &left.y); let is_y_sum_zero = y_sum.is_zero(builder); builder.assert_usize_eq(is_y_sum_zero, Usize::from(1)); - let zero_ext_arr: Array> = - builder.dyn_array(SEPTIC_EXTENSION_DEGREE); - builder.assign(&left.x, zero_ext_arr.clone()); - builder.assign(&left.y, zero_ext_arr.clone()); + builder.assign(&left.x, y_sum.clone()); + builder.assign(&left.y, y_sum.clone()); builder.assign(&left.is_infinity, Usize::from(1)); }, ); diff --git a/ceno_zkvm/src/scheme/septic_curve.rs b/ceno_zkvm/src/scheme/septic_curve.rs index f9b6b4f76..37b30abd8 100644 --- a/ceno_zkvm/src/scheme/septic_curve.rs +++ b/ceno_zkvm/src/scheme/septic_curve.rs @@ -225,7 +225,6 @@ impl SepticExtension { let norm = (self * &x).0[0]; // since self is not zero, norm is not zero let norm_inv = norm.try_inverse().unwrap(); - Some(x * norm_inv) } } diff --git a/ceno_zkvm/src/scheme/verifier.rs b/ceno_zkvm/src/scheme/verifier.rs index fe1f2301d..d3864f0cd 100644 --- a/ceno_zkvm/src/scheme/verifier.rs +++ b/ceno_zkvm/src/scheme/verifier.rs @@ -122,14 +122,8 @@ impl> ZKVMVerifier let end_pc = vm_proof.pi_evals[END_PC_IDX]; // add to shard ec sum - // _debug - // println!("=> shard pi: {:?}", vm_proof.pi_evals.clone()); let shard_ec = self.verify_proof_validity(shard_id, vm_proof, transcript)?; - // println!("=> start_ec_sum: {:?}", shard_ec_sum); - // println!("=> shard_ec: {:?}", shard_ec); - // shard_ec_sum = shard_ec_sum + self.verify_proof_validity(shard_id, vm_proof, transcript)?; shard_ec_sum = shard_ec_sum + shard_ec; - // println!("=> new_ec_sum: {:?}", shard_ec_sum); Ok((Some(end_pc), shard_ec_sum)) })?; From 4c6a82ce1d17b035c51978401abcc34abbbcc3c0 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Mon, 15 Dec 2025 17:52:55 -0500 Subject: [PATCH 10/12] Remove test --- ceno_recursion/src/aggregation/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_recursion/src/aggregation/mod.rs b/ceno_recursion/src/aggregation/mod.rs index b11e65b72..dd9704601 100644 --- a/ceno_recursion/src/aggregation/mod.rs +++ b/ceno_recursion/src/aggregation/mod.rs @@ -843,7 +843,7 @@ mod tests { } #[test] - // #[ignore = "need to generate proof first"] + #[ignore = "need to generate proof first"] pub fn test_aggregation() { let stack_size = 256 * 1024 * 1024; // 64 MB From 74b06d1392a93fbfdf925d9ba32830ad286d980d Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Mon, 15 Dec 2025 17:55:00 -0500 Subject: [PATCH 11/12] fmt clippy [skip ci] --- ceno_recursion/src/aggregation/internal.rs | 5 +++-- ceno_recursion/src/zkvm_verifier/verifier.rs | 6 ++++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index 4d885819e..0d57cdd7b 100644 --- a/ceno_recursion/src/aggregation/internal.rs +++ b/ceno_recursion/src/aggregation/internal.rs @@ -26,10 +26,11 @@ use crate::{ aggregation::{ InternalVmVerifierInput, types::{InternalVmVerifierExtraPvs, InternalVmVerifierPvs, VmVerifierPvs}, - }, zkvm_verifier::{ + }, + zkvm_verifier::{ binding::{SepticExtensionVariable, SepticPointVariable}, verifier::add_septic_points_in_place, - } + }, }; use openvm_continuations::verifier::{ common::{ diff --git a/ceno_recursion/src/zkvm_verifier/verifier.rs b/ceno_recursion/src/zkvm_verifier/verifier.rs index 0f911b58c..fc05eef23 100644 --- a/ceno_recursion/src/zkvm_verifier/verifier.rs +++ b/ceno_recursion/src/zkvm_verifier/verifier.rs @@ -4,7 +4,9 @@ use super::binding::{ }; use crate::{ arithmetics::{ - _print_ext_arr, PolyEvaluator, UniPolyExtrapolator, assert_ext_arr_eq, challenger_multi_observe, eq_eval, eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse + PolyEvaluator, UniPolyExtrapolator, assert_ext_arr_eq, + challenger_multi_observe, eq_eval, eval_ceno_expr_with_instance, eval_wellform_address_vec, + mask_arr, reverse, }, basefold_verifier::{ basefold::{BasefoldCommitmentVariable, RoundOpeningVariable, RoundVariable}, @@ -536,7 +538,7 @@ pub fn verify_chip_proof( log2_num_instances.clone() + Usize::from(composed_cs.rotation_vars().unwrap_or(0)), ); let shard_ec_sum = SepticPointVariable::zero(builder); - + if composed_cs.has_ecc_ops() { builder.assert_nonzero(&chip_proof.has_ecc_proof); let ecc_proof = &chip_proof.ecc_proof; From 441a151e725c70ee809eba69b0ef121334c38bd9 Mon Sep 17 00:00:00 2001 From: Ray Gao Date: Mon, 15 Dec 2025 18:05:01 -0500 Subject: [PATCH 12/12] recover root ec check --- ceno_recursion/src/aggregation/root.rs | 17 ++++++++--------- ceno_recursion/src/zkvm_verifier/verifier.rs | 13 ++++++------- ceno_zkvm/src/scheme/septic_curve.rs | 1 + 3 files changed, 15 insertions(+), 16 deletions(-) diff --git a/ceno_recursion/src/aggregation/root.rs b/ceno_recursion/src/aggregation/root.rs index 6e6615022..5c3596322 100644 --- a/ceno_recursion/src/aggregation/root.rs +++ b/ceno_recursion/src/aggregation/root.rs @@ -12,13 +12,14 @@ use openvm_stark_backend::keygen::types::MultiStarkVerifyingKey; use openvm_stark_sdk::config::FriParameters; use std::array; -use crate::aggregation::internal::NonLeafVerifierVariables; +use crate::aggregation::{SEPTIC_EXTENSION_DEGREE, internal::NonLeafVerifierVariables}; use openvm_native_compiler::prelude::*; use openvm_native_recursion::vars::StarkProofVariable; use openvm_stark_sdk::openvm_stark_backend::{ config::{StarkGenericConfig, Val}, proof::Proof, }; +use p3::field::FieldAlgebra; use serde::{Deserialize, Serialize}; #[derive(Serialize, Deserialize)] @@ -114,20 +115,18 @@ impl CenoRootVmVerifierConfig { internal_pcs, internal_advice, }; - let (_merged_pvs, _expected_leaf_commit) = + let (merged_pvs, _expected_leaf_commit) = non_leaf_verifier.verify_internal_or_leaf_verifier_proofs(&mut builder, &proofs); builder.cycle_tracker_end("VerifyProofs"); // Assert final ec sum is zero - /* _debug - let one: Felt<_> = builder.constant(::F::ZERO); + let z: Felt<_> = builder.constant(::F::ZERO); for i in 0..SEPTIC_EXTENSION_DEGREE { - builder.assert_felt_eq(merged_pvs.shard_ram_connector.x[i], one); - builder.assert_felt_eq(merged_pvs.shard_ram_connector.y[i], one); + builder.assert_felt_eq(merged_pvs.shard_ram_connector.x[i], z); + builder.assert_felt_eq(merged_pvs.shard_ram_connector.y[i], z); } - builder.assign(&f, ::F::ONE); - builder.assert_felt_eq(merged_pvs.shard_ram_connector.is_infinity, f); - */ + let one: Felt<_> = builder.constant(::F::ONE); + builder.assert_felt_eq(merged_pvs.shard_ram_connector.is_infinity, one); /* _todo: Change merged pv operations, including checking final ec sum is infinity // App Program should terminate diff --git a/ceno_recursion/src/zkvm_verifier/verifier.rs b/ceno_recursion/src/zkvm_verifier/verifier.rs index fc05eef23..e289d6a68 100644 --- a/ceno_recursion/src/zkvm_verifier/verifier.rs +++ b/ceno_recursion/src/zkvm_verifier/verifier.rs @@ -4,9 +4,8 @@ use super::binding::{ }; use crate::{ arithmetics::{ - PolyEvaluator, UniPolyExtrapolator, assert_ext_arr_eq, - challenger_multi_observe, eq_eval, eval_ceno_expr_with_instance, eval_wellform_address_vec, - mask_arr, reverse, + PolyEvaluator, UniPolyExtrapolator, assert_ext_arr_eq, challenger_multi_observe, eq_eval, + eval_ceno_expr_with_instance, eval_wellform_address_vec, mask_arr, reverse, }, basefold_verifier::{ basefold::{BasefoldCommitmentVariable, RoundOpeningVariable, RoundVariable}, @@ -1942,15 +1941,15 @@ pub fn septic_ext_mul( b: &SepticExtensionVariable, ) -> SepticExtensionVariable { let z: Ext = builder.constant(C::EF::ZERO); - let r: Array> = builder.dyn_array(7); - for i in 0..7 { + let r: Array> = builder.dyn_array(SEPTIC_EXTENSION_DEGREE); + for i in 0..SEPTIC_EXTENSION_DEGREE { builder.set(&r, i, z); } let two_ext: Ext = builder.constant(C::EF::TWO); let five_ext: Ext = builder.constant(C::EF::from_canonical_u32(5)); - for i in 0..7 { - for j in 0..7 { + for i in 0..SEPTIC_EXTENSION_DEGREE { + for j in 0..SEPTIC_EXTENSION_DEGREE { let mut index = i + j; let a_term = builder.get(&a.vs, i); diff --git a/ceno_zkvm/src/scheme/septic_curve.rs b/ceno_zkvm/src/scheme/septic_curve.rs index 37b30abd8..f9b6b4f76 100644 --- a/ceno_zkvm/src/scheme/septic_curve.rs +++ b/ceno_zkvm/src/scheme/septic_curve.rs @@ -225,6 +225,7 @@ impl SepticExtension { let norm = (self * &x).0[0]; // since self is not zero, norm is not zero let norm_inv = norm.try_inverse().unwrap(); + Some(x * norm_inv) } }