This repository contains an example of using Reilabs' gnark-lean-extractor library to prove the correctness of a gnark reimplementation of the circuits necessary to implement and operate the Semaphore protocol.
Under the hood, this repository makes heavy use of Reilabs' proven-zk library. It is a lean library to aid in the formal verification of circuits produced by the extractor.
For guidelines on how to build these things for yourself, or to contribute to the repository, see our contributing guide. It also contains a guide to the structure of the repository.
The main lean file contains formulations and accompanying proofs of the following properties for the circuit.
- Poseidon Equivalence: The equivalence of the Poseidon hash implementation to an implementation very closely based on the Poseidon reference implementation.
- No Censorship: A proof, given knowledge of secrets relating to an identity and that the identity commitment being included in the tree, that it is always possible to generate a valid proof.
- No Double Signalling: A proof that any attempt to signal twice using the same identity commitment will result in the equality of the corresponding nullifier hashes.
- No Unauthorized Signalling: A proof that it is not possible to have the circuit accept a proof where the identity commitment generating that proof is not already included in the tree of identity commitments.