[SPEC] is_eq gadget

[drewstone]

The basic equation goes like this:

let b = 1 - x * x_inverse;
assert(b * x, 0);

Where:
x is the number we want to check.
x_inverse is the inverse of x (meaning x * x_inverse == 1).
b is the boolean value indicating if x is 0.

Here is the gadget example:

#[derive(Debug, Default)]
struct IsZero<E: PairingEngine> {
	pub x: E::Fr,
	pub x_inv: E::Fr,
}

impl<E: PairingEngine, P: TEModelParameters<BaseField = E::Fr>> Circuit<E, P> for IsZero<E> {
	const CIRCUIT_ID: [u8; 32] = [0xff; 32];

	fn gadget(&mut self, composer: &mut StandardComposer<E, P>) -> Result<(), Error> {
		let x_var = composer.add_input(self.x);
		let x_inv_var = composer.add_input(self.x_inv);
		let one = composer.add_input(E::Fr::one());

		// x * x_inverse
		// -- should be 1 if x != 0
		// -- should be 0 if x == 0
		let res =
			composer.arithmetic_gate(|gate| gate.witness(x_var, x_inv_var, None).mul(E::Fr::one()));

		// b = 1 - x * x_inverse
		// will be 0 if x != 0
		// will be 1 if x == 0
		let b = composer.arithmetic_gate(|gate| {
			gate.witness(one, res, None)
				.add(E::Fr::one(), -E::Fr::one())
		});

		// ensures that x_inv is actually the inverse of x
		let b_check =
			composer.arithmetic_gate(|gate| gate.witness(x_var, b, None).mul(E::Fr::one()));
		composer.assert_equal(b_check, composer.zero_var());

		// If x is 0, b should be 1
		// If x is 1, b should be zero
		composer.assert_equal(b, one);

		Ok(())
	}

	fn padded_circuit_size(&self) -> usize {
		1 << 11
	}
}

The full code can be found here: https://github.com/webb-tools/arkworks-gadgets/blob/filip/iz-zero-gadget/arkworks-plonk-circuits/src/utils.rs

[GhostOfGauss]

Overview

Denoting the input wires as x_A and x_B and the output wire as x_C this gate should enforce x_C = 1 if and only if x_A = x_B and x_C = 0 otherwise. It would be used in conditional statements such as those that come up when proving knowledge of a path in a Merkle tree.

As a Constraint System

It's sufficient to define a gate with one input and one output that is 1 iff input is 0 and output is 0 iff input is non-zero.
The boolean variable b = (x==0) can be checked with that auxiliary variable y as an r1cs system:

x*y + b - 1 = 0
x*b = 0

In the case that x = 0 the first equation implies b=1 and the second equation is satisfied. In the case that x != 0 the second equation forces b=0 and then the first equation forces y to be the multiplicative inverse of x. What's maybe not ideal is that this forces the prover to compute the inverse of x in the case where x is non-zero.

That r1cs system can be written as a composition of gates... [to do]

[lazovicff]

@GhostOfGauss I added a gadget example in the description, although it's not working properly yet.

To avoid having to pass x_inverse into the circuit, it's best to add this change directly into the ark-plonk library, since from the inside you have the access to the values of the variables, so you can calculate the inverse easily. Example: https://github.com/ZK-Garage/plonk/blob/master/src/constraint_system/ecc/curve_addition/variable_base_gate.rs#L166-L172

[GhostOfGauss]

I've added an is-nonzero-gate that outputs a variable whose 0 if its input is 0 and 1 otherwise.  This seems to do the job.  Could you please check here to see what you think? https://github.com/webb-tools/ark-plonk/blob/todd/is-eq-gate/src/constraint_system/boolean.rs

[GhostOfGauss]

I've opened a PR webb-tools/ark-plonk#1

[GhostOfGauss]

PR ZK-Garage/plonk#77 has been merged and resolves this issue.