Exploring ZK Programming Languages

Zero-Knowledge Proofs (ZKP) are a powerful cryptographic tool that can validate the accuracy of computations while protecting the privacy of input data. Domain-Specific Languages (DSLs) play a crucial role as a part of this key infrastructure, simplifying the development and verification process of ZKP circuits. They act as an important bridge between abstract concepts and the precise circuit representation required by proof systems.

One of the key challenges faced by proof systems is translating abstract high-level concepts into practical circuits. However, the emergence of DSLs has addressed this issue by facilitating the structuring of these abstract concepts in a more concrete and implementable manner, thereby meeting this challenge.

In the past decade, we have witnessed a significant increase in the quantity and diversity of DSLs. This vibrancy in the field is evident in the development of various circuit languages, including Noir, Leo, and Zinc. Whether you need a versatile option like Circom or a customized solution for a specific platform like Cairo, you can choose from numerous languages and frameworks to write ZKP circuits.

In this article, we will explore the main ZK programming languages actively utilized by developers and analyze the best features of each language.

Cairo by StarkWare

Cairo is the core language for general computation programs supporting STARK proofs. It has played a key role in the success of StarkNet and StarkEx, driving the scalability of applications on the Ethereum mainnet. Notably, Cairo has been instrumental in supporting a variety of applications, including dYdX, Sorare, and Immutable X. The name “Cairo” is derived from the abbreviation of “CPU Algebraic Intermediate Representation.” In the realm of zero-knowledge proofs, it functions similarly to an assembly language, enabling developers familiar with low-level programming languages like C, C++, or Solidity to get started more easily.

Inspired by Rust, Cairo empowers developers to create Starknet smart contracts with a focus on security and user-friendly development. Cairo boasts a powerful syntax that simplifies the creation of ZK circuits, allowing users to perform various tasks within Cairo programs. Additionally, one of Cairo’s significant advantages is its scalability, permitting flexible integration of new features and functionalities.

In ZK systems, efficiency and scalability are crucial factors, and Cairo meets these requirements by emphasizing both. The language integrates optimization strategies, including constraint reduction and loop elimination, to alleviate the computational burden typically associated with ZK circuits. The optimization in circuit design results in faster proof generation and verification, making it an ideal choice for applications requiring high throughput and minimal latency.

The expansion and development of Cairo have been remarkable, witnessing an extraordinary surge in the number of full-time developers in the past two years. This surge highlights Cairo’s adaptability, as its use is not limited to blockchain but is significant in any context requiring computational verification. Hence, we can anticipate further significant growth in developers adopting Cairo.

On September 28, 2023, Starknet launched a major upgrade to its programming language with Cairo v2.3.0. This version marks a significant advancement in making contracts more modular by introducing new features, storage options, and event management, enhancing the potential of smart contracts. The integration of these components offers a flexible way to expand contract functionalities, allowing third-party modules to enhance the functionality of contracts.

Zinc by ZkSync

Zinc is a programming language specifically designed for creating smart contracts and SNARK circuits on the zkSync platform. It adopts Rust syntax, integrates elements of Solidity, and offers unique functionalities.

The uniqueness of Zinc lies in its user-friendliness. You can write secure code without needing to delve into all the complex details of the First-Order Constraint System (R1CS). Zinc emphasizes immutability, endowing it with inherent functional characteristics. This means it prioritizes immutable data and function evaluation, thereby reducing side effects and facilitating the writing of cleaner, less error-prone smart contract code.

Moreover, Zinc includes secure mathematical operations to prevent potential overflows, ensuring the safety of all operations. Despite some limitations, such as the absence of infinite loops and recursion, Zinc simplifies the debugging process through console log tracking. These logs make it easier to track and resolve transactional issues on test networks or the main network, thereby enhancing the debugging experience.

Noir By Aztec

Noir, an open-source DSL developed by Aztec and based on Rust, aims to simplify the creation of ZK circuits and ZK programs without requiring in-depth cryptographic knowledge. It is considered one of the most accessible languages for writing ZK applications compatible with any proving system. Noir focuses on security, simplicity, and performance, offering high-level syntax similar to Rust. It abstracts cryptographic security, simplifying the use of cryptographic primitives while maintaining high performance.

Noir has significant advantages in expanding the range of applications that can leverage the privacy protection capabilities offered by ZKP, thereby enhancing privacy and verification efficiency. It compiles into an intermediate representation called Abstract Circuit Intermediate Representation (Acer), which can then be further compiled into R1CS. The separation of the backend proving system from the language itself enables Noir to support various proving systems, including Aztec Brettenberg, Turbo Plonk, and potential future integrations like Groth16 and Halo2.

The language includes a standard library featuring efficient functionalities such as SHA-256 (a cryptographic hash function producing a fixed-size output) and Pedersen-Merkle checks (a cryptographic verification technique using Pedersen commitments and Merkle trees to ensure data integrity and consistency). Noir’s design, akin to Rust, encompasses familiar features for application developers, like functions, submodules, user-defined types (structs), conditional statements, loops, and global constants. Additionally, ongoing efforts are being made to develop generics and first-class functions to further enhance Noir’s expressiveness.

It’s important to note that Noir is still evolving, with potential limitations and bugs. However, the development team is committed to its continuous improvement and optimization.

o1js by 0(1) Labs

o1js, previously known as SnarkyJS, is a TypeScript library developed by 0(1) Labs for creating smart contracts using the SNARK programming language. It fully leverages established technologies such as Node.js and browser compatibility to ensure easy access and convenience for developers.

o1js seamlessly integrates with JavaScript and TypeScript libraries and tools, providing developers with a robust ecosystem and extensive community support. This integration simplifies the development process and reduces the learning curve associated with adopting new development environments. Additionally, it fully supports Visual Studio Code (VS Code), a widely-used code editor, enabling developers to take full advantage of features like code completion, syntax highlighting, and debugging to enhance the development experience.

Essentially, o1js is a multifunctional ZK framework offering key tools required for creating ZK proofs. It supports a diverse range of ZK programs, covering a variety of built-in provable operations such as basic arithmetic, hashing, signing, boolean operations, comparisons, and more. With the o1js framework, you can build zkApps on the Mina Protocol, these smart contracts execute on the client side with private inputs.

Notably, in early September 2023, the 0(1) Labs team announced the transition from SnarkyJS to o1js, emphasizing their commitment to improving performance. Particularly noteworthy is their achievement in reducing the library loading time by 3-4 times, which refers to the time required to import o1js, a process that could block the main thread. For web applications, loading time is crucial for the timing of JavaScript execution and the overall page rendering. Furthermore, the team also updated the Mina zkApp CLI, enhancing the user interface building experience, and announced further improvements to the Archive Node API to enhance its reliability and clarity.

Leo by Aleo

The Aleo blockchain stands out in the field of smart contracts with a strong emphasis on privacy protection. At its core is the Leo programming language, a statically-typed language inspired by Rust. Designed specifically for developing private applications, Leo supports creators who aim to build secure and confidential decentralized ecosystems. What truly sets Leo apart is its pioneering role in introducing a comprehensive toolkit for universal zero-knowledge applications. This toolkit includes a testing framework, package registry, import parser, remote compiler, and theorem generator.

The concept of Leo originates from a development team led by Howard Wu, envisioning a system that empowers developers to build decentralized applications with a priority on privacy and security. Drawing from the principles of Rust, Leo’s design also incorporates elements similar to JavaScript, facilitating a sense of familiarity and ease during the development process. Moreover, Leo aims to accelerate and streamline development by offering an integrated testing platform, package registry, and import converter. This integration allows developers to focus on the core logic of their applications without being bogged down by infrastructural issues.

A notable feature of Leo is its compiler, which transforms programs into the low-level R1CS proof format. The uniqueness of the Leo compiler lies in its rigorous formal verification process. This verification is critical as vulnerabilities can arise at multiple stages, from initial programming to auditing and compiling. By conducting strict mathematical checks to ensure the compiler aligns with the programmer’s intent, Leo aims to minimize the risk of undetected errors or potential vulnerabilities, particularly in L2 contexts, ZK-rollups, or private programs on the Leo platform.

Circom by iden3

Circom, a Domain-Specific Language (DSL) meticulously crafted for ZK circuit development, is a collaborative creation by Jordi Baylina and the iden3 team. The Circom compiler, written in Rust, primarily functions to compile circuits developed using the Circom language. Notably, Circom has emerged as the preferred choice for outstanding ZK applications in the real world, such as Dark Forest and Tornado Cash. Its popularity is attributed to its impressive performance, which includes fast browser proof times through optimized WASM proofs, efficient server-side proofs via rapidsnark, and effective on-chain verification.

However, it’s important to recognize that Circom’s functionality is mainly focused on ZK circuit development, which may render it less suitable for broader computational tasks. Developers seeking more versatile capabilities to meet a wider range of development needs might find Circom’s abilities somewhat limited. In such cases, developers might need to integrate other programming languages or frameworks to fulfill more comprehensive development requirements.

Image Source: Circom

Circom’s compatibility primarily focuses on widely-used Zero-Knowledge Proof (ZKP) systems such as snarkjs and libsnark. This compatibility ensures seamless integration with these commonly used systems, but it also means that Circom circuits inherit specific features and limitations associated with these dependencies. Developers who prefer or need alternative ZKP systems might face compatibility challenges or need to invest extra effort to adapt and integrate circuits generated by Circom into their preferred systems.

Lurk by Lurk Lab

Lurk is a statically-scoped Lisp dialect influenced by Scheme and Common Lisp, with a unique feature: it allows for the direct proof of program execution correctness using zk-SNARKs, enabling compact and efficient verification. The primary uses of Lurk include:

Verifiable Computation: Lurk enables the proof of correctness of its expressions under zero-knowledge conditions, enhancing trust in computation results.

Zero Knowledge: Users can prove knowledge without revealing specific information beyond public inputs, thus protecting privacy.

Content-Addressable Data: Each Lurk program is equipped with a unique content identifier (CID), making it compatible with IPFS and IPLD.

Turing Completeness: Lurk supports the creation and proof of arbitrary computational statements.

Higher-Order Functions: Lurk functions can accept and return other functions, facilitating expressive functional programming.

Computations with Private Data: Lurk allows for handling private data while ensuring provably correct output without privacy leaks.

In building general-purpose circuits, Lurk extensively uses Lisp’s “cons” memory allocator, which combines expressions and generates references through hashing. The key lies in proving that two expressions indeed hash to the same reference. This verification enables Lurk to perform computations within snark circuits.

Lurk’s functionality is rich, including support for infinite recursion, loops, conditional control flow, and multiple backend proof systems like Groth16, SnarkPack+, and Nova. This versatility opens doors to various applications, including verifiable computations, private data handling, and executing Turing-complete programs within snark circuits.

Conclusion

As the diversity of ZK applications grows, the prospects for DSLs in the ZK domain are broad. The key to a DSL’s success lies in establishing a thriving community and a rich library to enrich developers’ experiences. Those DSLs prioritizing compatibility with existing libraries can fully leverage the knowledge and resources of a broader developer community. This approach aids smoother integration, accelerates development, and offers greater flexibility in implementing ZK applications. Such collaborative efforts are crucial in nurturing a more robust ecosystem around DSLs, offering tangible benefits to developers and further driving the adoption and effectiveness of ZK technology.

Disclaimer：

1. This article is reprinted from [panewslab]. All copyrights belong to the original author [ScalingX]. If there are objections to this reprint, please contact the Gate Learn team, and they will handle it promptly.
2. Liability Disclaimer: The views and opinions expressed in this article are solely those of the author and do not constitute any investment advice.
3. Translations of the article into other languages are done by the Gate Learn team. Unless mentioned, copying, distributing, or plagiarizing the translated articles is prohibited.