Designing an API for ZK-Snark proof verification in Aiken - Eryx

[GENERAL] Name and surname of main applicant

Agustín Garassino

[GENERAL] Are you delivering this project as an individual or as an entity (whether formally incorporated or not)

Entity (Incorporated)

[GENERAL] Requested funds in ada

200000

[GENERAL] Please specify how many months you expect your project to last (from 2-12 months)

4

[GENERAL] Please indicate if your proposal has been auto-translated into English from another language

No

[GENERAL] Summarize your solution to the problem (200-character limit including spaces)

Simplify zk-dApp development by creating an intuitive API for circuit construction and ZK-Snark proof verification in Aiken, enhancing developer experience and reducing complexity.

[GENERAL] Does your project have any dependencies on other organizations, technical or otherwise?

No

[GENERAL] If YES, please describe what the dependency is and why you believe it is essential for your project’s delivery. If NO, please write “No dependencies.”

No dependencies.

[GENERAL] Will your project’s output/s be fully open source?

Yes

[GENERAL] Please provide here more information on the open source status of your project outputs

The tools will be open source and available on GitHub under the Apache 2.0 license.

[METADATA] Horizons

Developer Tools

[SOLUTION] 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.

[IMPACT] Please define the positive impact your project will have on the wider Cardano community

Aiken is a modern and widely used language for developing smart contracts in Cardano. This proposal aims to give Aiken developers the ability to seamlessly write circuits that can be verified on-chain.

Zero-Knowledge (ZK) smart contracts would benefit the Cardano ecosystem in two important directions:

• Scalability: ZK smart contracts can help scale the Cardano network by offloading computational work off-chain.
• Privacy: ZK smart contracts allow transactions and data to be verified without revealing sensitive information. This is particularly valuable for privacy focused dApps, such as financial transactions or identity verification.

[CAPABILITY & FEASIBILITY] What is your capability to deliver your project with high levels of trust and accountability? How do you intend to validate if your approach is feasible?

Eryx is a worker-owned labor cooperative with over 10 years of experience solving complex problems involving mathematics and software. We are a group of nerdy PhDs with a solid background in math and computer science. Our team has extensive experience in blockchain development, cryptography, and privacy-focused protocols, which gives us the expertise required to successfully deliver the project.

Among other things, we’ve been core contributors to the Lambdaworks library and implemented the CircleSTARKS protocol in GPU alongside with Nethermind. This involved implementing several ZK cryptographic primitives (field operations, polynomial commitment schemes, FRI protocols, FFTs), in different platforms and languages. Furthermore, we implemented a proving system based on the Plonk protocol. During this project we wrote a simple interface to design circuits. It included basic operations and conditionals that made the building blocks for more complex cryptographic primitives.

In relation to this proposal, we recently developed a Plonky2 backend for Aztec's Noir, funded by the Ethereum Foundation. During this project we learned much about DSL compilers and how they interact with proving systems. Also, we extended Plonky2 with several gadgets that were necessary to be fully compatible with Noir code.

[PROJECT MILESTONES] What are the key milestones you need to achieve in order to complete your project successfully?

Research: Compare different options of proving systems and existing libraries in the ecosystem, taking into account their limitations. Select one of these to use as a first verifier. Some of the features we would like to review are proof size, proving and verifying time, popularity, recursion friendly, and support for optimizations such as lookups and range checks.

• Outputs: technical review of the research done.
• Acceptance criteria: the team agrees on an appropriate verifier.
• Evidence of Milestone Completion: the technical documentation will be published.

Circuit library: implement a library for circuit construction in Aiken. This library will be compatible with the chosen verifier. Generate a set of primitives that allow for the creation of basic programs. These would include simple operations such as assert_eq, add, sub, neg, mul and conditionals. Code an example program such as Fibonacci.

• Outputs: an Aiken library to design simple circuits.
• Acceptance criteria: a simple circuit can be verified with the chosen library.
• Evidence of Milestone Completion: the public GitHub repository.

On-chain verification: Once we have a basic circuit, we aim to make the library compatible with the chosen verifier. We will verify a simple program on the testnet.

• Outputs: The ability of verifying the execution of a program with simple circuit constraints.
• Acceptance criteria: a simple circuit (e.g. Fibonacci) can be verified with the chosen verifier.
• Evidence of Milestone Completion: the public GitHub repository.

Gadgets: add a series of gadgets that allow for the creation of more complex programs using advanced cryptographic primitives without the need of implementing them from scratch. At these step we’ll research other tools and look for input from the community to build the most impactful gadgets. These gadgets will provide ready to use high level zk-constraints for hashes, merkle trees, polynomial evaluation and polynomial interpolation among other primitives.

• Outputs: a list of gadgets for cryptographic primitives and their implementation.
• Acceptance criteria: a complex circuit built with the library can be verified on the test net.
• Evidence of Milestone Completion: the public GitHub repository.

Final polishing and documentation: Refactors, extended testing, writing comprehensive documentation and tutorials.

• Outputs:
• Final codebase after optimizations and bug fixes.
• Full documentation for developers, including setup, usage, and contribution guidelines.
• User-friendly setup and usage tutorials.
• Acceptance Criteria:
• The library meets all functional expectations.
• Documentation and tutorials are complete and clear.
• Evidence of Milestone Completion:
• The source code will be publicly available on GitHub.
• Published documentation and tutorials on a documentation platform.

Final Report: 

• Outputs
• Publicly available source-code of the library in GitHub with its documentation.
• A final report describing the project process and outcome.
• A video showcasing the library and its features.
• Acceptance criteria
• The final library can be used to write circuit programs in Aiken and verify them on-chain.
• The final video complies with Catalyst requirements
• The final report complies with Catalyst requirements
• Evidence of milestone completion
• Source-code available in the GitHub repository
• Documentation publicly available
• Final video uploaded to Google drive or similar platform
• Final report uploaded to Google drive or similar platform

[RESOURCES] Who is in the project team and what are their roles?

Sergio Chouhy

• Role: ZK Cryptographer
• Github: https://github.com/schouhy 
• Responsibilities: Sergio has a PhD in math and is a senior applied ZK cryptographer at Eryx. He’s got extensive experience implementing zero-knowledge protocols across different ecosystems both from scratch and also building compatibility tools between established proving systems and libraries.

Agustín Garassino

• Role: ZK Cryptographer
• Github: https://github.com/ajgara 
• Responsibilities: Agustín is a computer scientist, professor at the University Torcuato Di Tella and a senior applied ZK cryptographer at Eryx. He’s got extensive experience implementing zero-knowledge protocols across different ecosystems. 

Carlo Ferrari

• Role: ZK Cryptographer
• Github: https://github.com/carlogf
• Responsibilities: Carlo has a Math phd and works as a applied ZK cryptographer at Eryx. He has experience implementing and optimizing zero-knowledge protocols in a variety of languages.

Agustin Franchella

• Role: Project Manager 
• LinkedIn: https://www.linkedin.com/in/afranchella/
• Responsibilities: Agustin is a Cardano Ambassador and Encoins team member. He has also been a funded proposer in F12. Agustín will be a project manager, leading the development of the project’s documentation and educational resources, ensuring that the solution’s concept, architecture, and potential applications are communicated clearly and effectively. He will collaborate closely with the development team to ensure the accuracy and accessibility of the project's documentation and onboarding materials for users and developers.

The rest of the Eryx team will be available to contribute or advise on this proposal as needed.

[BUDGET & COSTS] Please provide a cost breakdown of the proposed work and resources

Budget Breakdown

FTE = Full-time equivalent

Development: ₳180,000 total

The activities of this item will consider: Aiken Development; Mathematical and cryptographical research; circuit design and integration.

Cardano developer: 0.5 FTE x 4 months = ₳60,000

ZK Cryptographer: 0.5 FTE x 4 months = ₳60,000

ZK Cryptographer: 0.5 FTE x 4 months = ₳60,000

Project Management: ₳20,000

The activities of this item will be: Organize the project execution, create reports and write the documentation, and maintain communication with the community and reviewers.

Project Management: ½ FTE x 4 months = ₳20,000

Total Budget Request: ₳200,000

[VALUE FOR MONEY] How does the cost of the project represent value for money for the Cardano ecosystem?

We decided to focus on spending the expenses of the project in the development hours. In that regard, it is important to note:

• The team consists of 3 developers that will work a total of 60 hours per week in the project for 4 months. 
• The total development hours of the whole team will be approximately 960 hours. If we divide the development hours by the assigned budget (180.000₳ / 960h = 188₳), it results in 188 Ada per hour which according with the current valuation it results in approximately 65 dollars per development hour. 

Development hours: 960 hours

Cost per hour (₳): 188₳

Cost per hour ( at $0.35 * ₳): $65

Developer projected annual salary: 135,200 dollars

The projected annual salary is around $140,000 USD a year per developer. According to https://web3.career/web3-salaries/blockchain-develope is within the range of salaries of developers, these salaries vary from $50,000 to $250,000 with an average of 140,000 up to 200,000k for the web3 developer.