Skip to content

Fix leaf recursion debug constraint mismatches #1368

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
kunxian-xia wants to merge 1 commit into from
Closed

Fix leaf recursion debug constraint mismatches #1368

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions ceno_recursion_v2/src/bus.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,9 @@ pub struct TowerModuleMessage<T> {
pub idx: T,
pub tidx: T,
pub n_logup: T,
pub num_read_count: T,
pub num_write_count: T,
pub num_logup_count: T,
}

define_typed_per_proof_permutation_bus!(TowerModuleBus, TowerModuleMessage);
Expand Down
4 changes: 4 additions & 0 deletions ceno_recursion_v2/src/circuit/inner/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ pub use trace::*;
pub struct InnerCircuit<S: AggregationSubCircuit> {
pub verifier_circuit: Arc<S>,
pub def_hook_commit: Option<CommitBytes>,
pub has_fixed_commit: bool,
pub has_fixed_no_omc_init_commit: bool,
pub instance_public_value_indices: Arc<Vec<Vec<usize>>>,
}

Expand Down Expand Up @@ -67,6 +69,8 @@ impl<SC: StarkProtocolConfig<F = F>, S: AggregationSubCircuit> Circuit<SC> for I
lookup_challenge_bus,
pvs_air_consistency_bus,
deferral_enabled,
has_fixed_commit: self.has_fixed_commit,
has_fixed_no_omc_init_commit: self.has_fixed_no_omc_init_commit,
instance_public_value_indices: self.instance_public_value_indices.clone(),
}) as AirRef<SC>;

Expand Down
132 changes: 99 additions & 33 deletions ceno_recursion_v2/src/circuit/inner/vm_pvs/air.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,13 @@
use std::{borrow::Borrow, sync::Arc};

use ceno_emul::{FullTracer as Tracer, WORD_SIZE};
use ceno_zkvm::instructions::riscv::constants::{
END_CYCLE_IDX, END_PC_IDX, EXIT_CODE_IDX, EXIT_PC, HEAP_LENGTH_IDX, HEAP_START_ADDR_IDX,
HINT_LENGTH_IDX, HINT_START_ADDR_IDX, INIT_CYCLE_IDX, INIT_PC_IDX, PUBIO_DIGEST_IDX,
SHARD_ID_IDX, SHARD_RW_SUM_IDX,
use ceno_zkvm::{
instructions::riscv::constants::{
END_CYCLE_IDX, END_PC_IDX, EXIT_CODE_IDX, EXIT_PC, HEAP_LENGTH_IDX, HEAP_START_ADDR_IDX,
HINT_LENGTH_IDX, HINT_START_ADDR_IDX, INIT_CYCLE_IDX, INIT_PC_IDX, PUBIO_DIGEST_IDX,
SHARD_ID_IDX, SHARD_RW_SUM_IDX,
},
scheme::PublicValues,
};
use openvm_circuit_primitives::utils::{and, assert_array_eq, not};
use openvm_stark_backend::{
Expand All @@ -21,7 +24,11 @@ use stark_recursion_circuit_derive::AlignedBorrow;

use crate::{
bus::{LookupChallengeBus, LookupChallengeKind, LookupChallengeMessage},
circuit::inner::{bus::PvsAirConsistencyBus, vm_pvs::VmPvs},
circuit::inner::{
bus::{PvsAirConsistencyBus, PvsAirConsistencyMessage},
vm_pvs::VmPvs,
},
utils::TranscriptLabel,
};

#[repr(C)]
Expand All @@ -35,6 +42,9 @@ pub struct VmPvsCols<F> {
pub lookup_challenge_beta: [F; D_EF],
pub lookup_challenge_alpha_lookup_count: F,
pub lookup_challenge_beta_lookup_count: F,
pub fixed_commit_log2_max_codeword_size: F,
pub fixed_no_omc_init_commit_log2_max_codeword_size: F,
pub witness_commit_log2_max_codeword_size: F,
pub child_pvs: VmPvs<F>,
}

Expand All @@ -45,6 +55,8 @@ pub struct VmPvsAir {
pub lookup_challenge_bus: LookupChallengeBus,
pub pvs_air_consistency_bus: PvsAirConsistencyBus,
pub deferral_enabled: bool,
pub has_fixed_commit: bool,
pub has_fixed_no_omc_init_commit: bool,
pub instance_public_value_indices: Arc<Vec<Vec<usize>>>,
}

Expand Down Expand Up @@ -189,41 +201,60 @@ impl<AB: AirBuilder + InteractionBuilder + AirBuilderWithPublicValues> Air<AB> f
// );

// Commitments are observed after transcript-visible public values in preflight.
let start_tidx_after_public_value = VmPvs::<u8>::width() - 3 * DIGEST_SIZE;
for (didx, value) in local.child_pvs.fixed_commit.iter().enumerate() {
self.transcript_bus.receive(
let mut commit_tidx = TranscriptLabel::Riscv.field_len() + PublicValues::flattened_len();
if self.has_fixed_commit {
receive_commitment(
self,
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(start_tidx_after_public_value + didx),
value: (*value).into(),
is_sample: AB::Expr::ZERO,
},
commit_tidx,
local.child_pvs.fixed_commit,
local.fixed_commit_log2_max_codeword_size,
local.is_valid,
);
commit_tidx += DIGEST_SIZE + 1;
}
for (didx, value) in local.child_pvs.fixed_no_omc_init_commit.iter().enumerate() {
if self.has_fixed_no_omc_init_commit {
receive_commitment(
self,
builder,
local.proof_idx,
commit_tidx,
local.child_pvs.fixed_no_omc_init_commit,
local.fixed_no_omc_init_commit_log2_max_codeword_size,
local.is_valid,
);
commit_tidx += DIGEST_SIZE + 1;
}
receive_commitment(
self,
builder,
local.proof_idx,
commit_tidx,
local.child_pvs.witness_commit,
local.witness_commit_log2_max_codeword_size,
local.is_valid,
);
commit_tidx += DIGEST_SIZE + 1;

for i in 0..D_EF {
self.transcript_bus.receive(
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(start_tidx_after_public_value + DIGEST_SIZE + didx),
value: (*value).into(),
is_sample: AB::Expr::ZERO,
tidx: AB::Expr::from_usize(commit_tidx + i),
value: local.lookup_challenge_alpha[i].into(),
is_sample: AB::Expr::ONE,
},
local.is_valid,
);
}
for (didx, value) in local.child_pvs.witness_commit.iter().enumerate() {
self.transcript_bus.receive(
builder,
local.proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(
start_tidx_after_public_value + 2 * DIGEST_SIZE + didx,
),
value: (*value).into(),
is_sample: AB::Expr::ZERO,
tidx: AB::Expr::from_usize(commit_tidx + D_EF + i),
value: local.lookup_challenge_beta[i].into(),
is_sample: AB::Expr::ONE,
},
local.is_valid,
);
Expand Down Expand Up @@ -253,15 +284,15 @@ impl<AB: AirBuilder + InteractionBuilder + AirBuilderWithPublicValues> Air<AB> f
}

// We look up proof metadata from VerifierPvsAir here to ensure consistency on each row.
// self.pvs_air_consistency_bus.lookup_key(
// builder,
// local.proof_idx,
// PvsAirConsistencyMessage {
// deferral_flag,
// has_verifier_pvs: local.has_verifier_pvs.into(),
// },
// local.is_valid,
// );
self.pvs_air_consistency_bus.lookup_key(
builder,
local.proof_idx,
PvsAirConsistencyMessage {
deferral_flag,
has_verifier_pvs: local.has_verifier_pvs.into(),
},
local.is_valid,
);

// Finally, constrain that this AIR's output public values are consistent with child_pvs.
let &VmPvs::<_> {
Expand Down Expand Up @@ -383,6 +414,41 @@ where
}
}

fn receive_commitment<AB>(
air: &VmPvsAir,
builder: &mut AB,
proof_idx: AB::Var,
start_tidx: usize,
commit: [AB::Var; DIGEST_SIZE],
log2_max_codeword_size: AB::Var,
mult: AB::Var,
) where
AB: AirBuilder + InteractionBuilder + AirBuilderWithPublicValues,
{
for (didx, value) in commit.into_iter().enumerate() {
air.transcript_bus.receive(
builder,
proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(start_tidx + didx),
value: value.into(),
is_sample: AB::Expr::ZERO,
},
mult,
);
}
air.transcript_bus.receive(
builder,
proof_idx,
TranscriptBusMessage {
tidx: AB::Expr::from_usize(start_tidx + DIGEST_SIZE),
value: log2_max_codeword_size.into(),
is_sample: AB::Expr::ZERO,
},
mult,
);
}

impl VmPvsAir {
fn eval_deferrals<AB>(
&self,
Expand Down
6 changes: 3 additions & 3 deletions ceno_recursion_v2/src/circuit/inner/vm_pvs/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,9 @@ pub fn run_preflight<TS>(

let alpha_ext = ts.sample_ext();
let beta_ext = ts.sample_ext();
eprintln!("vm_pvs alpha {} beta {}", alpha_ext, beta_ext);
preflight.vm_pvs.lookup_challenge_alpha = alpha_ext;
preflight.vm_pvs.lookup_challenge_beta = beta_ext;
preflight.vm_pvs.lookup_challenge_alpha_lookup_count = 0;
preflight.vm_pvs.lookup_challenge_beta_lookup_count = 0;
let present_air_count = proof.chip_proofs.len();
preflight.vm_pvs.lookup_challenge_alpha_lookup_count = present_air_count;
preflight.vm_pvs.lookup_challenge_beta_lookup_count = present_air_count;
}
15 changes: 15 additions & 0 deletions ceno_recursion_v2/src/circuit/inner/vm_pvs/trace.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,16 @@ pub fn generate_proving_ctx(
.as_ref()
.map(|commitment| commitment.commit.clone()),
);
let fixed_commit_log2_max_codeword_size = child_vk
.fixed_commit
.as_ref()
.map(|commitment| F::from_u64(commitment.log2_max_codeword_size as u64))
.unwrap_or(F::ZERO);
let fixed_no_omc_init_commit_log2_max_codeword_size = child_vk
.fixed_no_omc_init_commit
.as_ref()
.map(|commitment| F::from_u64(commitment.log2_max_codeword_size as u64))
.unwrap_or(F::ZERO);

for (row_idx, row) in trace.chunks_exact_mut(width).enumerate() {
let (base_row, def_row) = row.split_at_mut(VmPvsCols::<u8>::width());
Expand All @@ -64,6 +74,11 @@ pub fn generate_proving_ctx(
F::from_usize(preflight.vm_pvs.lookup_challenge_alpha_lookup_count);
cols.lookup_challenge_beta_lookup_count =
F::from_usize(preflight.vm_pvs.lookup_challenge_beta_lookup_count);
cols.fixed_commit_log2_max_codeword_size = fixed_commit_log2_max_codeword_size;
cols.fixed_no_omc_init_commit_log2_max_codeword_size =
fixed_no_omc_init_commit_log2_max_codeword_size;
cols.witness_commit_log2_max_codeword_size =
F::from_u64(proof.witin_commit.log2_max_codeword_size as u64);
cols.child_pvs = build_vm_pvs(fixed_commit, fixed_no_omc_init_commit, proof);
}

Expand Down
4 changes: 4 additions & 0 deletions ceno_recursion_v2/src/continuation/prover/inner/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,8 @@ impl<
let circuit = Arc::new(InnerCircuit::new(
Arc::new(verifier_circuit),
def_hook_commit.map(|d| d.into()),
child_vk.fixed_commit.is_some(),
child_vk.fixed_no_omc_init_commit.is_some(),
instance_public_value_indices,
));
let (pk, vk) = engine.keygen(&circuit.airs());
Expand Down Expand Up @@ -127,6 +129,8 @@ impl<
let circuit = Arc::new(InnerCircuit::new(
Arc::new(verifier_circuit),
def_hook_commit.map(|d| d.into()),
child_vk.fixed_commit.is_some(),
child_vk.fixed_no_omc_init_commit.is_some(),
instance_public_value_indices,
));
let vk = Arc::new(pk.get_vk());
Expand Down
9 changes: 3 additions & 6 deletions ceno_recursion_v2/src/continuation/prover/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,9 +67,8 @@ impl AggregationOptions {
}

type CenoProof = ZKVMProof<RecursionField, Basefold<RecursionField, BasefoldRSParams>>;
type Engine = BabyBearPoseidon2CpuEngine<
openvm_stark_sdk::config::baby_bear_poseidon2::DuplexSponge,
>;
type Engine =
BabyBearPoseidon2CpuEngine<openvm_stark_sdk::config::baby_bear_poseidon2::DuplexSponge>;

/// Full recursion pipeline that aggregates N Ceno base-layer shard proofs
/// into a single compact root proof.
Expand All @@ -91,9 +90,7 @@ pub struct AggProver<const LEAF_FANIN: usize, const INTERNAL_FANIN: usize> {
options: AggregationOptions,
}

impl<const LEAF_FANIN: usize, const INTERNAL_FANIN: usize>
AggProver<LEAF_FANIN, INTERNAL_FANIN>
{
impl<const LEAF_FANIN: usize, const INTERNAL_FANIN: usize> AggProver<LEAF_FANIN, INTERNAL_FANIN> {
/// Create a new aggregation prover from the base-layer verifying key.
pub fn new(child_vk: Arc<RecursionVk>, options: AggregationOptions) -> Self {
let leaf_prover = InnerCpuProver::<LEAF_FANIN>::new::<Engine>(
Expand Down
Loading
Loading