Field-neq
Formalization and verification of a circuit
for field non-equality.
Given two field elements x and y,
their non-equality is calculated via constraints of the form
If x = y, the first constraint forces z = 0,
and the second constraint disappears;
if x \neq y, the second constraint forces z = 1,
and the fiest constraint becomes w = z / (x - y).
In other words, z is 1 or 0 depending on whether
x and y are non-equal or equal.
Subtopics
- Field-neq-correctness
- Correctness of the circuit.
- Field-neq-spec
- Specification of the circuit.
- Field-neq-circuit
- Construction of the circuit.
- Field-neq-lifting
- Lifting of the circuit to a predicate.
