Skip to content

control num_instances in one place to improve soundness check #901

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
wants to merge 2 commits into from
Closed

control num_instances in one place to improve soundness check #901

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e712182
move num_instances to root proof level
hero78119 Apr 9, 2025
005efdc
unify non-uniform witness in proof
hero78119 Apr 9, 2025
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
2 changes: 1 addition & 1 deletion ceno_zkvm/src/bin/e2e.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ fn verify(proof_file: &str, vk_file: &str) {
let transcript = TranscriptWithStat::new(&stat_recorder, b"riscv");
assert!(
verifier
.verify_proof_halt(zkvm_proof.clone(), transcript, zkvm_proof.has_halt())
.verify_proof_halt(zkvm_proof.clone(), transcript, zkvm_proof.has_halt(&vk))
.is_ok()
);
println!("e2e proof stat: {}", zkvm_proof);
Expand Down
67 changes: 36 additions & 31 deletions ceno_zkvm/src/scheme.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use sumcheck::structs::IOPProverMessage;

use crate::{
instructions::{Instruction, riscv::ecall::HaltInstruction},
structs::TowerProofs,
structs::{TowerProofs, ZKVMVerifyingKey},
};

pub mod constants;
Expand All @@ -30,9 +30,6 @@ mod tests;
deserialize = "E::BaseField: DeserializeOwned"
))]
pub struct ZKVMOpcodeProof<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> {
// TODO support >1 opcodes
pub num_instances: usize,

// product constraints
pub record_r_out_evals: Vec<E>,
pub record_w_out_evals: Vec<E>,
Expand Down Expand Up @@ -73,9 +70,6 @@ pub struct ZKVMTableProof<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>>

pub tower_proof: TowerProofs<E>,

// num_vars hint for rw dynamic address to work
pub rw_hints_num_vars: Vec<usize>,

pub fixed_in_evals: Vec<E>,
pub fixed_opening_proof: Option<PCS::Proof>,
pub wits_commit: PCS::Commitment,
Expand Down Expand Up @@ -144,8 +138,10 @@ pub struct ZKVMProof<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> {
pub raw_pi: Vec<Vec<E::BaseField>>,
// the evaluation of raw_pi.
pub pi_evals: Vec<E>,
opcode_proofs: BTreeMap<String, (usize, ZKVMOpcodeProof<E, PCS>)>,
Copy link
Collaborator Author

@hero78119 hero78119 Apr 9, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

here we have

  • String: circuit name
  • usize: circuit index

to carry information in proof. However a malicious prover can make both inconsistent.

The new fixed avoid duplicated information appear in different place

table_proofs: BTreeMap<String, (usize, ZKVMTableProof<E, PCS>)>,
// circuit size -> instance mapping
pub num_instances: Vec<(usize, usize)>,
opcode_proofs: BTreeMap<usize, ZKVMOpcodeProof<E, PCS>>,
table_proofs: BTreeMap<usize, ZKVMTableProof<E, PCS>>,
}

impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProof<E, PCS> {
Expand All @@ -167,6 +163,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProof<E, PCS> {
Self {
raw_pi,
pi_evals,
num_instances: vec![],
opcode_proofs: BTreeMap::new(),
table_proofs: BTreeMap::new(),
}
Expand All @@ -180,11 +177,19 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProof<E, PCS> {
self.opcode_proofs.len() + self.table_proofs.len()
}

pub fn has_halt(&self) -> bool {
pub fn has_halt(&self, vk: &ZKVMVerifyingKey<E, PCS>) -> bool {
let halt_instance_count = self
.opcode_proofs
.get(&HaltInstruction::<E>::name())
.map(|(_, p)| p.num_instances)
.num_instances
.iter()
.find_map(|(circuit_index, num_instances)| {
(*circuit_index
== vk
.circuit_vks
.keys()
.position(|circuit_name| *circuit_name == HaltInstruction::<E>::name())
.expect("halt circuit not exist"))
.then_some(*num_instances)
})
.unwrap_or(0);
if halt_instance_count > 0 {
assert_eq!(
Expand All @@ -208,10 +213,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let mpcs_opcode_commitment = self
.opcode_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These change make less readibility since now we lost circuit_name and instead only circuit index. But it's ok we fix it later, for now mpcs still be the major bottleneck of proof size

.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.wits_commit);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -221,10 +226,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let mpcs_opcode_opening = self
.opcode_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.wits_opening_proof);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -235,10 +240,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let tower_proof_opcode = self
.opcode_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.tower_proof);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -249,10 +254,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let main_sumcheck_opcode = self
.opcode_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.main_sel_sumcheck_proofs);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -263,10 +268,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let mpcs_table_commitment = self
.table_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.wits_commit);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -276,10 +281,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let mpcs_table_opening = self
.table_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.wits_opening_proof);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -289,10 +294,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let mpcs_table_fixed_opening = self
.table_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.fixed_opening_proof);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -303,10 +308,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let tower_proof_table = self
.table_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.tower_proof);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand All @@ -317,10 +322,10 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E> + Serialize> fmt::Dis
let same_r_sumcheck_table = self
.table_proofs
.iter()
.map(|(circuit_name, (_, proof))| {
.map(|(circuit_index, proof)| {
let size = bincode::serialized_size(&proof.same_r_sumcheck_proofs);
size.inspect(|size| {
*by_circuitname_stats.entry(circuit_name).or_insert(0) += size;
*by_circuitname_stats.entry(circuit_index).or_insert(0) += size;
})
})
.collect::<Result<Vec<u64>, _>>()
Expand Down
65 changes: 45 additions & 20 deletions ceno_zkvm/src/scheme/prover.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,13 +64,14 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
pi: PublicValues<u32>,
mut transcript: impl Transcript<E>,
) -> Result<ZKVMProof<E, PCS>, ZKVMError> {
let span = entered_span!("commit_to_fixed_commit", profiling_1 = true);
let mut vm_proof = ZKVMProof::empty(pi);

let span = entered_span!("commit_to_pi", profiling_1 = true);
// including raw public input to transcript
for v in vm_proof.raw_pi.iter().flatten() {
transcript.append_field_element(v);
}
exit_span!(span);

let pi: Vec<ArcMultilinearExtension<E>> = vm_proof
.raw_pi
Expand All @@ -82,6 +83,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
.collect();

// commit to fixed commitment
let span = entered_span!("commit_to_fixed_commit", profiling_1 = true);
for pk in self.pk.circuit_pks.values() {
if let Some(fixed_commit) = &pk.vk.fixed_commit {
PCS::write_commitment(fixed_commit, &mut transcript)
Expand All @@ -91,10 +93,48 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
exit_span!(span);

// commit to main traces
let circuit_name_index_mapping = self
.pk
.circuit_pks
.keys()
.enumerate()
.map(|(k, v)| (v, k))
.collect::<BTreeMap<_, _>>();
let mut commitments = BTreeMap::new();
let mut wits = BTreeMap::new();
let mut structural_wits = BTreeMap::new();

let mut num_instances = Vec::with_capacity(self.pk.circuit_pks.len());
for (index, (circuit_name, _)) in self.pk.circuit_pks.iter().enumerate() {
if let Some(num_instance) = witnesses
.get_opcode_witness(circuit_name)
.or_else(|| {
witnesses
.get_table_witness(circuit_name)
.map(|rmms| &rmms[0])
})
.map(|rmm| rmm.num_instances())
.and_then(|num_instance| {
if num_instance > 0 {
Some(num_instance)
} else {
None
}
})
{
num_instances.push((index, num_instance));
}
}

// verifier need this information from prover to achieve non-uniform design.
vm_proof.num_instances = num_instances;

// write (circuit_size, num_var) to transcript
for (circuit_size, num_var) in &vm_proof.num_instances {
transcript.append_message(&circuit_size.to_le_bytes());
transcript.append_message(&num_var.to_le_bytes());
}

let commit_to_traces_span = entered_span!("commit_to_traces", profiling_1 = true);
// commit to opcode circuits first and then commit to table circuits, sorted by name
for (circuit_name, mut rmm) in witnesses.into_iter_sorted() {
Expand All @@ -120,7 +160,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
PCS::batch_commit_and_write(&self.pk.pp, witness_rmm, &mut transcript)
.map_err(ZKVMError::PCSError)?;
let witness = PCS::get_arc_mle_witness_from_commitment(&commit);
commitments.insert(circuit_name.clone(), commit);
commitments.insert(circuit_name_index_mapping[&circuit_name], commit);
(witness, structural_witness)
}
};
Expand Down Expand Up @@ -155,7 +195,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
continue;
}
transcript.append_field_element(&E::BaseField::from_u64(index as u64));
let wits_commit = commitments.remove(circuit_name).unwrap();
let wits_commit = commitments.remove(&index).unwrap();
// TODO: add an enum for circuit type either in constraint_system or vk
let cs = pk.get_cs();
let is_opcode_circuit = cs.lk_table_expressions.is_empty()
Expand Down Expand Up @@ -187,9 +227,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
circuit_name,
num_instances
);
vm_proof
.opcode_proofs
.insert(circuit_name.clone(), (index, opcode_proof));
vm_proof.opcode_proofs.insert(index, opcode_proof);
} else {
let (structural_witness, structural_num_instances) = structural_wits
.remove(circuit_name)
Expand All @@ -211,9 +249,7 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
num_instances,
structural_num_instances
);
vm_proof
.table_proofs
.insert(circuit_name.clone(), (index, table_proof));
vm_proof.table_proofs.insert(index, table_proof);
for (idx, eval) in pi_in_evals {
vm_proof.update_pi_eval(idx, eval);
}
Expand Down Expand Up @@ -652,7 +688,6 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
let wits_commit = PCS::get_pure_commitment(&wits_commit);

Ok(ZKVMOpcodeProof {
num_instances,
record_r_out_evals,
record_w_out_evals,
lk_p1_out_eval,
Expand Down Expand Up @@ -919,15 +954,6 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
})
.collect_vec();

// (non uniform) collect dynamic address hints as witness for verifier
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Move this information from table proof to centralized place, and aligned with opcode proof with same terminology: num_instance

let rw_hints_num_vars = structural_witnesses
.iter()
.map(|mle| mle.num_vars())
.collect_vec();
for var in rw_hints_num_vars.iter() {
transcript.append_message(&var.to_le_bytes());
}

let (rt_tower, tower_proof) = TowerProver::create_proof(
// pattern [r1, w1, r2, w2, ...] same pair are chain together
r_wit_layers
Expand Down Expand Up @@ -1130,7 +1156,6 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>> ZKVMProver<E, PCS> {
tower_proof,
fixed_in_evals,
fixed_opening_proof,
rw_hints_num_vars,
wits_in_evals,
wits_commit,
wits_opening_proof,
Expand Down
1 change: 1 addition & 0 deletions ceno_zkvm/src/scheme/tests.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,7 @@ fn test_rw_lk_expression_combination() {
&vk.vp,
verifier.vk.circuit_vks.get(&name).unwrap(),
&proof,
num_instances,
&[],
&mut v_transcript,
NUM_FANIN,
Expand Down
Loading