Please describe your proposed solution
There are some on-chain proving systems already in the Cardano Ecosystem (like Groth16, Plonk (1), (2), and Bulletproofs). Yet there’s still a need for an easy way to use them in a smart contract.
In our ideal world, we would code our smart contracts in Aiken with the ability to define “private” or “off-chain” functionality depending on “privacy” settings. This would automatically compile into a set of ZK-circuits and Plutus code, that would allow an off-chain prover to run “private” functions, that would then be verified on-chain. By building appropriate tooling we can hide most of the ZK-jargon under the hood.
There are projects in other ecosystems that are going in this direction with some degree of success. One example is Noir. This DSL allows programmers to code functions with private and public inputs in a syntax similar to rust, and compiles to ACIR (Abstract Circuit Intermediate Representation), allowing different proving backends. Another example is o1js, this programming language is an extension of TypeScript that allows describing circuit constraints in a straightforward fashion inside smart contracts. Another example of DSL that provides provable code is Cairo, although its verifier uses a STARK-based proving system. All these options help developers by abstracting away some of the complexity of writing provable code.
Our final goal is to implement similar solutions in Cardano, that would allow programmers to implement smart contracts with some “off chain” functions.
The spirit of this proposal is to be a first step in that direction. We aim to develop an Aiken library that provides an easy to use API for the construction of ZK-circuits and its verification. Some popular proving systems such as Plonky2 provide this kind of functionality.
The requirements are:
- Ability to focus on business logic instead of proving and verifying logic.
- Easy to use by users without knowledge in ZK.
- Abstract away users from manual circuit optimizations.
- Protocol agnostic: it should be modular and allow compatibility with other proving systems with little effort.
One would think that since the circuit generation happens off-chain it is not necessary to write it in Aiken. Although this is true, our expected user is a smart contract developer, and the idea is that learning another language shouldn’t be a prerequisite to use ZK in the first place.
One important design choice is which proving system to support as a first approach. Some considerations in this regard are:
- It should be based on the current ZK primitives in Plutus V3 (BLS12381).
- It should have support for recursion, e.x., the ability to pass a proof as a private input to an offchain function and verify it inside that function. The ZK primitives in Plutus pose a restriction on this. The curve BLS12381 does not have a curve cycle. This means fast recursion strategies like those in Barretenberg (Aztec), Pickles (Mina) or Halo2 cannot be applied with the ZK primitives available in Plutus.
- Ideally it shouldn't need a trusted setup.
The mechanisms to send transactions and generate the offchain proofs are out of the scope of this proposal, but will be considered in our design choices. As an example, o1js instantiates the smart contract as an object, which you provide to the Tx, and then you can call prove() on said Tx before signing it and sending it. An idea would be integrating MeshJS to easily support the ZK proving counterpart of the on-chain verifiers.