Today, I’m going to write an intro to snarkVM or AVM (Aleo virtual machine), which is used in the Aleo network for executing zero-knowledge proof contracts on-chain.
Aleo is a network designed for ZK-proofs and it’s privacy-based, but in this post, we have our focus on snarkVM, AVM, Aleo OP codes, Leo language, and how they work and are designed at a high level. in the future, we go through them in low-level terms too.
1. Functional Paradigm
The snarkVM contracts are mainly written in the Leo programming language. snarkVM uses the functional paradigm instead of Object-oriented, actor model, or resources-oriented which we saw in traditional blockchain runtime environments like TVM, EVM, or MoveVM.
In the functional term, we have something called pure functions which doesn’t change any state of code. that helps to avoid some potential bugs and AVM also has this. for example, transition functions (we go through it soon) can’t change mappings, etc.
2. snarkVM code life-cycle
Your smart contract, written in Leo, has a life-cycle since you write it to when you deploy and call it on-chain.
2.1. The Leo Code
The first shape of your code is Leo programming language, which has a similar syntax to Rust and its compiler is written in rust too. also, it has some similarities to Javascript and Scala.
For example, this is a counter contract from my smart contract collection repository written in Leo:
// The 'counter' program.
// .aleo network ID used.
program counter.aleo {
// makes a map of address to u8.
mapping counter: address => u8;
// increase function can be called from ouside since it's a transition function.
transition increase(num: u8) {
// calling the finalize function of increase, to update the map.
return then finalize(self.caller, num);
}
// only finalize functions can update this map values and they are only callable from transition functions.
finalize increase(public addr: address, public num: u8) {
// getting the value of address or use 0 if there is no record for this address.
let current: u8 = Mapping::get_or_use(counter, addr, 0u8);
// updating the value with provided number.
Mapping::set(counter, addr, num);
}
}Leo contains two different groups of data types: scalar and aggregate types. scalar types are atomic datatypes such as integers and address types, and aggregate types are tuples, arrays, records, and so on.
In another post, I’ll explain Leo, its compiler, and data types in more detail.
2.2. Aleo Instructions
This Leo source code will be compiled to an Aleo Instructions which is kept in a file with the .aleo prefix. they look like this:
program counter.aleo; // defining the program.
mapping counter: // defines a hash map called counter.
key as address.public; // set the key to a address type and it's public.
value as u8.public; // value is 8 byte unsigned integer.
function increase: // define a transition function called increse.
input r0 as u8.private; // get an input as 8 byte unsigned integer and pushing it to register 1.
async increase self.caller r0 into r1; // calling finalize function of increase.
output r1 as counter.aleo/increase.future; // this future means this code block will execute on-chain.
// read about futures and asyncs here: https://developer.aleo.org/aleo/language#futures
finalize increase: // defines the finalize of increase.
input r0 as address.public; // give it's input and push it to r0 register.
input r1 as u8.public; // giving another input.
get.or_use counter[r0] 0u8 into r2; // gives the value of address from hash map or use 0 if not found.
set r1 into counter[r0]; // set new value (input pushed to r1 register) for address value in counter hash map.2.2. AVM OP codes
In the last step, these Instructions will be compiled into AVM Operation codes which are defined here. These OP codes will represented in R1CS format.
3. snrakVM/AVM design
Now, that’s time to talk about the design of snarkVM itself which is cool in the case of private decentralized computing with privacy. snarkVM is designed based on Zexe (Zero-knowledge EXEcution) paper which talks about:
Enabling Decentralized Private Computation.
So, this part is mostly an overview of Zexe design too.
3.1 privacy for a single arbitrary function
As you know we had privacy-based blockchain and projects such as Zerochash, Zcash, Monero, Firo, and so on. They enabled us to use predefined and known functions on blockchain like transferring native coins with privacy. but, what about arbitrary functions?
The AVM will allow us to run private user-defined functions on the blockchain besides known functions. This feature enables privacy DeFi projects such as user-defined assets, private decentralized asset exchanges, and regulation-friendly private stablecoins on Blockchain.
You can find some examples with Leo here.
3.2 Decentralized private computation (DPC)
The ZEXE defines a new concept called e decentralized private computation pr DCP, which allows us to do computation on-chain with privacy, in such a way that the user will do the computation offline and publish the transaction with zero-knowledge proofs to the network.
3.3 Data Structures for DPC
By the way, I had planned to explain the storage and data structure details used in snarkVM implementation itself and how high-level codes such as the Leo program treat and interact with it or what type of storage they can use to keep states in this section, but I found only resources about how ZEXE paper defined some data structure for its purpose which is DPC. I’ll keep the snarkVM and AVM storage details in terms of software design such as whether it’s stack-based or not or it’s registers, etc, for another post; a technical overview of snarkVM.
So, here we talk about the data structures used in ZEXE and snark in terms of on-chain data which can be related to the parts I pointed to above somehow. We have three main data structures called: records, transactions, and ledger.
3.3.1 Records
Records are a unit of data that contains some parameters like death and birth predicate which means when the record is created and when it is consumed, also it contains some arbitrary data and a field that shows when it is committed. also, all records contain a public key which is called the owner that shows the owner of the record. this is the same thing we have in Leo language too:
// token record.
record Token {
owner: address, // owner of the tokens.
balance: u64,
}3.3.2 Transactions
A transaction represent a state change that involved consumption and creation of some records. this transactions mainly contains the serial number of records that they are consuming and the records they are adding or creating. also it caintains a memo/comment which is an arbitrary string from user.
3.3.3 Ledger
The ledger contains the transactions as you know which is an append-only ledger.
Conclusion
That was snarkVM/AVM/ZEXE introduction based on my studies. as I said before I’ll go for a technical overview of snarkVM too in future.
That’s good to mention one of coolest thing in ZEXE/snarkVM for me was that in this model/design is that transactions don’t need to get executed by a node (who keep the ledger) each time to verify it and the computation is done offline and nodes has a cryptographic proof of this state changes and executions and they can verify it.
That was how we reach private decentralized execution, going beyond private stroing and transferring the assets and goods itself.
