Merge pull request #1054 from powdr-labs/fix-halo2-verification

Fix Halo2 verification

executor/src/witgen/mod.rs

@@ -158,16 +158,9 @@ impl<'a, 'b, T: FieldElement> WitnessGenerator<'a, 'b, T> {
         record_end(OUTER_CODE_NAME);
         reset_and_print_profile_summary();
 
-        log::debug!("Publics:");
-        for (name, public_declaration) in self.analyzed.public_declarations_in_source_order() {
-            let poly_name = &public_declaration.referenced_poly_name();
-            let poly_index = public_declaration.index;
-            let value = columns[poly_name][poly_index as usize];
-            log::debug!("  {name:>30}: {value}");
-        }
-
         // Order columns according to the order of declaration.
-        self.analyzed
+        let witness_cols = self
+            .analyzed
             .committed_polys_in_source_order()
             .into_iter()
             .flat_map(|(p, _)| p.array_elements())
@@ -176,10 +169,35 @@ impl<'a, 'b, T: FieldElement> WitnessGenerator<'a, 'b, T> {
                 assert!(!column.is_empty());
                 (name, column)
             })
-            .collect()
+            .collect::<Vec<_>>();
+
+        log::debug!("Publics:");
+        for (name, value) in extract_publics(&witness_cols, self.analyzed) {
+            log::debug!("  {name:>30}: {value}");
+        }
+        witness_cols
     }
 }
 
+pub fn extract_publics<T: FieldElement>(
+    witness: &[(String, Vec<T>)],
+    pil: &Analyzed<T>,
+) -> Vec<(String, T)> {
+    let witness = witness
+        .iter()
+        .map(|(name, col)| (name.clone(), col))
+        .collect::<BTreeMap<_, _>>();
+    pil.public_declarations_in_source_order()
+        .iter()
+        .map(|(name, public_declaration)| {
+            let poly_name = &public_declaration.referenced_poly_name();
+            let poly_index = public_declaration.index;
+            let value = witness[poly_name][poly_index as usize];
+            ((*name).clone(), value)
+        })
+        .collect()
+}
+
 /// Data that is fixed for witness generation.
 pub struct FixedData<'a, T> {
     analyzed: &'a Analyzed<T>,

halo2/src/prover.rs

@@ -8,6 +8,7 @@ use halo2_proofs::{
             multiopen::{ProverGWC, VerifierGWC},
             strategy::AccumulatorStrategy,
         },
+        VerificationStrategy,
     },
     transcript::{EncodedChallenge, TranscriptReadBuffer, TranscriptWriterBuffer},
 };
@@ -250,11 +251,19 @@ impl<'a, F: FieldElement> Halo2Prover<'a, F> {
             AccumulatorStrategy::new(self.params.verifier_params()),
             &[instances.as_slice()],
             &mut transcript,
-        );
+        )
+        .map(|strategy| {
+            <AccumulatorStrategy<'_, _> as VerificationStrategy<'_, _, VerifierGWC<_>>>::finalize(
+                strategy,
+            )
+        });
 
         match res {
             Err(e) => Err(e.to_string()),
-            Ok(_) => Ok(()),
+            Ok(valid) => match valid {
+                true => Ok(()),
+                false => Err("Proof is invalid".to_string()),
+            },
         }
     }
 

pipeline/src/test_util.rs

@@ -98,6 +98,8 @@ pub fn test_halo2(_file_name: &str, _inputs: Vec<Bn254Field>) {}
 
 #[cfg(feature = "halo2")]
 pub fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
+    use powdr_executor::witgen::extract_publics;
+
     use crate::util::write_or_panic;
 
     let file_name = format!("{}/../test_data/{file_name}", env!("CARGO_MANIFEST_DIR"));
@@ -108,7 +110,11 @@ pub fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
         .with_prover_inputs(inputs)
         .with_backend(powdr_backend::BackendType::Halo2);
 
-    let pil = pipeline.optimized_pil_ref().unwrap();
+    // Generate a proof with the setup and verification key generated on the fly
+    pipeline.clone().proof().unwrap().proof.unwrap();
+
+    // Repeat the proof generation, but with an externally generated setup and verification key
+    let pil = pipeline.optimized_pil_ref().unwrap().clone();
 
     // Setup
     let setup_file_path = tmp_dir.as_path().join("params.bin");
@@ -119,6 +125,7 @@ pub fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
             .generate_setup(pil.degree(), writer)
             .unwrap()
     });
+    let mut pipeline = pipeline.with_setup_file(Some(setup_file_path));
 
     // Verification Key
     let vkey_file_path = tmp_dir.as_path().join("verification_key.bin");
@@ -126,24 +133,20 @@ pub fn gen_halo2_proof(file_name: &str, inputs: Vec<Bn254Field>) {
     write_or_panic(vkey_file, |writer| {
         pipeline.export_verification_key(writer).unwrap()
     });
+    let mut pipeline = pipeline.with_vkey_file(Some(vkey_file_path));
 
     // Create the proof before adding the setup and vkey to the backend,
     // so that they're generated during the proof
-    let proof = pipeline.clone().proof().unwrap().proof.unwrap();
+    let proof_artifact = pipeline.clone().proof().unwrap();
 
-    // Now we add the previously generated setup and verification key
-    // and verify the proof.
-    let mut pipeline = pipeline
-        .with_setup_file(Some(setup_file_path))
-        .with_vkey_file(Some(vkey_file_path));
+    let publics = extract_publics(proof_artifact.witness.as_ref().unwrap(), &pil)
+        .iter()
+        .map(|(_name, v)| *v)
+        .collect();
 
-    pipeline.verify(proof, &[vec![]]).unwrap();
-
-    // We can also run the same proof path as the first proof generation above,
-    // to make sure the proof also works when the setup and vkey are given
-    // and not generated on-the-fly.
-
-    pipeline.proof().unwrap().proof.unwrap();
+    pipeline
+        .verify(proof_artifact.proof.unwrap(), &[publics])
+        .unwrap();
 }
 
 #[cfg(not(feature = "halo2"))]

pipeline/tests/pil.rs

@@ -54,9 +54,8 @@ fn test_invalid_witness_halo2mock() {
         .unwrap();
 }
 
-// TODO: This test should panic but currently succeeds. See:
-// https://github.com/powdr-labs/powdr/pull/1051
 #[test]
+#[should_panic = "called `Result::unwrap()` on an `Err` value: [\"Proof is invalid\"]"]
 #[cfg(feature = "halo2")]
 fn test_invalid_witness_halo2() {
     let f = "pil/trivial.pil";