Add --disable-safety-check option

This option allows variables that are not constrained.

examples/fixture/asm/kimchi/unused_variables.asm

@@ -0,0 +1,7 @@
+@ noname.0.7.0
+@ public inputs: 1
+
+DoubleGeneric<1>
+DoubleGeneric<1,0,-1,0,1>
+DoubleGeneric<1,0,0,0,-2>
+(0,0) -> (2,0)

examples/fixture/asm/r1cs/unused_variables.asm

@@ -0,0 +1,4 @@
+@ noname.0.7.0
+@ public inputs: 1
+
+2 == (v_1) * (1)

examples/unused_variables.no

@@ -0,0 +1,4 @@
+fn main(pub xx: Field, yy: Field) {
+    let zz = yy + 1;
+    assert_eq(xx, 2);
+}

src/backends/kimchi/mod.rs

@@ -309,6 +309,7 @@ impl Backend for KimchiVesta {
         &mut self,
         public_output: Option<Var<Self::Field, Self::Var>>,
         returned_cells: Option<Vec<KimchiCellVar>>,
+        disable_safety_check: bool,
     ) -> Result<()> {
         // TODO: the current tests pass even this is commented out. Add a test case for this one.
         // important: there might still be a pending generic gate
@@ -338,14 +339,18 @@ impl Backend for KimchiVesta {
                     .find(|private_cell_var| private_cell_var.index == var)
                 {
                     // TODO: is this error useful?
-                    let err = Error::new(
-                        "constraint-finalization",
-                        ErrorKind::PrivateInputNotUsed,
-                        private_cell_var.span,
-                    );
-                    Err(err)?;
+                    if !disable_safety_check {
+                        let err = Error::new(
+                            "constraint-finalization",
+                            ErrorKind::PrivateInputNotUsed,
+                            private_cell_var.span,
+                        );
+                        Err(err)?;
+                    }
                 } else {
-                    Err(Error::new("contraint-finalization", ErrorKind::UnexpectedError("there's a bug in the circuit_writer, some cellvar does not end up being a cellvar in the circuit!"), Span::default()))?;
+                    if !disable_safety_check {
+                        Err(Error::new("contraint-finalization", ErrorKind::UnexpectedError("there's a bug in the circuit_writer, some cellvar does not end up being a cellvar in the circuit!"), Span::default()))?;
+                    }
                 }
             }
         }

src/backends/kimchi/prover.rs

@@ -269,7 +269,7 @@ mod tests {
         .unwrap();
 
         let kimchi_vesta = KimchiVesta::new(false);
-        let compiled_circuit = compile(&sources, tast, kimchi_vesta, &mut None)?;
+        let compiled_circuit = compile(&sources, tast, kimchi_vesta, &mut None, false)?;
 
         let (prover_index, _) = compiled_circuit.compile_to_indexes().unwrap();
 

src/backends/mod.rs

@@ -362,6 +362,7 @@ pub trait Backend: Clone {
         &mut self,
         public_output: Option<Var<Self::Field, Self::Var>>,
         returned_cells: Option<Vec<Self::Var>>,
+        disable_safety_check: bool,
     ) -> Result<()>;
 
     /// Generate the witness for a backend.

src/backends/r1cs/arkworks.rs

@@ -91,6 +91,7 @@ pub const WITH_PUBLIC_OUTPUT_ARRAY: &str =
 
 pub fn compile_source_code<BF: BackendField>(
     code: &str,
+    disable_safety_check: bool,
 ) -> Result<CompiledCircuit<R1CS<BF>>, crate::error::Error> {
     let mut sources = Sources::new();
 
@@ -111,7 +112,7 @@ pub fn compile_source_code<BF: BackendField>(
     let mast = mast::monomorphize(tast)?;
     let r1cs = R1CS::<BF>::new();
     // compile
-    CircuitWriter::generate_circuit(mast, r1cs)
+    CircuitWriter::generate_circuit(mast, r1cs, disable_safety_check)
 }
 
 #[cfg(test)]
@@ -124,7 +125,7 @@ mod tests {
 
     #[test]
     fn test_arkworks_cs_is_satisfied() {
-        let compiled_circuit = compile_source_code::<R1csBn254Field>(SIMPLE_ADDITION).unwrap();
+        let compiled_circuit = compile_source_code::<R1csBn254Field>(SIMPLE_ADDITION, false).unwrap();
         let inputs_public = r#"{"public_input": "2"}"#;
         let inputs_private = r#"{"private_input": "2"}"#;
 
@@ -147,7 +148,7 @@ mod tests {
     #[test]
     fn test_arkworks_cs_is_satisfied_array() {
         let compiled_circuit =
-            compile_source_code::<R1csBn254Field>(WITH_PUBLIC_OUTPUT_ARRAY).unwrap();
+            compile_source_code::<R1csBn254Field>(WITH_PUBLIC_OUTPUT_ARRAY, false).unwrap();
         let inputs_public = r#"{"public_input": ["2", "5"]}"#;
         let inputs_private = r#"{"private_input": ["8", "2"]}"#;
 

src/backends/r1cs/mod.rs

@@ -365,6 +365,7 @@ where
         &mut self,
         public_output: Option<crate::var::Var<Self::Field, Self::Var>>,
         returned_cells: Option<Vec<LinearCombination<F>>>,
+        disable_safety_check: bool,
     ) -> crate::error::Result<()> {
         // store the return value in the public input that was created for that
         if let Some(public_output) = public_output {
@@ -404,17 +405,21 @@ where
                     .iter()
                     .find(|private_cell_var| private_cell_var.index == index)
                 {
-                    Err(Error::new(
-                        "constraint-finalization",
-                        ErrorKind::PrivateInputNotUsed,
-                        private_cell_var.span,
-                    ))?
+                    if !disable_safety_check {
+                        Err(Error::new(
+                            "constraint-finalization",
+                            ErrorKind::PrivateInputNotUsed,
+                            private_cell_var.span,
+                        ))?
+                    }
                 } else {
-                    Err(Error::new(
-                        "constraint-finalization",
-                        ErrorKind::UnexpectedError("there's a bug in the circuit_writer, some cellvar does not end up being a cellvar in the circuit!"),
-                        Span::default(),
-                    ))?
+                    if !disable_safety_check {
+                        Err(Error::new(
+                            "constraint-finalization",
+                            ErrorKind::UnexpectedError("there's a bug in the circuit_writer, some cellvar does not end up being a cellvar in the circuit!"),
+                            Span::default(),
+                        ))?
+                    }
                 }
             }
         }

src/circuit_writer/mod.rs

@@ -120,6 +120,7 @@ impl<B: Backend> CircuitWriter<B> {
     pub fn error(&self, kind: ErrorKind, span: Span) -> Error {
         Error::new("constraint-generation", kind, span)
     }
+
 }
 
 impl<B: Backend> CircuitWriter<B> {
@@ -132,7 +133,7 @@ impl<B: Backend> CircuitWriter<B> {
         }
     }
 
-    pub fn generate_circuit(typed: Mast<B>, backend: B) -> Result<CompiledCircuit<B>> {
+    pub fn generate_circuit(typed: Mast<B>, backend: B, disable_safety_check: bool) -> Result<CompiledCircuit<B>> {
         // create circuit writer
         let mut circuit_writer = CircuitWriter::new(typed, backend);
 
@@ -207,7 +208,7 @@ impl<B: Backend> CircuitWriter<B> {
 
         circuit_writer
             .backend
-            .finalize_circuit(public_output, returned_cells)?;
+            .finalize_circuit(public_output, returned_cells, disable_safety_check)?;
 
         //
         Ok(CompiledCircuit::new(circuit_writer))

src/cli/cmd_build_and_check.rs

@@ -71,6 +71,10 @@ pub struct CmdBuild {
     /// Run in server mode to help debug and understand the compiler passes.
     #[clap(long)]
     server_mode: bool,
+
+    /// Do not check that every variable is in a constraint
+    #[arg(long = "disable-safety-check", global = true)]
+    disable_safety_check: bool,
 }
 
 pub fn cmd_build(args: CmdBuild) -> miette::Result<()> {
@@ -88,7 +92,7 @@ pub fn cmd_build(args: CmdBuild) -> miette::Result<()> {
 
     // build
     let (sources, prover_index, verifier_index) =
-        build(&curr_dir, args.asm, args.debug, &mut server_mode)?;
+        build(&curr_dir, args.asm, args.debug, &mut server_mode, args.disable_safety_check)?;
 
     // create COMPILED_DIR
     let compiled_path = curr_dir.join(COMPILED_DIR);
@@ -255,6 +259,7 @@ pub fn build(
     asm: bool,
     debug: bool,
     server_mode: &mut Option<crate::server::ServerShim>,
+    disable_safety_check: bool,
 ) -> miette::Result<(Sources, ProverIndex, VerifierIndex)> {
     // produce all TASTs
     let (sources, tast) = produce_all_asts(curr_dir, server_mode)?;
@@ -263,7 +268,7 @@ pub fn build(
     let double_generic_gate_optimization = false;
 
     let kimchi_vesta = KimchiVesta::new(double_generic_gate_optimization);
-    let compiled_circuit = compile(&sources, tast, kimchi_vesta, server_mode)?;
+    let compiled_circuit = compile(&sources, tast, kimchi_vesta, server_mode, disable_safety_check)?;
 
     if asm {
         println!("{}", compiled_circuit.asm(&sources, debug));
@@ -304,6 +309,10 @@ pub struct CmdTest {
     /// enable the double generic gate optimization of kimchi (by default noname uses that optimization)
     #[clap(long)]
     double: bool,
+
+    /// Do not check that every variable is in a constraint
+    #[arg(long = "disable-safety-check", global = true)]
+    disable_safety_check: bool,
 }
 
 pub fn cmd_test(args: CmdTest) -> miette::Result<()> {
@@ -324,7 +333,7 @@ pub fn cmd_test(args: CmdTest) -> miette::Result<()> {
         BackendKind::KimchiVesta(_) => {
             let (tast, sources) = typecheck_file(&args.path)?;
             let kimchi_vesta = KimchiVesta::new(args.double);
-            let compiled_circuit = compile(&sources, tast, kimchi_vesta, &mut None)?;
+            let compiled_circuit = compile(&sources, tast, kimchi_vesta, &mut None, args.disable_safety_check)?;
 
             let (prover_index, verifier_index) = compiled_circuit.compile_to_indexes()?;
             println!("successfully compiled");
@@ -343,10 +352,10 @@ pub fn cmd_test(args: CmdTest) -> miette::Result<()> {
             println!("proof verified");
         }
         BackendKind::R1csBls12_381(r1cs) => {
-            test_r1cs_backend(r1cs, &args.path, public_inputs, private_inputs, args.debug)?;
+            test_r1cs_backend(r1cs, &args.path, public_inputs, private_inputs, args.debug, args.disable_safety_check)?;
         }
         BackendKind::R1csBn254(r1cs) => {
-            test_r1cs_backend(r1cs, &args.path, public_inputs, private_inputs, args.debug)?;
+            test_r1cs_backend(r1cs, &args.path, public_inputs, private_inputs, args.debug, args.disable_safety_check)?;
         }
     }
 
@@ -371,6 +380,10 @@ pub struct CmdRun {
     /// JSON encoding of the private inputs. Similar to `--public-inputs` but for private inputs.
     #[clap(long, value_parser, default_value = "{}")]
     private_inputs: Option<String>,
+
+    /// Do not check that every variable is in a constraint
+    #[arg(long = "disable-safety-check", global = true)]
+    disable_safety_check: bool,
 }
 
 pub fn cmd_run(args: CmdRun) -> miette::Result<()> {
@@ -396,10 +409,10 @@ pub fn cmd_run(args: CmdRun) -> miette::Result<()> {
             unimplemented!("kimchi-vesta backend is not yet supported for this command")
         }
         BackendKind::R1csBls12_381(r1cs) => {
-            run_r1cs_backend(r1cs, &curr_dir, public_inputs, private_inputs)?
+            run_r1cs_backend(r1cs, &curr_dir, public_inputs, private_inputs, args.disable_safety_check)?
         }
         BackendKind::R1csBn254(r1cs) => {
-            run_r1cs_backend(r1cs, &curr_dir, public_inputs, private_inputs)?
+            run_r1cs_backend(r1cs, &curr_dir, public_inputs, private_inputs, args.disable_safety_check)?
         }
     }
 
@@ -411,14 +424,15 @@ fn run_r1cs_backend<F>(
     curr_dir: &PathBuf,
     public_inputs: JsonInputs,
     private_inputs: JsonInputs,
+    disable_safety_check: bool,
 ) -> miette::Result<()>
 where
     F: BackendField,
 {
     // Assuming `curr_dir`, `public_inputs`, and `private_inputs` are available in the scope
     let (sources, tast) = produce_all_asts(curr_dir, &mut None)?;
 
-    let compiled_circuit = compile(&sources, tast, r1cs, &mut None)?;
+    let compiled_circuit = compile(&sources, tast, r1cs, &mut None, disable_safety_check)?;
 
     let generated_witness =
         generate_witness(&compiled_circuit, &sources, public_inputs, private_inputs)?;
@@ -445,6 +459,7 @@ fn test_r1cs_backend<F: BackendField>(
     public_inputs: JsonInputs,
     private_inputs: JsonInputs,
     debug: bool,
+    disable_safety_check: bool,
 ) -> miette::Result<()>
 where
     F: BackendField,
@@ -471,7 +486,7 @@ where
         &mut None,
     )?;
 
-    let compiled_circuit = compile(&sources, tast, r1cs, &mut None)?;
+    let compiled_circuit = compile(&sources, tast, r1cs, &mut None, disable_safety_check)?;
 
     generate_witness(&compiled_circuit, &sources, public_inputs, private_inputs)?;
 

src/cli/cmd_prove_and_verify.rs

@@ -26,14 +26,18 @@ pub struct CmdProve {
     /// JSON encoding of the private inputs. Similar to `--public-inputs` but for private inputs.
     #[clap(long, value_parser, default_value = "{}")]
     private_inputs: String,
+
+    /// Do not check that every variable is in a constraint
+    #[arg(long = "disable-safety-check", global = true)]
+    disable_safety_check: bool,
 }
 
 pub fn cmd_prove(args: CmdProve) -> miette::Result<()> {
     let curr_dir = args
         .path
         .unwrap_or_else(|| std::env::current_dir().unwrap().try_into().unwrap());
 
-    let (sources, prover_index, verifier_index) = build(&curr_dir, false, args.debug, &mut None)?;
+    let (sources, prover_index, verifier_index) = build(&curr_dir, false, args.debug, &mut None, args.disable_safety_check)?;
 
     // parse inputs
     let public_inputs = parse_inputs(&args.public_inputs).unwrap();
@@ -86,14 +90,18 @@ pub struct CmdVerify {
     /// An optional expected public output, in JSON format.
     #[clap(short, long, value_parser)]
     public_output: Option<String>,
+
+    /// Do not check that every variable is in a constraint
+    #[arg(long = "disable-safety-check", global = true)]
+    disable_safety_check: bool,
 }
 
 pub fn cmd_verify(args: CmdVerify) -> miette::Result<()> {
     let curr_dir = args
         .path
         .unwrap_or_else(|| std::env::current_dir().unwrap().try_into().unwrap());
 
-    let (_sources, _prover_index, verifier_index) = build(&curr_dir, false, false, &mut None)?;
+    let (_sources, _prover_index, verifier_index) = build(&curr_dir, false, false, &mut None, args.disable_safety_check)?;
 
     // parse inputs
     let mut public_inputs = parse_inputs(&args.public_inputs).unwrap();

src/compiler.rs

@@ -203,6 +203,7 @@ pub fn compile<B: Backend>(
     tast: TypeChecker<B>,
     backend: B,
     server_mode: &mut Option<crate::server::ServerShim>,
+    disable_safety_check: bool,
 ) -> miette::Result<CompiledCircuit<B>> {
     // monomorphization pass
     let mast = mast::monomorphize(tast)?;
@@ -221,7 +222,7 @@ pub fn compile<B: Backend>(
     serde_json::to_string(&mast).unwrap();
 
     // synthesizer pass
-    CircuitWriter::generate_circuit(mast, backend).into_miette(sources)
+    CircuitWriter::generate_circuit(mast, backend, disable_safety_check).into_miette(sources)
 }
 
 pub fn generate_witness<B: Backend>(

src/negative_tests.rs

@@ -57,7 +57,7 @@ fn mast_pass(code: &str) -> Result<Mast<R1csBackend>> {
 
 fn synthesizer_pass(code: &str) -> Result<CompiledCircuit<R1csBackend>> {
     let mast = mast_pass(code);
-    CircuitWriter::generate_circuit(mast?, R1CS::new())
+    CircuitWriter::generate_circuit(mast?, R1CS::new(), false)
 }
 
 #[test]