As the ZEXE research evolved into the Aleo network, the Provable team has contributed to various formal specifications. And we’re excited to announce that these are now publicly available!
For users and developers seeking more precise information about system behavior, formal specifications provide mathematically precise definitions. These can range from human-readable formalizations to "mechanizable" specifications that can be precisely understood by a computer program.
It’s been essential to establish these specifications, because over the years, the system which is now Aleo underwent more and more changes:
The proof system was upgraded from Groth16 to Varuna, coming with improved flexibility and prover speed.
The virtual machine design was improved to e.g. compose operations efficiently and to add support for operations on public state, marrying the benefits of private and public ledgers.
The consensus algorithm was upgraded to support dynamic validator sets.
All of these components come together whenever you deploy a program or create a transaction with the Leo language: transaction contain client-side generated Varuna proofs, which are processed in the AleoVM by validators after inclusion in consensus.
Let’s take a look at these in more detail!
The Varuna Proof System
How are computations represented in zero knowledge proofs? The Aleo network uses Varuna (specification; Sage Math implementation), which is based on Marlin.
Some notable features of Varuna and Marlin are:
1. They have a universal and updatable structured reference string (SRS) (which of course has already been set up for the Aleo network), yet still have a small proof size.
2. They can take a rank-1 constraint system (R1CS) as input and use holography to preprocess the constraints for efficiency.
3. They have a modular proving pipeline with solid theoretical foundations.
You can read more about Marlin here.
Varuna adds many optimizations on top of Marlin. One optimization that is particularly notable is the ability to batch multiple circuits and multiple instances together, with a saving on proof size and verifier time over proving the instances separately.
Another innovation in Varuna is the generalization of the input constraints to GR1CS (Generalized Rank-1 Constraint System), formalized in the Garuda and Pari paper.
The AleoVM Virtual Machine
As noted above, the main inspiration behind Aleo's architecture was the ZEXE paper. However, the design left a lot to be desired: large prover costs and communication complexity, complex composability and a lack of on-chain computation.
You can check out the finer details of how these challenges were solved in the latest Aleo VM specification. It includes discussions of challenges, solutions, and rationale for design choices, in addition to a detailed description of the protocols comprising the AleoVM.
The AleoBFT Consensus Algorithm
The Aleo network is a distributed ledger, secured by validators who must reach consensus on the ledger blocks. The consensus algorithm AleoBFT is based on Bullshark and Narwhal, with extensions for dynamic committees with staking. Here is a draft work in progress of a formal specification of AleoBFT.
We have further formalized key features of the AleoBFT specification in the ACL2 theorem prover (documentation; code).
We have formally verified that the consensus algorithm as specified has certain properties including non-forking of blockchains for both static and dynamic stake-weighted committees.
Stay Tuned
Whether you’re a builder, user or just curious, we hope some of these specifications will be helpful. We strive to keep the specifications consistent with the code and appreciate any feedback.