Execution, Gas, Halting
Execution of an AVM program, within a provided execution context, includes the following steps:
- Fetch contract bytecode and decode into a vector of AVM instructions
- Repeat the next step until a halt is reached
- Execute the instruction at the index specified by the context's program counter
- Instruction execution will update the program counter
The following shorthand syntax is used to refer to this execution routine in the "Instruction Set", "Nested execution", and other sections:
execute(context)
Bytecode fetch and decode
Before execution begins, a contract's bytecode is retrieved.
bytecode = context.worldState.contracts[context.environment.address].bytecode
As described in "Contract Deployment", contracts are not stored in a dedicated tree. A contract class is represented as an unencrypted log containing the
ContractClass
structure (which contains the bytecode) and a nullifier representing the class identifier. A contract instance is represented as an unencrypted log containing theContractInstance
structure and a nullifier representing the contract address.
Thus, the syntax used above for bytecode retrieval is shorthand for:
- Perform a membership check of the contract instance address nullifier
- Retrieve the
ContractInstance
from a database that tracks all such unencrypted logscontractInstance = contractInstances[context.environment.address]
- Perform a membership check of the contract class identifier nullifier
- Retrieve the
ContractClass
and its bytecode from a database that tracks all such unencrypted logscontractClass = contractClasses[contractInstance.contract_class_id]
bytecode = contractClass.packed_public_bytecode
The bytecode is then decoded into a vector of instructions
. An instruction is referenced throughout this document according to the following interface:
Member | Description |
---|---|
opcode | The 8-bit opcode value that identifies the operation an instruction is meant to perform. |
indirect | Toggles whether each memory-offset argument is an indirect offset. Rightmost bit corresponds to 0th offset arg, etc. Indirect offsets result in memory accesses like M[M[offset]] instead of the more standard M[offset] . |
inTag | The tag/size to check inputs against and/or tag the destination with. |
args | Named arguments as specified for an instruction in the "Instruction Set". As an example, instr.args.aOffset refers to an instructions argument named aOffset . |
execute | Apply this instruction's transition function to an execution context (e.g. instr.execute(context) ). |
Instruction execution
Once bytecode has been fetched and decoded into the instructions
vector, instruction execution begins.
The AVM executes the instruction at the index specified by the context's program counter.
while (!halted)
instr = instructions[machineState.pc]
instr.execute(context)
An instruction's execution mutates the context's state as specified in the "Instruction Set".
Program Counter and Control Flow
A context is initialized with a program counter of zero, and so instruction execution always begins with a contract's the very first instruction.
The program counter specifies which instruction the AVM will execute next, and each instruction's execution updates the program counter in some way. This allows the AVM to progress to the next instruction at each step.
Most instructions simply increment the program counter by 1. This allows VM execution to flow naturally from instruction to instruction. Some instructions (JUMP
, JUMPI
, INTERNALCALL
) modify the program counter based on arguments.
The INTERNALCALL
instruction pushes machineState.pc+1
to machineState.internalCallStack
and then updates pc
to the instruction's destination argument (instr.args.loc
). The INTERNALRETURN
instruction pops a destination from machineState.internalCallStack
and assigns the result to pc
.
An instruction will never assign program counter a value from memory (
machineState.memory
). AJUMP
,JUMPI
, orINTERNALCALL
instruction's destination is a constant from the program bytecode. This property allows for easier static program analysis.
Gas checks and tracking
See "Gas and Fees" for a deeper dive into Aztec's gas model and for definitions of each type of gas.
Each instruction has an associated l2GasCost
and daGasCost
. The AVM uses these values to enforce that sufficient gas is available before executing an instruction, and to deduct the cost from the context's remaining gas. The process of checking and charging gas is referred to in other sections using the following shorthand:
chargeGas(context, l2GasCost, daGasCost)
Checking gas
Before an instruction is executed, the VM enforces that there is sufficient gas remaining via the following assertions:
assert machineState.l2GasLeft - instr.l2GasCost >= 0
assert machineState.daGasLeft - instr.daGasCost >= 0
Many instructions (like arithmetic operations) have 0
daGasCost
. Instructions only incur a DA cost if they modify the world state or accrued substate.
Charging gas
If these assertions pass, the machine state's gas left is decreased prior to the instruction's core execution:
machineState.l2GasLeft -= instr.l2GasCost
machineState.daGasLeft -= instr.daGasCost
If either of these assertions fail for an instruction, this triggers an exceptional halt. The gas left is set to 0 and execution reverts.
machineState.l2GasLeft = 0
machineState.daGasLeft = 0
Reverting and exceptional halts are covered in more detail in the "Halting" section.
Gas cost notes and examples
An instruction's gas cost is meant to reflect the computational cost of generating a proof of its correct execution. For some instructions, this computational cost changes based on inputs. Here are some examples and important notes:
- All instructions have a base cost.
JUMP
is an example of an instruction with constant gas cost. Regardless of its inputs, the instruction always incurs the samel2GasCost
anddaGasCost
. - The
SET
instruction operates on a different sized constant (based on itsdstTag
). Therefore, this instruction's gas cost increases with the size of its input. - In addition to the base cost, the cost of an instruction increases with the number of reads and writes to memory. This is affected by the total number of input and outputs: the gas cost for
AND
should be greater than that ofNOT
since it takes one more input. - Input parameters flagged as "indirect" require an extra memory access, so these should further increase the gas cost of the instruction.
- The base cost for instructions that operate on a data range of a specified "size" scale in cost with that size, but only if they perform an operation on the data other than copying. For example,
CALLDATACOPY
copiescopySize
words fromenvironment.calldata
tomachineState.memory
, so its increased cost is captured by the extra memory accesses. On the other hand,SSTORE
requires accesses to persistent storage proportional tosrcSize
, so its base cost should also increase. - The
CALL
/STATICCALL
/DELEGATECALL
instruction's gas cost is determined by its*Gas
arguments, but any gas unused by the nested contract call's execution is refunded after its completion (more on this later).
An instruction's gas cost will roughly align with the number of rows it corresponds to in the SNARK execution trace including rows in the sub-operation table, memory table, chiplet tables, etc.
An instruction's gas cost takes into account the costs of associated downstream computations. An instruction that triggers accesses to the public data tree (
SLOAD
/SSTORE
) incurs a cost that accounts for state access validation in later circuits (public kernel or rollup). A contract call instruction (CALL
/STATICCALL
/DELEGATECALL
) incurs a cost accounting for the nested call's complete execution as well as any work required by the public kernel circuit for this additional call.
Halting
A context's execution can end with a normal halt or exceptional halt. A halt ends execution within the current context and returns control flow to the calling context.
Normal halting
A normal halt occurs when the VM encounters an explicit halting instruction (RETURN
or REVERT
). Such instructions consume gas normally and optionally initialize some output data before finally halting the current context's execution.
machineState.l2GasLeft -= instr.l2GasCost
machineState.daGasLeft -= instr.daGasCost
results.reverted = instr.opcode == REVERT
results.output = machineState.memory[instr.args.retOffset:instr.args.retOffset+instr.args.retSize]
Definitions:
retOffset
andretSize
here are arguments to theRETURN
andREVERT
instructions. IfretSize
is 0, the context will have no output. Otherwise, these arguments point to a region of memory to output.
results.output
is only relevant when the caller is a contract call itself. In other words, it is only relevant for nested contract calls. When an initial contract call (initiated by a public execution request) halts normally, itsresults.output
is ignored.
Exceptional halting
An exceptional halt is not explicitly triggered by an instruction but instead occurs when an exceptional condition is met.
When an exceptional halt occurs, the context is flagged as consuming all of its allocated gas and is marked as reverted
with no output data, and then execution within the current context ends.
machineState.l2GasLeft = 0
machineState.daGasLeft = 0
results.reverted = true
// results.output remains empty
The AVM's exceptional halting conditions area listed below:
- Insufficient gas
assert machineState.l2GasLeft - instr.l2GasCost >= 0
assert machineState.daGasLeft - instr.l2GasCost >= 0 - Invalid instruction encountered
assert instructions[machineState.pc].opcode <= MAX_AVM_OPCODE
- Jump destination past end of program
assert instructions[machineState.pc].opcode not in {JUMP, JUMPI, INTERNALCALL}
OR instr.args.loc < instructions.length - Failed memory tag check
- Defined per-instruction in the Instruction Set
- Out of bounds memory access (max memory offset is )
for offset in instr.args.*Offset:
assert offset < 2^32 - World state modification attempt during a static call
assert !environment.isStaticCall
OR instructions[machineState.pc].opcode not in WS_AS_MODIFYING_OPSDefinition:
WS_AS_MODIFYING_OPS
represents the list of all opcodes corresponding to instructions that modify world state or accrued substate. - Maximum contract call depth (1024) exceeded
assert environment.contractCallDepth <= 1024
assert instructions[machineState.pc].opcode not in {CALL, STATICCALL, DELEGATECALL}
OR environment.contractCallDepth < 1024 - Maximum contract call calls per execution request (1024) exceeded
assert worldStateAccessTrace.contractCalls.length <= 1024
assert instructions[machineState.pc].opcode not in {CALL, STATICCALL, DELEGATECALL}
OR worldStateAccessTrace.contractCalls.length < 1024 - Maximum internal call depth (1024) exceeded
assert machineState.internalCallStack.length <= 1024
assert instructions[machineState.pc].opcode != INTERNALCALL
OR environment.contractCallDepth < 1024 - Maximum world state accesses (1024-per-category) exceeded
assert worldStateAccessTrace.publicStorageReads.length <= 1024
AND worldStateAccessTrace.publicStorageWrites.length <= 1024
AND worldStateAccessTrace.noteHashChecks.length <= 1024
AND worldStateAccessTrace.noteHashes.length <= 1024
AND worldStateAccessTrace.nullifierChecks.length <= 1024
AND worldStateAccessTrace.nullifiers.length <= 1024
AND worldStateAccessTrace.l1ToL2MessageChecks.length <= 1024
AND worldStateAccessTrace.archiveChecks.length <= 1024
// Storage
assert instructions[machineState.pc].opcode != SLOAD
OR worldStateAccessTrace.publicStorageReads.length < 1024
assert instructions[machineState.pc].opcode != SSTORE
OR worldStateAccessTrace.publicStorageWrites.length < 1024
// Note hashes
assert instructions[machineState.pc].opcode != NOTEHASHEXISTS
OR noteHashChecks.length < 1024
assert instructions[machineState.pc].opcode != EMITNOTEHASH
OR noteHashes.length < 1024
// Nullifiers
assert instructions[machineState.pc].opcode != NULLIFIEREXISTS
OR nullifierChecks.length < 1024
assert instructions[machineState.pc].opcode != EMITNULLIFIER
OR nullifiers.length < 1024
// Read L1 to L2 messages
assert instructions[machineState.pc].opcode != L1TOL2MSGEXISTS
OR worldStateAccessTrace.l1ToL2MessagesChecks.length < 1024 - Maximum accrued substate entries (per-category) exceeded
assert accruedSubstate.unencryptedLogs.length <= MAX_UNENCRYPTED_LOGS
AND accruedSubstate.sentL2ToL1Messages.length <= MAX_SENT_L2_TO_L1_MESSAGES
// Unencrypted logs
assert instructions[machineState.pc].opcode != EMITUNENCRYPTEDLOG
OR unencryptedLogs.length < MAX_UNENCRYPTED_LOGS
// Sent L2 to L1 messages
assert instructions[machineState.pc].opcode != SENDL2TOL1MSG
OR sentL2ToL1Messages.length < MAX_SENT_L2_TO_L1_MESSAGESNote that ideally the AVM should limit the total accrued substate entries per-category instead of the entries per-call.