fix(soundness): bind verifying-key digest into proof transcript (#356)

.gitignore

@@ -1,4 +1,5 @@
 target
+.tmp/
 .vscode
 .idea
 *.log

ceno_recursion/src/zkvm_verifier/verifier.rs

@@ -113,7 +113,7 @@ fn challenger_observe_exts<C: Config>(
     }
 }
 
-pub fn verify_zkvm_proof<C: Config<F = F>>(
+pub fn verify_zkvm_proof<C: Config<F = F, EF = E>>(
     builder: &mut Builder<C>,
     zkvm_proof_input: ZKVMProofInputVariable<C>,
     vk: &ZKVMVerifyingKey<E, Pcs>,
@@ -125,6 +125,14 @@ pub fn verify_zkvm_proof<C: Config<F = F>>(
     let prod_w: Ext<C::F, C::EF> = builder.constant(C::EF::ONE);
     let logup_sum: Ext<C::F, C::EF> = builder.constant(C::EF::ZERO);
 
+    let vk_digest = vk.compute_digest();
+    let vk_digest_array: Array<C, Ext<C::F, C::EF>> = builder.dyn_array(vk_digest.len());
+    for (i, digest_element) in vk_digest.iter().enumerate() {
+        let baked: Ext<C::F, C::EF> = builder.constant(*digest_element);
+        builder.set_value(&vk_digest_array, i, baked);
+    }
+    challenger_observe_exts(builder, &mut challenger, &vk_digest_array);
+
     for (_, circuit_vk) in vk.circuit_vks.iter() {
         for instance_value in circuit_vk.get_cs().zkvm_v1_css.instance.iter() {
             let raw = builder.get(&zkvm_proof_input.pi, instance_value.0);

ceno_zkvm/Cargo.toml

@@ -23,6 +23,7 @@ mpcs = { workspace = true, features = ["whir"] }
 multilinear_extensions.workspace = true
 once_cell.workspace = true
 p3.workspace = true
+poseidon.workspace = true
 rayon.workspace = true
 serde.workspace = true
 serde_json.workspace = true

ceno_zkvm/src/scheme/prover.rs

@@ -34,7 +34,7 @@ use crate::{
         hal::{DeviceProvingKey, ProofInput},
         utils::build_main_witness,
     },
-    structs::{TowerProofs, ZKVMProvingKey, ZKVMWitnesses},
+    structs::{RV32imMemStateConfig, TowerProofs, ZKVMProvingKey, ZKVMWitnesses},
 };
 
 type CreateTableProof<'a, PB> = (
@@ -317,6 +317,11 @@ impl<
             shard_id = shard_ctx.shard_id
         )
         .in_scope(|| {
+            let digest_span = entered_span!("commit_to_vk_digest", profiling_1 = true);
+            let vk_digest = self.pk.compute_vk_digest::<RV32imMemStateConfig>();
+            transcript.append_field_element_exts(&vk_digest);
+            exit_span!(digest_span);
+
             let span = entered_span!("commit_to_pi", profiling_1 = true);
             // Include transcript-visible public values in canonical circuit order.
             // The order must match verifier and recursion verifier exactly.

ceno_zkvm/src/scheme/verifier.rs

@@ -491,6 +491,9 @@ impl<E: ExtensionField, PCS: PolynomialCommitmentScheme<E>>
             }
         }
 
+        let vk_digest = self.vk.compute_digest();
+        transcript.append_field_element_exts(&vk_digest);
+
         // Include transcript-visible public values in canonical circuit order.
         // This must match prover and recursion verifier exactly.
         for (_, circuit_vk) in self.vk.circuit_vks.iter() {

ceno_zkvm/src/structs.rs

@@ -19,6 +19,8 @@ use gkr_iop::{
 use itertools::Itertools;
 use mpcs::{Point, PolynomialCommitmentScheme};
 use multilinear_extensions::Instance;
+use p3::field::FieldAlgebra;
+use poseidon::challenger::{CanObserve, DefaultChallenger, FieldChallenger};
 use rayon::{
     iter::{IntoParallelIterator, IntoParallelRefIterator, ParallelIterator},
     prelude::ParallelSlice,
@@ -965,6 +967,101 @@ pub struct ZKVMVerifyingKey<
     pub fixed_no_omc_init_commit: Option<<PCS as PolynomialCommitmentScheme<E>>::Commitment>,
     // circuit index -> circuit name
     // mainly used for debugging
+    #[serde(skip)]
     pub circuit_index_to_name: BTreeMap<usize, String>,
     pub mem_state_verifier: M,
 }
+
+/// Number of extension-field elements squeezed from the digest sponge.
+pub const VK_DIGEST_LEN: usize = 2;
+
+/// Convert bytes into base-field elements using ≤ 3-byte chunks.
+fn bytes_to_felts_safe<F: FieldAlgebra>(bytes: &[u8]) -> Vec<F> {
+    bytes
+        .chunks(3)
+        .map(|chunk| {
+            let mut arr = [0u8; 4];
+            arr[..chunk.len()].copy_from_slice(chunk);
+            F::from_canonical_u32(u32::from_le_bytes(arr))
+        })
+        .collect()
+}
+
+/// Hash the supplied VK preimage into `VK_DIGEST_LEN` extension elements.
+/// `circuits` must iterate in `BTreeMap` lex order on `name`.
+fn compute_vk_digest_inner<'a, E, PCS, M>(
+    vp: &PCS::VerifierParam,
+    entry_pc: u32,
+    fixed_commit: &Option<<PCS as PolynomialCommitmentScheme<E>>::Commitment>,
+    fixed_no_omc_init_commit: &Option<<PCS as PolynomialCommitmentScheme<E>>::Commitment>,
+    mem_state_verifier: &M,
+    circuits: impl IntoIterator<Item = (&'a String, &'a VerifyingKey<E>)>,
+) -> [E; VK_DIGEST_LEN]
+where
+    E: ExtensionField,
+    PCS: PolynomialCommitmentScheme<E>,
+    M: Serialize,
+{
+    let circuit_view: Vec<(&str, &ComposedConstrainSystem<E>)> = circuits
+        .into_iter()
+        .map(|(name, vk)| (name.as_str(), &vk.cs))
+        .collect();
+    let bytes = bincode::serialize(&(
+        vp,
+        entry_pc,
+        fixed_commit,
+        fixed_no_omc_init_commit,
+        mem_state_verifier,
+        &circuit_view,
+    ))
+    .expect("vk digest serialization is infallible for a valid VK");
+
+    let mut sponge = DefaultChallenger::<E::BaseField>::new_poseidon_default();
+    sponge.observe_slice(&bytes_to_felts_safe::<E::BaseField>(&bytes));
+    std::array::from_fn(|_| sponge.sample_ext_element())
+}
+
+impl<E, PCS, M> ZKVMVerifyingKey<E, PCS, M>
+where
+    E: ExtensionField,
+    PCS: PolynomialCommitmentScheme<E>,
+    M: Clone + Default + Serialize + DeserializeOwned,
+{
+    /// Poseidon-sponge digest of the verifying key's soundness-bound fields.
+    pub fn compute_digest(&self) -> [E; VK_DIGEST_LEN] {
+        compute_vk_digest_inner::<E, PCS, M>(
+            &self.vp,
+            self.entry_pc,
+            &self.fixed_commit,
+            &self.fixed_no_omc_init_commit,
+            &self.mem_state_verifier,
+            self.circuit_vks.iter(),
+        )
+    }
+}
+
+impl<E, PCS> ZKVMProvingKey<E, PCS>
+where
+    E: ExtensionField,
+    PCS: PolynomialCommitmentScheme<E>,
+{
+    /// Prover-side mirror of [`ZKVMVerifyingKey::compute_digest`] for `M`.
+    pub fn compute_vk_digest<M>(&self) -> [E; VK_DIGEST_LEN]
+    where
+        M: Clone + Default + From<Platform> + Serialize,
+    {
+        let mem_state_verifier: M = self
+            .program_ctx
+            .as_ref()
+            .map(|ctx| M::from(ctx.platform.clone()))
+            .unwrap_or_default();
+        compute_vk_digest_inner::<E, PCS, M>(
+            &self.vp,
+            self.entry_pc,
+            &self.fixed_commit,
+            &self.fixed_no_omc_init_commit,
+            &mem_state_verifier,
+            self.circuit_pks.iter().map(|(n, pk)| (n, &pk.vk)),
+        )
+    }
+}

gkr_iop/src/circuit_builder.rs

@@ -169,6 +169,7 @@ pub struct ConstraintSystem<E: ExtensionField> {
     pub chip_record_alpha: Expression<E>,
     pub chip_record_beta: Expression<E>,
 
+    #[serde(skip)]
     pub debug_map: HashMap<usize, Vec<Expression<E>>>,
 
     pub(crate) phantom: PhantomData<E>,