A survey of ZK Languages
We will go over the DSLs shaping the ZK Space.
A survey of ZK Languages
Intro
Domain-Specific Languages (DSLs) play a crucial role in the realm of zero knowledge proofs (ZK). At their core, ZK tackles the challenge of proving the existence of certain properties in secret data without revealing any additional information. However, transforming high-level ideas into tangible proofs can be intricate. This is where DSLs come into play, bridging abstract concepts and the circuit representation required by proof systems.
Such as a proof system is a method or protocol that allows one party to prove to another party the validity of a statement or claim without revealing any sensitive information. It involves a set of rules and procedures that enable the prover to convince the verifier of the truthfulness of a statement, such as the correctness of computation or the possession of certain knowledge, without revealing any underlying secrets or data.
However, proof systems cannot directly consume high-level ideas from one’s mind. Instead, one must translate these ideas into circuits representing the desired properties. This transition from high-level concepts to circuits presents a challenge. There’s where circuit languages come into play. Circuit languages solve this problem by offering a means to express high-level ideas in a structured and formal manner.
Over the past decade, there has been a significant surge in the number and diversity of circuit languages. The development of numerous circuit languages, such as Noir, Cairo, Leo, and Zinc, has demonstrated vibrant activity in this domain. This proliferation of languages allows one to compare and contrast their features, similarities, and differences. A deeper understanding of the entire circuit language landscape can be gained by examining these languages collectively.
TLDR;
– Noir – developed by Aztec, abstracts away the complexity of cryptography, allowing developers from any background to write ZK circuits.
– SnarkyJS – A TypeScript library by O(1) Labs. Allows developers to write smart contracts. Integrates well with existing JavaScript and TypeScript libraries and tools.
– Circom – designed for ZKP circuit development. Provides precision and clarity, its functionality is primarily focused on this specific domain
– Leo – provides a user-friendly environment for developers. Incorporates a formally verified compiler architecture, focusing on early bug detection and prevention.
– Cairo – emphasizes efficiency and scalability. Supports interoperability through standard interfaces, enabling integration with blockchain platforms, smart contracts, and off-chain systems.
– Zinc – designed for constructing smart contracts and performing generic computation, including producing ZKPs, emphasizing immutability.
– Lurk – addresses the limitations of traditional SNARKs by utilizing Lisp to implement a universal circuit.
Sign up for our quarterly State of ZK report
Glossary
Since we will be covering technical concepts, here’s a glossary with the most complex terms that you may encounter in the following text:
• Abstract Circuit Intermediate Representation (Acer): An intermediate representation of ZK circuits used by Noir, which can be compiled into a rank-one constraint system (R1CS).
• Custom gates: Specialized logical gates designed for efficient and secure execution of cryptographic operations in ZK circuits.
• SHA-256: A cryptographic hash function that takes an input and produces a fixed-size output.
• Pedersen-Merkle checks: Cryptographic verification techniques that enable the validation of data integrity and consistency using Pedersen commitments and Merkle trees.
• Turing completeness: A property of a computational system that can simulate a Turing machine, capable of solving any computable problem given enough time and resources.
• Continuation Passing Style (CPS): A programming technique that breaks down evaluations into manageable steps, enabling uniform and efficient execution.
• Field elements: an element from a finite mathematical field, commonly used in cryptographic schemes and calculations
Noir
Noir is a Domain-Specific Language (DSL) designed by Aztec to facilitate the creation of ZK circuits and ZK programs without requiring extensive knowledge of cryptography or being a cryptographer. Its primary goal is to enable developers from any background to write ZK (zero knowledge) circuits. Noir prioritizes safety, simplicity, and performance. It provides a high-level, rust-like syntax that abstracts cryptographic safety and simplifies the usage of cryptographic primitives while maintaining high performance.
Expanding Possibilities with ZK Proofs
One of the advantages of Noir is its potential to expand the range of applications that can leverage privacy-preserving properties offered by ZK proofs. These proofs enhance privacy and provide efficient verification. Noir compiles down to an intermediate representation called the Abstract Circuit Intermediate Representation (Acer), which can further be compiled into a rank one constraint system (R1CS). This decoupling of the back-end proof system and the language allows Noir to support various proving systems, including Aztec Brettenberg, Turbo Plonk, and potential future integrations such as Groth16 and Halo 2.
Optimizations and Standard Library
Developers can optimize circuits on the proving system layer, leveraging custom gates, a type of specialized logical gates designed for efficient and secure execution of cryptographic operations, enhancing speed, security, and functionality in various applications. and proving system optimizations. The language offers a standard library with optimized functions like SHA-256 and Pedersen-Merkle checks, ryptographic verification techniques that enable the validation of data integrity and consistency using Pedersen commitments and Merkle trees.
Code Organization and Expressiveness
Noir supports code organization through modules and external crates, facilitating the creation of libraries for Noir programs. It offers compound data types such as arrays, tuples, and structs, allowing developers to group data and implement public functions. The language also supports control flow constructs like for loops, if statements, and logical and bitwise operators. Generics and first-class functions are actively being developed, further enhancing the expressiveness of Noir.
Indeed, it’s important to note that Noir is still a work in progress. It may have limitations and potential bugs. The development team is continuously iterating upon the language and aiming for constant improvements.
SnarkyJS
SnarkyJS is a TypeScript library designed by (0)1Labs for writing smart contracts using the Snark programming language. It leverages existing open technologies such as Node.js and the browser, making it accessible and convenient for developers. By building on TypeScript, SnarkyJS allows developers to utilize their existing knowledge of JavaScript and TypeScript libraries and tools.
Integration
SnarkyJS seamlessly integrates with JavaScript and TypeScript libraries and tools, providing developers access to robustness and extensive community support. This integration enhances productivity and reduces the learning curve of adopting a new development environment.
VS Code Support
It provides support for Visual Studio Code (VS Code), a popular code editor. Developers can take advantage of features such as code completion, syntax highlighting, and debugging, enhancing the overall development experience.
Standard Library
SnarkyJS offers a comprehensive standard library that includes essential types such as field elements, un-64, un-32, public key, private key, and signature. These types come with built-in methods, simplifying the handling of cryptographic schemes, optional data, booleans, and elliptic curves.
Circom
Circom, short for Circuit Compiler, is a powerful Domain-Specific Language (DSL) specifically designed for zero knowledge proof (ZKP) circuit development created by Jordi Balyna and the iden3 team.
Expressive Circuit Definition
With its expressive syntax, Circom allows developers to define circuits for ZKP applications with precision and clarity. However, newcomers to Circom and those unfamiliar with DSLs or ZKP concepts may find its syntax and semantics challenging to grasp. It may require additional effort and time for developers who are new to circuit development or have a background in general-purpose programming languages.
Scope Limitations
While Circom excels in ZKP circuit development, it is important to note that its functionality is primarily focused on this specific domain. As a result, developers seeking a more versatile language capable of handling a wide range of computational tasks may find Circom to be restrictive. Complementing Circom with other programming languages or frameworks may be necessary to address broader development requirements.
Tooling and Ecosystem Constraints
Circom is supported by various development tools and has a growing ecosystem, although it may still have relatively limited tooling and resource availability compared to more established programming languages and frameworks. Developers may encounter challenges in finding comprehensive documentation, libraries, and community support for specific use cases or advanced features. This limitation could potentially impact the development speed and community adoption of Circom.
Compatibility Considerations
Circom’s compatibility is primarily centered around popular zero knowledge proof systems like snarkjs and libsnark. While this allows for seamless integration with these systems, it also introduces dependencies on their specific features and constraints. Developers who prefer or require alternative ZKP systems may face compatibility issues or need to invest additional effort in adapting and integrating the circuits generated by Circom into their preferred systems.
Leo
Leo is a programming language specifically designed to facilitate the development of zero knowledge proof-powered applications. It aims to provide a user-friendly environment for developers, particularly those with prior experience in the blockchain ecosystem. With similarities to Rust and some JavaScript-like elements, LEO strives to create familiarity and ease in application development.
One notable feature of Leo is its compiler, which transforms programs into a low-level proof format known as R1CS. What distinguishes Leo’s compiler is the rigorous process of formal verification it undergoes. This verification is essential because bugs can emerge at various stages, including programming, auditing, and compilation. By mathematically ensuring the compiler’s adherence to the programmer’s intent, Leo aims to minimize the risk of bugs going unnoticed or being exploited, particularly in private programs within L2 contexts, ZK-rollups, or LEO’s platform.
Recognizing the inevitability of bugs despite best efforts, the Leo team emphasizes the importance of early bug prevention and detection, particularly in systems handling significant value transfers. To address this concern, Leo’s formally verified compiler architecture instills added confidence, reducing the likelihood of unintended deviations from the intended program behavior.
Beyond the language and compiler, Leo offers a variety of developer experience tools and features. These components are crafted to enhance the development process, streamlining tasks and improving efficiency. Drawing from seven years of experience and observing the growth of the Ethereum ecosystem, the Leo team aims to provide a user-friendly environment akin to the evolution of tools such as explorers, deployment frameworks like Truffle and Ganache, and other resources that simplify application development and testing.
Cairo
Cairo offers a syntax that simplifies the process of constructing ZKP circuits. Drawing inspiration from traditional programming languages, Cairo allows developers to leverage their existing programming skills while designing ZK systems. With its declarative approach, Cairo enables the specification of logical statements and computations, making it easier to represent real-world scenarios in the context of zero knowledge proofs.
Efficiency and Scalability
Performance is a critical factor when it comes to ZK systems. Cairo addresses this concern by focusing on efficiency and scalability. The language incorporates optimization techniques, such as constraint reduction and cycle elimination, to minimize the computational overhead associated with ZKP circuits. By optimizing the circuit design, Cairo enables faster proof generation and verification, making it suitable for applications that require high throughput and low latency.
Interoperability and Integration
Cairo is designed to integrate with existing software infrastructures, enabling developers to combine the power of ZKPs with other technologies. The language supports interoperability through standard interfaces, allowing for integration with blockchain platforms, smart contracts, and off-chain systems. This flexibility opens up possibilities for implementing privacy-enhancing features within decentralized applications, financial systems, and data validation protocols.
Community and Ecosystem
The Cairo project has fostered a community of developers, researchers, and enthusiasts who contribute to its growth. The availability of documentation, tutorials, and sample code facilitates the onboarding process, enabling developers to grasp the concepts and start building ZK systems. Additionally, Cairo benefits from the wider ecosystem of StarkWare, which provides support, tooling, and research advancements to enhance the language and its capabilities.
Zinc
Zinc is a language designed for constructing smart contracts and performing generic computation, including producing zero knowledge proofs. It follows the Rust syntax and borrows elements from Solidity while offering several unique features. The language is fully type-safe, allowing you to define custom types and avoid mixing them up. It also supports type inference, which enhances the syntax and makes it more concise.
One notable feature of Zinc is its emphasis on immutability, making it a functional language by default. A functional language is a programming paradigm that emphasizes using immutable data and evaluating functions as primary constructs.
This design choice reduces side effects and helps create cleaner, less error-prone code, especially for smart contracts. Additionally, Zinc includes safe math operations, ensuring that all operations are secure and preventing potential overflows.
Zinc comes with a packet manager called Zargo, analogous to Rust’s Cargo, providing various options for managing projects, building, testing, and benchmarking. It offers functionality for creating projects consisting of multiple modules and files, generating documentation, and formatting source code. The testing experience in Zinc is particularly robust, surpassing that of Solidity, with a dedicated unit testing framework.
The language has certain restrictions, as it is incomplete and lacks unbounded loops and recursion. However, Zinc addresses the need for effective debugging by introducing console log traces, allowing developers to trace and debug transactions running on testnets or mainnets. This feature simplifies the debugging process, making understanding what went wrong during a transaction easier.
One of the advantages of Zinc is its compatibility with Solidity. It is possible to manually rewrite existing Solidity contracts into Zinc, as the Curve DeFi protocol contracts demonstrate. Additionally, an experimental transpiler called Soul Z enables the automatic conversion of legacy Solidity code into Zinc. While the transpiler lacks support for Turing-complete parts, most DeFi contracts can be easily converted with minimal modifications.
Lurk
Lurk aims to address the limitations of traditional SNARKs and circuits by utilizing Lisp, a functional programming language, to implement a universal circuit. Using Lisp, Lurk introduces a universal function called “eval”, which enables the evaluation of any data expression within the snark circuit.
Code as Data, Data as Code
One of the fundamental principles of Lurk is the concept of representing programs as content-addressable data. This approach allows for efficient evaluation and verification of Lurk programs. The content-addressability simplifies parsing processes, and the resulting data can be directly utilized in the snark prover without requiring a separate compilation step.
Implementing Lisp in a SNARK
To create a universal circuit, Lurk leverages Lisp’s memory allocator called “cons.” This allocator combines two expressions and generates a reference to the resulting expression through hashing. By proving that two expressions hash to the same reference, Lurk can perform computations within the snark circuit.
Continuation Passing Style
Lurk employs a continuation passing style (CPS) to break down evaluations into manageable steps. Each evaluation step becomes a tractable computation, enabling uniform and efficient execution. Including explicit continuations within the SNARK, circuit facilitates the step-wise evaluation process.
Empowering Turing Completeness and Recursion
By adopting Lisp, Lurk achieves Turing completeness and supports unbounded recursion within the snark circuit. This significant capability allows for the proof of complex computations and the implementation of universal circuits capable of executing arbitrary computations.
Implications and Applications
Lurk’s capabilities have wide-ranging implications. With support for unbounded recursion, loops, and conditional control flow, Lurk enables complex computations within a snark circuit. This opens up various applications for verified computations, private data processing, and the execution of Turing-complete programs.
Conclusion
The offer of domain-specific languages (DSLs) is diverse and is expected to continue growing as the use cases of zero-knowledge proofs (ZK) expand across various blockchain ecosystems. Currently, the race to establish the predominant language for building ZK applications is still in its early stages, indicating that we can anticipate further improvements in this field.
However, one common limitation among the majority of DSLs is the absence of a network effect resulting from a large community and robust libraries. Having a thriving community and comprehensive libraries can greatly enhance the developer experience. Although this deficiency may be addressed over time, it is crucial for teams involved in DSL development to prioritize compatibility with other libraries, taking inspiration from the approach employed by SnarkyJS.
By ensuring compatibility with existing libraries, DSLs can tap into the collective knowledge and resources of the wider developer community, enabling easier integration, faster development, and greater flexibility in implementing ZK applications. This collaborative approach will foster the growth of a stronger ecosystem around DSLs, benefiting developers and ultimately advancing the adoption and effectiveness of ZK technology.
