diff --git a/maingate/src/instructions.rs b/maingate/src/instructions.rs index 230e24d2..abf186d8 100644 --- a/maingate/src/instructions.rs +++ b/maingate/src/instructions.rs @@ -330,9 +330,8 @@ pub trait MainGateInstructions: Chip { .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>, @@ -340,23 +339,27 @@ pub trait MainGateInstructions: Chip { c2: &AssignedCondition, ) -> Result, 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: Chip { ctx: &mut RegionCtx<'_, F>, a: &AssignedCondition, b: &AssignedCondition, - ) -> Result<(), Error> { - self.apply( - ctx, - [Term::assigned_to_mul(a), Term::assigned_to_mul(b)], - F::ZERO, - CombinationOptionCommon::OneLinerMul.into(), - )?; - Ok(()) + ) -> Result, 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: diff --git a/maingate/src/main_gate.rs b/maingate/src/main_gate.rs index 0d15fda8..b27700ae 100644 --- a/maingate/src/main_gate.rs +++ b/maingate/src/main_gate.rs @@ -1522,4 +1522,91 @@ mod tests { }; assert_eq!(prover.verify(), Ok(())); } + + #[derive(Default)] + struct TestCircuitLogicOps { + _marker: PhantomData, + } + + impl Circuit for TestCircuitLogicOps { + type Config = TestCircuitConfig; + type FloorPlanner = SimpleFloorPlanner; + #[cfg(feature = "circuit-params")] + type Params = (); + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let main_gate_config = MainGate::::configure(meta); + TestCircuitConfig { main_gate_config } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let main_gate = MainGate:: { + 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:: { + _marker: PhantomData::, + }; + 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(())); + } }