Casper ZK Workshop
Inaugural Casper ZK workshop
Introduction
In an effort to focus efforts aimed towards integrating zero-knowledge (ZK) cryptography into various dimensions of the Casper platform, an inaugural exploration workshop was held at the Casper offices in Zug, Switzerland during the week of 23rd January.
In attendance were the following:
- Michal Papierski, Core Protocol Engineer @ Casper Labs
- Morgan Thomas, Applied Cryptographer @ Casper Association
- Jonas Pauli, R&D Intern @ Casper Association
- Mark Greenslade, Head of R&D @ Casper Association
At a high level the agenda, spread over 5 days, was as follows:
- Knowledge Transfer
- Landscape Review
- Coding
The knowledge transfer focused upon the recent work of the participants:
The landscape review focused upon the following themes:
- Virtual Machines
- Layer 2 Scaling via Rollups
- Zero Knowledge Circuit Systems
- Other Projects
The coding work focused upon a mix of the following:
- Integration prototyping of ZK provers with existing execution engine
- ACTUS core in python, typescript, rust & Marlowe
- OSL enhancements & defining type constraints over Casper platform
Knowledge Transfer
Casper Node Execution Engine
Michal began the knowledge transfer session with a deep dive into the Casper node’s execution engine (EE), i.e. the WASM based virtual machine environment within which Casper smart contracts execute.
The EE is a form of black box largely decoupled from the node, i.e. it can be run in a standalone mode outside of the node’s runtime environment. In fact in very early versions of the Casper node software, this decoupling was reinforced by the fact that the node was implemented in Scala and the EE in rust.
The boundary between the EE and it’s host (the component within the node responsible for encapsulating interactions with the EE), was a particular focus of the knowledge transfer discussions. It is quite clear that supporting ZK proving systems will require extending the Casper smart contract runtime API so as to support a wider array of inbuilt cryptographic primitives.
For example, one might imagine extending the API with a set of new hash functions optimized for ZK systems. The reason for this is to optimize gas costs in respect of ZK proof verification. As previous work by Maciej Zielinski illustrates, these costs can be prohibitive.
It is worth noting here that it is imperative to find a software solution to the challenge of optimizing on-chain ZK proof verification costs. Hardware based solutions are out of scope as the Casper node targets general purpose hardware.
Open Specification Language
Open Specification Language (OSL) is a language for writing statements to be proven by ZK-SNARKs. ZK-SNARK theories allow for proving wide classes of statements. They usually require the statement to be proven to be expressed as a constraint system, called an arithmetic circuit, which can take various forms depending on the theory. It is difficult to express complex statements in the form of arithmetic circuits.
OSL is a language of statements which is similar to type theories used in proof engineering, such as Agda and Coq. OSL has a feature set which is sufficiently limited to make it feasible to compile a statement expressed in OSL to an arithmetic circuit which expresses the same statement. This work builds on Σ¹₁ arithmetization in Halo 2, by defining a frontend for a user-friendly circuit compiler.
ACTUS Standard for Financial Contracts
The ACTUS standard defines a taxonomy of real world financial contracts. For each supported financial contract type, the standard mandates the following:
- A set of machine readable terms.
- A set of validation rules to be applied to the terms.
- A set of algorithms to compute payment schedules from valid terms.
For the Casper Association, the ACTUS standard acts as a focalizing use case, an application domain well suited to applying ZK technology within a blockchain setting.
As part of the knowledge transfer the following topics were covered:
- A deep dive into the ACTUS taxonomy.
- An exploration of the technical assets currently available.
- Considerations of how ZK tech could be sensibly utilized.
Landscape Review
Considering the set of constraints under which the Association operates, adopting a synthesis driven approach to R&D is a pragmatic strategy. Such an approach involves performing a landscape review and then reaching out to projects of interest. In an open source environment it is imperative to navigate such a landscape with genuine respect for the behavioral norms of open source collaborations.
As noted in the introduction, the review was constrained to themes of concrete relevance to the application of ZK technology to the Casper platform. For the participants there was a lot to digest.
Virtual Machines
Introduction
At a low level smart contracts are byte-code executing within a virtual machine capable of interpreting the byte-code's format. Within the Casper platform, smart contracts execute within a virtual machine (VM) capable of interpreting WASM byte-code.
VM design, implementation, testing & performance optimization is non-trivial. An order of magnitude of complexity is introduced when one aspires to underpin the VM with a ZK proving system. Such additional complexity is justified by the fact that ZK execution proofs exhibit useful properties.
One such property is that the correctness of the original computation (i.e. smart contract execution) can be subsequently verified without having to rerun the computation. Applied to a blockchain system this enables compute to be moved to the edge rather than having to be applied at each node within the network.
TinyRAM
TinyRAM is a virtual machine with the goal of having a small footprint, low memory usage, a small amount of code, and a small binary. It was deemed a useful project to begin exploring the VM landscape, primarily as it has been previously utilized by Morgan in OSL related work.
TinyRAM is an ISA designed by Ben-Sasson et al., for the purposes of building a zero knowledge VM. It was leveraged as part of OSL related work as it was deemed useful because Halo 2 TinyRAM code is the simplest example (that we know of) of a zk-VM, in terms of code footprint.
Miden VM
Miden VM is a ZK-stark based general purpose virtual machine being incubated by the awesome Polygon Miden team. It is of particular interest due to being a high quality rust based implementation. The underlying ZK tech is provided by the winterfell project, i.e. a ZK STARK prover and verifier for arbitrary computations.
ZK-WASM
ZK WASM is an L2 framework to connect the traditional WASM community (including web, gaming, office, and social applications) with decentralized applications running on the blockchain. It is of particular interest due to not only being a high quality rust based implementation, but the added dimension of WASM support makes it a very good fit for the casper-node execution engine environment. Futhermore the underlying ZK proving system is halo2, thus conveniently synergitic with the OSL related work.
ZK Rollups
Introduction
Building a ZK roll-up is no easy task. Before one can even begin to consider the ZK dimension, one has to consider the usual suspects of any complex distributed transactional system, i.e. data storage, data availability, consensus, transaction formats … etc.
In many ways it is a more complex undertaking than an L1 blockchain. Teams that have successfully rolled out production systems are still relatively few. Furthermore the development time frames are typically multiyear. Having said that, frameworks are coming on-stream that greatly simplify roll-up development.
ZK Sync
ZK Sync is a ZK rollup, a trustless protocol that uses cryptographic validity proofs to provide scalable and low-cost transactions on Ethereum. In zkSync, computation is performed off-chain and most data is stored off-chain as well. As all transactions are proven on the Ethereum mainchain, users enjoy the same security level as in Ethereum. This project was of particular interest due being a live high quality rust based implementation.
StarkNet
StarkNet is a permissionless decentralized Validity-Rollup (referred to as a ZK-Rollup). It operates as an L2 network over Ethereum, enabling any dApp to achieve unlimited scale for its computation — without compromising Ethereum’s composability and security. It went live upon Ethereum in June 2020 and was arguably the first such production ZK rollup environment. It powers several applications such as dYdX, rhino.fi and Canvas.
ZK Circuits
Introduction
In computational complexity theory, arithmetic circuits are the standard model for computing polynomials. Informally, an arithmetic circuit takes as inputs either variables or numbers, and is allowed to either add or multiply two expressions it has already computed. Arithmetic circuits provide a formal way to understand the complexity of computing polynomials. The basic type of question in this line of research is “what is the most efficient way to compute a given polynomial ?
Applying constraint systems over arithmetic circuits lies at the heart of ZK proof creation. Whilst various circuit frameworks currently exist, each one typically comes bundled with a set of “standard” circuits such as comparators, hash functions, digital signatures, binary and decimal convertors. Application custom circuits are built on-top of the “standard” circuits.
Circom
Circom has been incubated by Iden3, a blockchain-based identity management solution including privacy by design with zkSNARKs. It is a novel domain-specific language for defining arithmetic circuits that can be used to generate zero-knowledge proofs. Circom compiler is a circom language compiler written in Rust that can be used to generate a R1CS file with a set of associated constraints and a program (written either in C++ or WebAssembly) to efficiently compute a valid assignment to all wires of the circuit. One of the main particularities of circom is its modularity that allows the programmers to define parameterizable circuits called templates, which can be instantiated to form larger circuits.
Halo 2
Halo 2 is a proving system that combines the Halo recursion technique with an arithmetization based on PLONK, and a polynomial commitment scheme based around the Inner Product Argument. The Halo 2 book details it’s design & implementation as well as providing resources for developers.
Since Halo 2 is written in Rust, you can compile it to WASM, which will allows one to use the prover and verifier for circuits in a wide variety of application contexts. For example one can imagine a game whereby a set of Halo 2 circuits help prove in a ZK sense the correctness of the game play.
Cairo
Cairo was the first production-grade proof system implementing a Turing Complete von Neumann Architecture: each Cairo program P resides in the virtual machine’s memory, alongside the data D processed by it. Cairo comes with a single AIR (and thus a single Verifier — in a smart contract, WebAssembly, etc.) that can verify any Cairo program. Namely, the Cairo AIR verifies the computational integrity of executing P on D, and the correctness of the post-execution state of the system. With Cairo, new business logic doesn’t require a new smart contract, it only requires a different Cairo program. Consequently, the business logic and the proof system are clearly demarcated.
Cairo 1.0 is about to be released and is not just an iteration over Cairo 0. It is a full rewrite in Rust, whereas Cairo 0 has been written in a pythonic DSL. New Cairo at its core is very similar to Rust. It is meant to be backward compatible at the byte-code level.
Other
Modularization of blockchain systems is enabled by ZK technology. Compute and data availability can be decoupled from the core node functions of networking & consensus. Celestia, Anoma and Avail are 3 projects embracing the modularization thesis. In this design space, L1 blockchains become verification layers for compute and data storage activities located at the edge.
Current DEXes are completely transparent: Anyone can see your balances and trade history. Trade privacy means that your trading activity is completely obscured from all third-parties, both before and after a trade is filled. No one except you can learn the details of your balances or trades. Prenumbra and Renegade are excellent examples of private DEXs, that leverages ZK proofs and threshold cryptography. Supporting such applications is imperative for a platform such as Casper.
Summary
Over the course of a pretty intense week, some serious focus went into laying down the foundations for augmenting the Casper platform with ZK technology. In particular we explored how to scale the platform via an L2 optimistic roll-up running arbitrary WASM bytecode in a ZK enabled virtual machine.
The next ZK Workshop will be held once again be in Zug during the week of March 6th. A report will be published in this channel in due course.
