Wishing to learn more about zero-knowledge proofs (ZKP), I decided this Spring to complete the ZKP MOOC. This course confirmed my interest in this technology. I also participated in the ZKP/Web3 Hackathon with Piergiuseppe Mallozzi. After collaborating to define the architecture of the project, I mainly focused on blockchain integration and implementing the end-to-end proof of concept with a toy circuit. The resulting project, nicknamed Fact Fortress, is available here. It is an on-chain zero-knowledge proof solution to fact-checking that democratizes the use of zero-knowledge proofs to ensure the integrity of private data.
In the context of the MOOC, I already had experienced expressing arithmetic circuits. The task was challenging as I had to use Circom 2, a language with a logic quite different from what developers usually experience. Fortunately, during the hackathon, we employed a different language, Noir, a domain-specific language for creating and verifying proofs, that proved to be easier to use. Indeed, Noir aims to simplify implementing and compiling circuits: “By abstracting away underlying cryptographic complexity while retaining all the power and flexibility of other circuit-building languages, Noir allows any developer–not just those with cryptography knowledge–to construct zk apps. Developers can now focus solely on designing the logic behind private applications.” (Source). Noir compiles circuits into Abstract Circuit Intermediate Representations (ACIR) compatible with different SNARK-based proving systems. For this project, we used the default one: the PLONK SNARK prover Barretenberg.
In this article, I would like to highlight our experience with this language.
Now that the toy circuit was usable, I first generated the verifier smart contract using the Noir command line nargo codegen-verifier. Because the generated smart contract failed to verify valid signatures, I decided, as an alternative approach, to generate it programmatically using the Noir TypeScript library. This time, the smart contract failed to compile because of a stack too deep error, as Noir generates a function referring to a number of variables larger than the EVM stack limit (limited to 16 slots). The issue was fixed by adding block scopes and this technique is now used by Fact Fortress to make the verifier contracts compilable.
A more problematic issue presently affects the Noir smart contracts: the verifying functions only accept the serialized proof as a parameter, which contains public inputs as embedded bytes. In other words, these contracts do not allow to specify the public inputs associated with a proof. An extractor and a public input verifier had to be added in the main smart contract to overcome this issue. Therefore, the main contract performs a pre-check on the public inputs before calling the relevant verifier smart contract with the actual proof. This is a short-term solution, as extractors and public input verifiers have to be implemented for each circuit. Hopefully this limitation of Noir will be addressed in the future.
Last, the Noir TypeScript library uses a WebAssembly (WASM) module, written in Rust, to compile the circuits (it uses a similar approach to generate Grumpkin-based public keys, used by Fact Fortress as a helper for the frontend). Basically, the calling function (from the host, in WebAssembly terminology) provides the path to the circuit definition to the WASM module, which compiles it and returns the compiled circuit to the host. While this technique allows Noir to be theoretically compatible with a variety of languages, it also makes debugging the host harder, as demonstrated by this example, where a runtime error, from the host perspective, is caused by an obscure circuit compilation error, from the module perspective.
We implemented a working solution despite these limitations—expected for an early development language. As part of it, Piergiuseppe additionally implemented a circuit generator that leverages this language. Noir has been tremendously helpful to us in this context and simplified the conception of the process of proving and verifying circuits.