Keelung is a user-friendly toolkit for developing zero-knowledge proofs (ZKPs), featuring a domain-specific language (DSL) embedded in Haskell and a compiler. It simplifies the creation of reliable ZKPs, making advanced cryptography accessible to developers without specialized knowledge.
Keelung integrates Haskell to balance speed and abstraction, enabling developers to utilize Haskell’s advanced type system and robust ecosystem. This facilitates writing high-level zero-knowledge proofs (ZKPs) confidently. Haskell, known for its safety and reliability, aids in creating correct programs at varying levels of abstraction. Keelung’s integration with Haskell not only taps into a dynamic community but also leverages Haskell’s Typeclass feature for a natural syntax and custom datatype definitions.
Keelung’s modular design supports easy upgrades of ZKPs from pre- to post-quantum, a key factor for zkApps' long-term security. It offers several modular proving systems, accommodating both pre- and post-quantum needs. This architecture allows developers to seamlessly update zkApps, maintaining flexibility for future security requirements. Moreover, Keelung's design integrates advancements in zero-knowledge proof systems effortlessly.
Designed with post-quantum security in mind, Keelung provides access to post-quantum proving systems. This ensures that Keelung-generated proofs are resilient against quantum attacks. Developers can create R1CS circuits using Keelung with post-quantum systems, ensuring long-term security for zkApps. This integration prepares zero-knowledge proof technologies for a secure future.
Keelung's versatility shines in its ability to deploy zkApps across various virtual environments capable of zero-knowledge proof verification. This flexibility caters to diverse use cases and requirements, offering developers the liberty to choose their preferred verification environments. It fosters innovation and agility in zkApp development across different ecosystems.
Keelung is engineered for rapid zero-knowledge proof generation, leveraging Haskell’s abstraction capabilities for swift compilation of post-quantum cryptographic primitives. It optimizes by reducing circuit constraints, thereby decreasing computational needs during compilation. This approach results in faster proof generation, enhancing the efficiency and performance of zkApps. Additionally, the reduction in circuit constraints bolsters scalability, equipping Keelung to handle larger, more complex circuits, essential for real-world applications involving numerous participants and intricate computations.
Privacy-preserving Analytics
Perform secure and private data analysis without revealing sensitive information like revenue. Applications include business intelligence, data analytics & ML.
Financial verification
ING Bank uses ZKPs to prove that the incomes of their mortgage applicants are within the admissible range without revealing their exact salary.
Anonymous verifiable voting
Prove voting eligibility without revealing identities. Voters may also request a verifiable proof that their vote was included in the final ballot tally.
Visit our Github repository to discover the latest offerings in Keelung language and the compiler.
Dive into Keelung whitepaper to uncover its distinctive capabilities and benefits.
Read the Keelung documentation to better understand its features and capabilities.
Learn Keelung with a variety of hands-on tutorials and examples.
Explore the standard library for Keelung and learn by doing.
A Keelung program will go through several stages: elaboration, type erasure, rewriting compilation, optimization, and circuit construction. At the end of a successful compilation, an R1CS circuit is generated. These stages are explained in more detail as follows.
Elaboration
Keelung provides developers with a variety of high-level constructs that do not necessarily exist in R1CS. In order to convert these constructs into R1CS, Keelung programs will need to go through an elaboration stage. For example, loops will be unrolled into repetitive instructions, while array manipulations will be resolved into simple variable assignments. Elaboration essentially strips away syntactic sugar, expressing a user program in a much smaller core language that is easier to process in the subsequent stages.
Type Erasure
Like Haskell and other strongly-typed programming languages, Keelung helps developers to write safer programs by distinguishing between concepts like an array of Booleans or numbers. These type distinctions are erased at this stage to reduce overhead in the generated R1CS circuit. This is similar to a vanilla Haskell program: the type system is mostly visible at compile time to provide a strong guarantee of correctness; the information on types is then erased before the binary is generated so the runtime price we need to pay for having the extra safety guarantee is minimal.
Rewriting compilation
Complex expressions are then replaced with simpler equivalents to reduce the size of the resulting ZK circuit. Up until this stage, the whole program is still in the form of a syntax tree, with variables as leaves and operators as internal nodes. This syntax tree will be traversed and broken down into small constraints that describe the relationship between variables in the syntax tree. Take A = (B ∗ C) + (D ∗ E) as an example. Because this expression is too complicated to directly encode into R1CS, it will be compiled into 3 smaller constraints: A = X + Y, X = B ∗ C, and Y = D ∗ E. These constraints will then be used to construct an R1CS circuit (Figure 1).
Optimization
Many of these constraints may be redundant or can be replaced by simpler constraints that express equivalent relationships among the variables. Sometimes we can even eliminate certain variables altogether. Ideally, we would like to remove as many redundant constraints as possible as the number of constraints will significantly impact the size of the resulting ZK circuit. We have designed a set of optimization passes that will remove redundant constraints and simplify the remaining ones. These constraints will go through these optimization passes repeatedly until the number has been reduced to a bare minimum.
Circuit construction
The final stage is to construct an R1CS circuit from the remaining constraints. An R1CS circuit is made of a set of polynomials that describe the relationship between variables, and they are actually not that different from the constraints we have been obtained so far. All we need to do is to convert the constraints into polynomials and arrange them in an appropriate way to fit the selected ZK proving system's requirements.
Advantages over other Zero-Knowledge DSLs
Keelung sets itself apart from other zero-knowledge domain-specific languages (DSLs) by offering several unique features. First, it supports mobile witness and zero-knowledge proof generation, enabling zkApps to run on resource-constrained devices. Second, Keelung has a library of both pre-and post-quantum cryptographic primitives and proving systems, ensuring long-term security and flexibility for developers. Third, Keelung is designed to be developer-friendly, even to non-experts, thanks to its higher level of abstraction and its embedded support in Haskell. Lastly, Keelung is soon to offer tightly coupled hardware acceleration, which will provide even faster and more efficient zero-knowledge proof generation for developers.