diff --git a/ceno_recursion/src/aggregation/internal.rs b/ceno_recursion/src/aggregation/internal.rs index bd494a0e9..0d57cdd7b 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::{ conversion::CompilerOptions, - ir::{Array, Builder, Config, DIGEST_SIZE, Felt, RVar}, - prelude::Var, + ir::{Array, Builder, Config, DIGEST_SIZE, Felt, RVar, Usize}, + prelude::*, }; use openvm_native_recursion::{ challenger::duplex::DuplexChallengerVariable, fri::TwoAdicFriPcsVariable, stark::StarkVerifier, @@ -21,15 +22,22 @@ 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, types::VmVerifierPvs, - }, - internal::{ - types::{InternalVmVerifierExtraPvs, InternalVmVerifierInput, InternalVmVerifierPvs}, - vars::InternalVmVerifierInputVariable, + assert_single_segment_vm_exit_successfully, get_program_commit, }, + internal::vars::InternalVmVerifierInputVariable, }; use openvm_native_recursion::hints::Hintable; @@ -91,6 +99,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,26 +116,61 @@ impl NonLeafVerifierVariables { let proof_vm_pvs = self.verify_internal_or_leaf_verifier_proof(builder, &proof); assert_single_segment_vm_exit_successfully(builder, &proof); - builder.if_eq(i, RVar::zero()).then_or_else( |builder| { - 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, 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, - ); + 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, @@ -125,72 +178,27 @@ 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); + 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); - // 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)); - // }, - // ); - - // add_septic_points_in_place(builder, &ec_sum, &shard_ec); - // }); - - // add_septic_points_in_place(builder, &ec_sum, &calculated_shard_ec_sum); + 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. @@ -301,6 +309,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 a91235298..f498ab0de 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; @@ -24,11 +24,7 @@ use openvm_stark_backend::config::{PcsProverData, Val}; use internal::InternalVmVerifierConfig; use openvm_continuations::{ C, - verifier::{ - common::types::VmVerifierPvs, - internal::types::{InternalVmVerifierInput, InternalVmVerifierPvs, VmStarkProof}, - root::types::RootVmVerifierInput, - }, + verifier::{internal::types::InternalVmVerifierInput, root::types::RootVmVerifierInput}, }; #[cfg(feature = "gpu")] use openvm_cuda_backend::engine::GpuBabyBearPoseidon2Engine as BabyBearPoseidon2Engine; @@ -41,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}, }; @@ -58,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, @@ -448,16 +435,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 +456,27 @@ 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)) @@ -504,7 +505,6 @@ impl CenoLeafVmVerifierConfig { // ); // builder.assign(&prev_pc, end_pc); // }); - // }); for pv in stark_pvs.flatten() { @@ -613,101 +613,101 @@ pub(crate) fn chunk_ceno_leaf_proof_inputs( // 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 8f7917e23..cc93532cd 100644 --- a/ceno_recursion/src/aggregation/root.rs +++ b/ceno_recursion/src/aggregation/root.rs @@ -1,10 +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 openvm_continuations::{C, F, SC}; use openvm_instructions::program::Program; use openvm_native_compiler::{ @@ -19,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)] @@ -127,6 +121,15 @@ impl CenoRootVmVerifierConfig { non_leaf_verifier.verify_internal_or_leaf_verifier_proofs(&mut builder, &proofs); builder.cycle_tracker_end("VerifyProofs"); + // Assert final ec sum is 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], z); + builder.assert_felt_eq(merged_pvs.shard_ram_connector.y[i], z); + } + 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 builder.assert_felt_eq(merged_pvs.connector.is_terminate, F::ONE); diff --git a/ceno_recursion/src/aggregation/types.rs b/ceno_recursion/src/aggregation/types.rs index be88a6fb8..cf244aec2 100644 --- a/ceno_recursion/src/aggregation/types.rs +++ b/ceno_recursion/src/aggregation/types.rs @@ -1,38 +1,111 @@ -// TODO: enable this -// #[derive(Debug, Clone, AlignedBorrow)] -// pub struct ContinuationPvs { -// pub sum: SepticPoint, -// } - -// impl ContinuationPvs> { -// pub fn uninit(builder: &mut Builder) -> Self { -// todo!() -// } -// } - -// #[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], -// } - -// 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()), -// } -// } -// } +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 std::{array, borrow::BorrowMut}; + +#[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 { + Self { + x: array::from_fn(|_| builder.uninit()), + y: array::from_fn(|_| builder.uninit()), + is_infinity: Felt::uninit(builder), + } + } +} + +#[derive(Clone, Copy, 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. + 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], +} + +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()), + } + } +} + +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 + } +} diff --git a/ceno_recursion/src/zkvm_verifier/binding.rs b/ceno_recursion/src/zkvm_verifier/binding.rs index 50de33315..44d464641 100644 --- a/ceno_recursion/src/zkvm_verifier/binding.rs +++ b/ceno_recursion/src/zkvm_verifier/binding.rs @@ -11,7 +11,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}; @@ -800,6 +800,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 e521186f7..330417b0c 100644 --- a/ceno_recursion/src/zkvm_verifier/verifier.rs +++ b/ceno_recursion/src/zkvm_verifier/verifier.rs @@ -226,15 +226,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); @@ -551,16 +543,7 @@ 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); @@ -1881,7 +1864,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)); @@ -1960,7 +1947,11 @@ pub fn septic_ext_mul( a: &SepticExtensionVariable, b: &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)); @@ -2211,10 +2202,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/verifier.rs b/ceno_zkvm/src/scheme/verifier.rs index 94055853a..63aa545f5 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)) })?;