Skip to content

Commit

Permalink
Fix nand and xor instructions (#86)
Browse files Browse the repository at this point in the history
* add: xor, nand tests

* fix nand

* fix xor
  • Loading branch information
davidnevadoc authored Jan 26, 2024
1 parent 8260abc commit 4e8e704
Show file tree
Hide file tree
Showing 2 changed files with 115 additions and 17 deletions.
45 changes: 28 additions & 17 deletions maingate/src/instructions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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:
Expand Down
87 changes: 87 additions & 0 deletions maingate/src/main_gate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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(()));
}
}

0 comments on commit 4e8e704

Please sign in to comment.