Merge pull request #235 from zksecurity/feat/disable-safety-check-option

Add --disable-safety-check option

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

@@ -335,6 +335,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
@@ -357,7 +358,7 @@ impl Backend for KimchiVesta {
         }
 
         for var in 0..self.next_variable {
-            if !written_vars.contains(&var) {
+            if !written_vars.contains(&var) && !disable_safety_check {
                 if let Some(private_cell_var) = self
                     .private_input_cell_vars
                     .iter()

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

@@ -407,6 +407,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,8 @@ 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"}"#;
 
@@ -148,7 +150,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

@@ -407,6 +407,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 {
@@ -440,7 +441,7 @@ where
                 continue;
             }
 
-            if !written_vars.contains(&index) {
+            if !written_vars.contains(&index) && !disable_safety_check {
                 if let Some(private_cell_var) = self
                     .private_input_cell_vars
                     .iter()

src/circuit_writer/mod.rs

@@ -139,7 +139,11 @@ 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);
 
@@ -212,9 +216,11 @@ impl<B: Backend> CircuitWriter<B> {
             }
         }
 
-        circuit_writer
-            .backend
-            .finalize_circuit(public_output, returned_cells)?;
+        circuit_writer.backend.finalize_circuit(
+            public_output,
+            returned_cells,
+            disable_safety_check,
+        )?;
 
         //
         Ok(CompiledCircuit::new(circuit_writer))

src/cli/cmd_build_and_check.rs

@@ -71,6 +71,11 @@ pub struct CmdBuild {
     /// Run in server mode to help debug and understand the compiler passes.
     #[clap(long)]
     server_mode: bool,
+
+    /// WARNING: This option disables safety checks that ensure each variable is properly constrained.
+    /// 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<()> {
@@ -87,8 +92,13 @@ 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)?;
+    let (sources, prover_index, verifier_index) = 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 +265,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 +274,13 @@ 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 +321,11 @@ pub struct CmdTest {
     /// enable the double generic gate optimization of kimchi (by default noname uses that optimization)
     #[clap(long)]
     double: bool,
+
+    /// WARNING: This option disables safety checks that ensure each variable is properly constrained.
+    /// 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 +346,13 @@ 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 +371,24 @@ 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 +413,11 @@ 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>,
+
+    /// WARNING: This option disables safety checks that ensure each variable is properly constrained.
+    /// 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<()> {
@@ -395,12 +442,20 @@ pub fn cmd_run(args: CmdRun) -> miette::Result<()> {
         BackendKind::KimchiVesta(_) => {
             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)?
-        }
-        BackendKind::R1csBn254(r1cs) => {
-            run_r1cs_backend(r1cs, &curr_dir, public_inputs, private_inputs)?
-        }
+        BackendKind::R1csBls12_381(r1cs) => 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,
+            args.disable_safety_check,
+        )?,
     }
 
     Ok(())
@@ -411,14 +466,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 +501,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 +528,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,25 @@ 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,
+
+    /// WARNING: This option disables safety checks that ensure each variable is properly constrained.
+    /// 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 +97,25 @@ pub struct CmdVerify {
     /// An optional expected public output, in JSON format.
     #[clap(short, long, value_parser)]
     public_output: Option<String>,
+
+    /// WARNING: This option disables safety checks that ensure each variable is properly constrained.
+    /// 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

@@ -210,6 +210,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)?;
@@ -228,7 +229,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]