fix: solvable intermediate gates for csat (#433)

Co-authored-by: TomAFrench <tom@tomfren.ch>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>

Cargo.toml

@@ -17,7 +17,6 @@ brillig = { version = "0.20.0", path = "brillig", default-features = false }
 blackbox_solver = { package = "acvm_blackbox_solver", version = "0.20.0", path = "blackbox_solver", default-features = false }
 
 bincode = "1.3.3"
-rmp-serde = "1.1.0"
 
 num-bigint = "0.4"
 num-traits = "0.2"

acir/Cargo.toml

@@ -15,7 +15,7 @@ acir_field.workspace = true
 brillig.workspace = true
 serde.workspace = true
 thiserror.workspace = true
-rmp-serde = { version ="1.1.0", optional = true }
+rmp-serde = { version = "1.1.0", optional = true }
 flate2 = "1.0.24"
 bincode.workspace = true
 

acir/src/circuit/brillig.rs

@@ -5,15 +5,15 @@ use serde::{Deserialize, Serialize};
 
 /// Inputs for the Brillig VM. These are the initial inputs
 /// that the Brillig VM will use to start.
-#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug, Hash)]
+#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug)]
 pub enum BrilligInputs {
     Single(Expression),
     Array(Vec<Expression>),
 }
 
 /// Outputs for the Brillig VM. Once the VM has completed
 /// execution, this will be the object that is returned.
-#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug, Hash)]
+#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Debug)]
 pub enum BrilligOutputs {
     Simple(Witness),
     Array(Vec<Witness>),

acir/src/circuit/mod.rs

@@ -20,6 +20,8 @@ pub struct Circuit {
     pub current_witness_index: u32,
     pub opcodes: Vec<Opcode>,
 
+    /// The set of private inputs to the circuit.
+    pub private_parameters: BTreeSet<Witness>,
     // ACIR distinguishes between the public inputs which are provided externally or calculated within the circuit and returned.
     // The elements of these sets may not be mutually exclusive, i.e. a parameter may be returned from the circuit.
     // All public inputs (parameters and return values) must be provided to the verifier at verification time.
@@ -43,6 +45,11 @@ impl Circuit {
         self.current_witness_index + 1
     }
 
+    /// Returns all witnesses which are required to execute the circuit successfully.
+    pub fn circuit_arguments(&self) -> BTreeSet<Witness> {
+        self.private_parameters.union(&self.public_parameters.0).cloned().collect()
+    }
+
     /// Returns all public inputs. This includes those provided as parameters to the circuit and those
     /// computed as return values.
     pub fn public_inputs(&self) -> PublicInputs {
@@ -178,6 +185,7 @@ mod tests {
         let circuit = Circuit {
             current_witness_index: 5,
             opcodes: vec![and_opcode(), range_opcode(), directive_opcode()],
+            private_parameters: BTreeSet::new(),
             public_parameters: PublicInputs(BTreeSet::from_iter(vec![Witness(2), Witness(12)])),
             return_values: PublicInputs(BTreeSet::from_iter(vec![Witness(4), Witness(12)])),
         };
@@ -206,6 +214,7 @@ mod tests {
                 range_opcode(),
                 and_opcode(),
             ],
+            private_parameters: BTreeSet::new(),
             public_parameters: PublicInputs(BTreeSet::from_iter(vec![Witness(2)])),
             return_values: PublicInputs(BTreeSet::from_iter(vec![Witness(2)])),
         };

acvm/src/compiler/mod.rs

@@ -1,5 +1,8 @@
 use acir::{
-    circuit::{opcodes::UnsupportedMemoryOpcode, Circuit, Opcode, OpcodeLabel},
+    circuit::{
+        brillig::BrilligOutputs, directives::Directive, opcodes::UnsupportedMemoryOpcode, Circuit,
+        Opcode, OpcodeLabel,
+    },
     native_types::{Expression, Witness},
     BlackBoxFunc, FieldElement,
 };
@@ -57,12 +60,18 @@ pub fn compile(
     let range_optimizer = RangeOptimizer::new(acir);
     let (acir, opcode_label) = range_optimizer.replace_redundant_ranges(opcode_label);
 
-    let transformer = match &np_language {
+    let mut transformer = match &np_language {
         crate::Language::R1CS => {
             let transformer = R1CSTransformer::new(acir);
             return Ok((transformer.transform(), opcode_label));
         }
-        crate::Language::PLONKCSat { width } => CSatTransformer::new(*width),
+        crate::Language::PLONKCSat { width } => {
+            let mut csat = CSatTransformer::new(*width);
+            for value in acir.circuit_arguments() {
+                csat.mark_solvable(value);
+            }
+            csat
+        }
     };
 
     // TODO: the code below is only for CSAT transformer
@@ -106,20 +115,114 @@ pub fn compile(
                     transformed_gates.push(Opcode::Arithmetic(gate));
                 }
             }
-            other_gate => {
+            Opcode::BlackBoxFuncCall(func) => {
+                match func {
+                    acir::circuit::opcodes::BlackBoxFuncCall::AND { output, .. }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::XOR { output, .. } => {
+                        transformer.mark_solvable(*output)
+                    }
+                    acir::circuit::opcodes::BlackBoxFuncCall::RANGE { .. } => (),
+                    acir::circuit::opcodes::BlackBoxFuncCall::SHA256 { outputs, .. }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::Keccak256 { outputs, .. }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::Keccak256VariableLength {
+                        outputs,
+                        ..
+                    }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::RecursiveAggregation {
+                        output_aggregation_object: outputs,
+                        ..
+                    }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::Blake2s { outputs, .. } => {
+                        for witness in outputs {
+                            transformer.mark_solvable(*witness);
+                        }
+                    }
+                    acir::circuit::opcodes::BlackBoxFuncCall::FixedBaseScalarMul {
+                        outputs,
+                        ..
+                    }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::Pedersen { outputs, .. } => {
+                        transformer.mark_solvable(outputs.0);
+                        transformer.mark_solvable(outputs.1)
+                    }
+                    acir::circuit::opcodes::BlackBoxFuncCall::HashToField128Security {
+                        output,
+                        ..
+                    }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::EcdsaSecp256k1 { output, .. }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::EcdsaSecp256r1 { output, .. }
+                    | acir::circuit::opcodes::BlackBoxFuncCall::SchnorrVerify { output, .. } => {
+                        transformer.mark_solvable(*output)
+                    }
+                }
+
                 new_opcode_labels.push(opcode_label[index]);
-                transformed_gates.push(other_gate.clone())
+                transformed_gates.push(opcode.clone());
+            }
+            Opcode::Directive(directive) => {
+                match directive {
+                    Directive::Invert { result, .. } => {
+                        transformer.mark_solvable(*result);
+                    }
+                    Directive::Quotient(quotient_directive) => {
+                        transformer.mark_solvable(quotient_directive.q);
+                        transformer.mark_solvable(quotient_directive.r);
+                    }
+                    Directive::ToLeRadix { b, .. } => {
+                        for w in b {
+                            transformer.mark_solvable(*w);
+                        }
+                    }
+                    Directive::PermutationSort { bits, .. } => {
+                        for w in bits {
+                            transformer.mark_solvable(*w);
+                        }
+                    }
+                    Directive::Log(_) => (),
+                }
+                new_opcode_labels.push(opcode_label[index]);
+                transformed_gates.push(opcode.clone());
+            }
+            Opcode::MemoryInit { .. } => {
+                // `MemoryInit` does not write values to the `WitnessMap`
+            }
+            Opcode::MemoryOp { op, .. } => {
+                for (_, w1, w2) in &op.index.mul_terms {
+                    transformer.mark_solvable(*w1);
+                    transformer.mark_solvable(*w2);
+                }
+                for (_, w) in &op.index.linear_combinations {
+                    transformer.mark_solvable(*w);
+                }
+            }
+
+            Opcode::Block(_) | Opcode::ROM(_) | Opcode::RAM(_) => {
+                unimplemented!("Stepwise execution is not compatible with {}", opcode.name())
+            }
+            Opcode::Brillig(brillig) => {
+                for output in &brillig.outputs {
+                    match output {
+                        BrilligOutputs::Simple(w) => transformer.mark_solvable(*w),
+                        BrilligOutputs::Array(v) => {
+                            for w in v {
+                                transformer.mark_solvable(*w);
+                            }
+                        }
+                    }
+                }
+                new_opcode_labels.push(opcode_label[index]);
+                transformed_gates.push(opcode.clone());
             }
         }
     }
 
     let current_witness_index = next_witness_index - 1;
-
     Ok((
         Circuit {
             current_witness_index,
             opcodes: transformed_gates,
             // The optimizer does not add new public inputs
+            private_parameters: acir.private_parameters,
             public_parameters: acir.public_parameters,
             return_values: acir.return_values,
         },

acvm/src/compiler/optimizers/redundant_range.rs

@@ -112,6 +112,7 @@ impl RangeOptimizer {
             Circuit {
                 current_witness_index: self.circuit.current_witness_index,
                 opcodes: optimized_opcodes,
+                private_parameters: self.circuit.private_parameters,
                 public_parameters: self.circuit.public_parameters,
                 return_values: self.circuit.return_values,
             },
@@ -139,6 +140,8 @@ fn extract_range_opcode(opcode: &Opcode) -> Option<(Witness, u32)> {
 
 #[cfg(test)]
 mod tests {
+    use std::collections::BTreeSet;
+
     use crate::compiler::optimizers::redundant_range::{extract_range_opcode, RangeOptimizer};
     use acir::{
         circuit::{
@@ -163,6 +166,7 @@ mod tests {
         Circuit {
             current_witness_index: 1,
             opcodes,
+            private_parameters: BTreeSet::new(),
             public_parameters: PublicInputs::default(),
             return_values: PublicInputs::default(),
         }