Fix nand and xor instructions

maingate/src/instructions.rs

@@ -330,33 +330,36 @@ pub trait MainGateInstructions<F: PrimeField, const WIDTH: usize>: Chip<F> {
             .swap_remove(2))
     }
 
-    /// Assigns new value equal to `1` if `c1 ^ c0 = 1`,
-    /// equal to `0` if `c1 ^ c0 = 0`
-    // `new_assigned_value + 2 * c1 * c2 - c1 - c2 = 0`.
+    /// Returns c0 ^ c1.
+    ///  Enforcing `result + 2 * c1 * c2 - c1 - c2 = 0`.
     fn xor(
         &self,
         ctx: &mut RegionCtx<'_, F>,
         c1: &AssignedCondition<F>,
         c2: &AssignedCondition<F>,
     ) -> Result<AssignedCondition<F>, Error> {
         // Find the new witness
-        let c = c1
+        let result = c1
             .value()
             .zip(c2.value())
             .map(|(c1, c2)| *c1 + *c2 - (F::ONE + F::ONE) * *c1 * *c2);
 
-        Ok(self
+        // The original constraint: `result + 2 * c1 * c2 - c1 - c2 = 0`.
+        // requires scaling the multiplication by 2, but in this implementation
+        // it is easier to scale other terms by 1/2.
+        let result = self
             .apply(
                 ctx,
                 [
-                    Term::assigned_to_sub(c1),
-                    Term::assigned_to_sub(c2),
-                    Term::unassigned_to_add(c),
+                    Term::Assigned(c1, -F::TWO_INV),
+                    Term::Assigned(c2, -F::TWO_INV),
+                    Term::Unassigned(result, F::TWO_INV),
                 ],
                 F::ZERO,
                 CombinationOptionCommon::OneLinerMul.into(),
             )?
-            .swap_remove(2))
+            .swap_remove(2);
+        Ok(result)
     }
 
     /// Assigns new value that is logic inverse of the given assigned value.
@@ -885,14 +888,22 @@ pub trait MainGateInstructions<F: PrimeField, const WIDTH: usize>: Chip<F> {
         ctx: &mut RegionCtx<'_, F>,
         a: &AssignedCondition<F>,
         b: &AssignedCondition<F>,
-    ) -> Result<(), Error> {
-        self.apply(
-            ctx,
-            [Term::assigned_to_mul(a), Term::assigned_to_mul(b)],
-            F::ZERO,
-            CombinationOptionCommon::OneLinerMul.into(),
-        )?;
-        Ok(())
+    ) -> Result<AssignedCondition<F>, Error> {
+        // result + ab - 1 =0
+        let result = a.value().zip(b.value()).map(|(a, b)| F::ONE - *a * b);
+        let result = self
+            .apply(
+                ctx,
+                [
+                    Term::assigned_to_mul(a),
+                    Term::assigned_to_mul(b),
+                    Term::unassigned_to_add(result),
+                ],
+                -F::ONE,
+                CombinationOptionCommon::OneLinerMul.into(),
+            )?
+            .swap_remove(2);
+        Ok(result)
     }
 
     /// Assigns a new witness `r` as:

maingate/src/main_gate.rs

@@ -1522,4 +1522,91 @@ mod tests {
         };
         assert_eq!(prover.verify(), Ok(()));
     }
+
+    #[derive(Default)]
+    struct TestCircuitLogicOps<F: PrimeField> {
+        _marker: PhantomData<F>,
+    }
+
+    impl<F: PrimeField> Circuit<F> for TestCircuitLogicOps<F> {
+        type Config = TestCircuitConfig;
+        type FloorPlanner = SimpleFloorPlanner;
+        #[cfg(feature = "circuit-params")]
+        type Params = ();
+
+        fn without_witnesses(&self) -> Self {
+            Self::default()
+        }
+
+        fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
+            let main_gate_config = MainGate::<F>::configure(meta);
+            TestCircuitConfig { main_gate_config }
+        }
+
+        fn synthesize(
+            &self,
+            config: Self::Config,
+            mut layouter: impl Layouter<F>,
+        ) -> Result<(), Error> {
+            let main_gate = MainGate::<F> {
+                config: config.main_gate_config,
+                _marker: PhantomData,
+            };
+
+            layouter.assign_region(
+                || "region 0",
+                |region| {
+                    let offset = 0;
+                    let ctx = &mut RegionCtx::new(region, offset);
+
+                    let zero = &main_gate.assign_constant(ctx, F::ZERO)?;
+                    let one = &main_gate.assign_constant(ctx, F::ONE)?;
+
+                    let xor_io = [
+                        [zero, zero, zero],
+                        [zero, one, one],
+                        [one, zero, one],
+                        [one, one, zero],
+                    ];
+
+                    let nand_io = [
+                        [zero, zero, one],
+                        [zero, one, one],
+                        [one, zero, one],
+                        [one, one, zero],
+                    ];
+
+                    for io in xor_io.iter() {
+                        let out_xor = main_gate.xor(ctx, io[0], io[1])?;
+                        main_gate.assert_equal(ctx, &out_xor, io[2])?;
+                    }
+
+                    for io in nand_io.iter() {
+                        let out_nand = main_gate.nand(ctx, io[0], io[1])?;
+                        main_gate.assert_equal(ctx, &out_nand, io[2])?;
+                    }
+
+                    Ok(())
+                },
+            )?;
+
+            Ok(())
+        }
+    }
+
+    #[test]
+    fn test_logic_ops() {
+        const K: u32 = 8;
+
+        let circuit = TestCircuitLogicOps::<Fp> {
+            _marker: PhantomData::<Fp>,
+        };
+        let public_inputs = vec![vec![]];
+        let prover = match MockProver::run(K, &circuit, public_inputs) {
+            Ok(prover) => prover,
+            Err(e) => panic!("{:#?}", e),
+        };
+
+        assert_eq!(prover.verify(), Ok(()));
+    }
 }