From d37116372d510c61e1e36e5dbaea0636fca2662a Mon Sep 17 00:00:00 2001
From: Georg Wiese <georgwiese@gmail.com>
Date: Tue, 13 Feb 2024 11:47:06 +0100
Subject: [PATCH] Test that proving fails for unsatisfying witness

---
 halo2/src/prover.rs       |  5 ---
 pipeline/src/pipeline.rs  | 22 ++++++++++++++
 pipeline/tests/pil.rs     | 64 ++++++++++++++++++++++++++++++++++++++-
 test_data/pil/trivial.pil |  5 +++
 4 files changed, 90 insertions(+), 6 deletions(-)
 create mode 100644 test_data/pil/trivial.pil

diff --git a/halo2/src/prover.rs b/halo2/src/prover.rs
index b4b3b1483..7956c9142 100644
--- a/halo2/src/prover.rs
+++ b/halo2/src/prover.rs
@@ -1,5 +1,4 @@
 use halo2_proofs::{
-    dev::MockProver,
     halo2curves::bn256::{Fr, G1Affine},
     plonk::{create_proof, keygen_pk, keygen_vk, verify_proof, Circuit, ProvingKey, VerifyingKey},
     poly::{
@@ -312,10 +311,6 @@ fn gen_proof<
     circuit: C,
     instances: &[Vec<Fr>],
 ) -> Vec<u8> {
-    MockProver::run(params.k(), &circuit, instances.to_vec().clone())
-        .unwrap()
-        .assert_satisfied();
-
     let instances = instances
         .iter()
         .map(|instances| instances.as_slice())
diff --git a/pipeline/src/pipeline.rs b/pipeline/src/pipeline.rs
index a342e43d5..a9d8f44d7 100644
--- a/pipeline/src/pipeline.rs
+++ b/pipeline/src/pipeline.rs
@@ -451,6 +451,28 @@ impl<T: FieldElement> Pipeline<T> {
         }
     }
 
+    /// Advances to PilWithEvaluatedFixedCols and then sets the witness to the provided value,
+    /// skipping witness generation.
+    pub fn skip_witness_generation(mut self, witness: Vec<(String, Vec<T>)>) -> Self {
+        self.advance_to(Stage::PilWithEvaluatedFixedCols).unwrap();
+
+        let (pil, fixed_cols) = match self.artifact.unwrap() {
+            Artifact::PilWithEvaluatedFixedCols(PilWithEvaluatedFixedCols { pil, fixed_cols }) => {
+                (pil, fixed_cols)
+            }
+            _ => panic!(),
+        };
+
+        Pipeline {
+            artifact: Some(Artifact::GeneratedWitness(GeneratedWitness {
+                pil,
+                fixed_cols,
+                witness: Some(witness),
+            })),
+            ..self
+        }
+    }
+
     fn name_from_path(path: &Path) -> String {
         path.file_stem().unwrap().to_str().unwrap().to_string()
     }
diff --git a/pipeline/tests/pil.rs b/pipeline/tests/pil.rs
index 8004fbc48..2f914c04c 100644
--- a/pipeline/tests/pil.rs
+++ b/pipeline/tests/pil.rs
@@ -1,11 +1,73 @@
+#[cfg(feature = "halo2")]
+use powdr_number::Bn254Field;
 use powdr_number::GoldilocksField;
-use powdr_pipeline::test_util::{gen_estark_proof, test_halo2, verify_test_file};
+use powdr_pipeline::{
+    test_util::{
+        gen_estark_proof, resolve_test_file, test_halo2, verify_pipeline, verify_test_file,
+    },
+    Pipeline,
+};
 use test_log::test;
 
 pub fn verify_pil(file_name: &str, inputs: Vec<GoldilocksField>) {
     verify_test_file(file_name, inputs, vec![]);
 }
 
+#[test]
+#[should_panic = "Pil verifier run was unsuccessful."]
+fn test_invalid_witness_pilcom() {
+    let f = "pil/trivial.pil";
+    let pipeline = Pipeline::default()
+        .from_file(resolve_test_file(f))
+        .skip_witness_generation(vec![(
+            "main.w".to_string(),
+            vec![GoldilocksField::from(0); 4],
+        )]);
+    verify_pipeline(pipeline);
+}
+
+#[test]
+#[should_panic = "assertion failed: stark_verify::<MerkleTreeGL,\\n            TranscriptGL>(&starkproof, &setup.const_root, &setup.starkinfo,\\n        &self.params, &mut setup.program).unwrap()"]
+fn test_invalid_witness_estark() {
+    let f = "pil/trivial.pil";
+    Pipeline::default()
+        .from_file(resolve_test_file(f))
+        .skip_witness_generation(vec![(
+            "main.w".to_string(),
+            vec![GoldilocksField::from(0); 4],
+        )])
+        .with_backend(powdr_backend::BackendType::EStark)
+        .proof()
+        .unwrap();
+}
+
+#[test]
+#[should_panic = "circuit was not satisfied"]
+#[cfg(feature = "halo2")]
+fn test_invalid_witness_halo2mock() {
+    let f = "pil/trivial.pil";
+    Pipeline::default()
+        .from_file(resolve_test_file(f))
+        .skip_witness_generation(vec![("main.w".to_string(), vec![Bn254Field::from(0); 4])])
+        .with_backend(powdr_backend::BackendType::Halo2Mock)
+        .proof()
+        .unwrap();
+}
+
+// TODO: This test should panic but currently succeeds. See:
+// https://github.com/powdr-labs/powdr/pull/1051
+#[test]
+#[cfg(feature = "halo2")]
+fn test_invalid_witness_halo2() {
+    let f = "pil/trivial.pil";
+    Pipeline::default()
+        .from_file(resolve_test_file(f))
+        .skip_witness_generation(vec![("main.w".to_string(), vec![Bn254Field::from(0); 4])])
+        .with_backend(powdr_backend::BackendType::Halo2)
+        .proof()
+        .unwrap();
+}
+
 #[test]
 fn test_fibonacci() {
     let f = "pil/fibonacci.pil";
diff --git a/test_data/pil/trivial.pil b/test_data/pil/trivial.pil
new file mode 100644
index 000000000..bf3f37eef
--- /dev/null
+++ b/test_data/pil/trivial.pil
@@ -0,0 +1,5 @@
+// The the simplest PIL that doesn't get optimized away completely.
+namespace main(4);
+    let index = |i| i;
+    let w;
+    w = index;
\ No newline at end of file