Keelung - A toolkit for fast, private and secure applications

Oct 3, 2022 • Ting-Gian Lua

Hello, Keelung!

We are excited to announce Keelung, a zero-knowledge cryptography development toolkit for fast, private and secure applications. Keelung makes it simple to build zero-knowledge proofs (ZKPs) for your application regardless of the business logic or use case. Zero-knowledge cryptography has a bright future, and we want to make it easy for teams to build and ship.

Problems with zkApp development

zkApps are still young and the tooling ecosystem is immature. Here’s what we noticed when we took a look at the development ecosystem.

Lack of expressivity
Developers battle a low level of abstraction in most languages, requiring developers to have a significant amount of experience in order to avoid common mistakes. In low-level languages, developers need to translate their business logic into circuit level logic - not an easy thing to do. Pushing developers into a new mode of thought makes zkApp development feel uneasy and inaccessible. We aim to change that.

Pre-quantum proving systems
Many teams are getting acquainted with ZK yet few are thinking about the long-term security implications of the proving systems being used. Most other languages target pre-quantum proving systems which means their zk-proofs are vulnerable to attacks by quantum computers. This takes the “zero” out of zero-knowledge. zkApps can’t get left behind in the transition to PQC while the rest of the world does.

Inefficient compilers
Once business logic is translated from a classical program to a format that is zk-friendly (called a circuit), you need to compile the circuit down to the necessary primitives to actually generate the proof. This process is non-trivial and often involves rich computations over large vectors of numbers. There’s been little attention paid to optimizing these computations which leave developers stuck with circuits they can’t run very efficiently.

How Keelung solves these problems

Higher level of abstraction
Keelung defies the tradeoff between speed and abstraction by embedding itself in Haskell. This allows developers to write high-level ZKPs guarded by Haskell’s advanced type system while leveraging Haskell’s mature ecosystem and tooling. Haskell has been long-regarded as being a safe and reliable programming language, allowing developers to write powerful software with extreme confidence.

Flexible ZKPs
Keelung’s modular design allows developers to easily upgrade their ZKPs from pre- to post-quantum. This is implemented as several modular proving systems (both pre- and post-quantum) that your circuit can plug-and-play with. This grants you maximum flexibility with minimal friction for upgrading your zkApp when the time is right.

Cross-chain compatibility
Keelung gives you the flexibility to change the target environment for proof verification. You may use Keelung to deploy applications in any blockchain environment capable of zero-knowledge proof verification.

Fast compilation
Keelung provides extremely fast zero knowledge proof generation. We leverage Haskell’s abstraction power to enable fast compilation of post-quantum cryptographic primitives. This is done by reducing the number of constraints associated with each circuit, drastically reducing the number of rich computations required at compilation time.

Choose from a wide set of available proving systems to make your zkApp compatible for your use case.Choose from a wide set of available proving systems to make your zkApp compatible for your use case.

How does Keelung work?

A Keelung program will go through these stages before becoming a R1CS circuit.

Elaboration and type erasure
During elaboration, sophisticated constructs such as loops and array manipulations are unrolled and expanded into simple and repetitive instructions. Types are then erased because we no longer need to distinguish between concepts like Booleans or numbers afterward.

Rewriting
Complex expressions are replaced with simpler equivalents to reduce the number of constraints generated in the following stage.

Compilation
Statements and expressions are compiled into special constraints. These constraints describe the relationship between inputs and outputs and are essential in creating ZK proofs.

Optimization
The number of constraints significantly impacts the size of the resulting ZK proof. These constraints will go through different optimization passes repeatedly until the number has been reduced to a bare minimum.

Translation
After all these transformations and optimizations, the resulting constraints are not too far from circuits for generating ZK proofs. Constraints are simply translated into an appropriate format to fit the selected proving system’s requirements.

High level design of Keelung's optimized compiler.High level design of Keelung's optimized compiler.

What’s in store?

We’ll be releasing an alpha version of Keelung which will give developers early access to the programming language and compiler. This will be followed by a beta version offering extensive libraries to make it easier to build apps in popular blockchain environments. We’re extremely excited to partner with teams who are interested in building with Keelung. If you’d like to be involved in the alpha or beta versions, please feel free to reach out to us at desk@btq.li. For more information about Keelung, please visit the Keelung website.