Skip to content

Commit

Permalink
docs(yellowpaper): avm tree-access operations (AztecProtocol#4552)
Browse files Browse the repository at this point in the history
  • Loading branch information
dbanks12 authored Feb 13, 2024
1 parent 9dc05bc commit 913f4bd
Show file tree
Hide file tree
Showing 12 changed files with 772 additions and 341 deletions.
26 changes: 15 additions & 11 deletions avm-transpiler/src/opcodes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -60,16 +60,18 @@ pub enum AvmOpcode {
CMOV,

// World State
BLOCKHEADERBYNUMBER,
SLOAD, // Public Storage
SSTORE, // Public Storage
READL1TOL2MSG, // Messages
SENDL2TOL1MSG, // Messages
EMITNOTEHASH, // Notes & Nullifiers
EMITNULLIFIER, // Notes & Nullifiers
SLOAD, // Public Storage
SSTORE, // Public Storage
NOTEHASHEXISTS, // Notes & Nullifiers
EMITNOTEHASH, // Notes & Nullifiers
NULLIFIEREXISTS, // Notes & Nullifiers
EMITNULLIFIER, // Notes & Nullifiers
READL1TOL2MSG, // Messages
HEADERMEMBER, // Archive tree & Headers

// Accrued Substate
EMITUNENCRYPTEDLOG,
SENDL2TOL1MSG,

// Control Flow - Contract Calls
CALL,
Expand Down Expand Up @@ -143,16 +145,18 @@ impl AvmOpcode {
AvmOpcode::CMOV => "CMOV",

// World State
AvmOpcode::BLOCKHEADERBYNUMBER => "BLOCKHEADERBYNUMBER",
AvmOpcode::SLOAD => "SLOAD", // Public Storage
AvmOpcode::SSTORE => "SSTORE", // Public Storage
AvmOpcode::NOTEHASHEXISTS => "NOTEHASHEXISTS", // Notes & Nullifiers
AvmOpcode::EMITNOTEHASH => "EMITNOTEHASH", // Notes & Nullifiers
AvmOpcode::NULLIFIEREXISTS => "NULLIFIEREXISTS", // Notes & Nullifiers
AvmOpcode::EMITNULLIFIER => "EMITNULLIFIER", // Notes & Nullifiers
AvmOpcode::READL1TOL2MSG => "READL1TOL2MSG", // Messages
AvmOpcode::SENDL2TOL1MSG => "SENDL2TOL1MSG", // Messages
AvmOpcode::EMITNOTEHASH => "EMITNOTEHASH", // Notes & Nullifiers
AvmOpcode::EMITNULLIFIER => "EMITNULLIFIER", // Notes & Nullifiers
AvmOpcode::HEADERMEMBER => "HEADERMEMBER", // Archive tree & Headers

// Accrued Substate
AvmOpcode::EMITUNENCRYPTEDLOG => "EMITUNENCRYPTEDLOG",
AvmOpcode::SENDL2TOL1MSG => "SENDL2TOL1MSG",

// Control Flow - Contract Calls
AvmOpcode::CALL => "CALL",
Expand Down
16 changes: 10 additions & 6 deletions barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -66,16 +66,18 @@ const std::unordered_map<OpCode, size_t> Bytecode::OPERANDS_NUM = {
//{ OpCode::CMOV, },

//// World State
//{ OpCode::BLOCKHEADERBYNUMBER, },
//{ OpCode::SLOAD, }, // Public Storage
//{ OpCode::SSTORE, }, // Public Storage
//{ OpCode::READL1TOL2MSG, }, // Messages
//{ OpCode::SENDL2TOL1MSG, }, // Messages
//{ OpCode::NOTEHASHEXISTS, }, // Notes & Nullifiers
//{ OpCode::EMITNOTEHASH, }, // Notes & Nullifiers
//{ OpCode::NULLIFIEREXISTS, }, // Notes & Nullifiers
//{ OpCode::EMITNULLIFIER, }, // Notes & Nullifiers
//{ OpCode::READL1TOL2MSG, }, // Messages
//{ OpCode::HEADERMEMBER, },

//// Accrued Substate
//{ OpCode::EMITUNENCRYPTEDLOG, },
//{ OpCode::SENDL2TOL1MSG, },

//// Control Flow - Contract Calls
//{ OpCode::CALL, },
Expand Down Expand Up @@ -135,14 +137,16 @@ bool Bytecode::has_in_tag(OpCode const op_code)
case OpCode::INTERNALRETURN:
case OpCode::MOV:
case OpCode::CMOV:
case OpCode::BLOCKHEADERBYNUMBER:
case OpCode::SLOAD:
case OpCode::SSTORE:
case OpCode::READL1TOL2MSG:
case OpCode::SENDL2TOL1MSG:
case OpCode::NOTEHASHEXISTS:
case OpCode::EMITNOTEHASH:
case OpCode::NULLIFIEREXISTS:
case OpCode::EMITNULLIFIER:
case OpCode::READL1TOL2MSG:
case OpCode::HEADERMEMBER:
case OpCode::EMITUNENCRYPTEDLOG:
case OpCode::SENDL2TOL1MSG:
case OpCode::CALL:
case OpCode::STATICCALL:
case OpCode::RETURN:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -74,16 +74,18 @@ enum class OpCode : uint8_t {
CMOV,

// World State
BLOCKHEADERBYNUMBER,
SLOAD, // Public Storage
SSTORE, // Public Storage
READL1TOL2MSG, // Messages
SENDL2TOL1MSG, // Messages
EMITNOTEHASH, // Notes & Nullifiers
EMITNULLIFIER, // Notes & Nullifiers
SLOAD, // Public Storage
SSTORE, // Public Storage
NOTEHASHEXISTS, // Notes & Nullifiers
EMITNOTEHASH, // Notes & Nullifiers
NULLIFIEREXISTS, // Notes & Nullifiers
EMITNULLIFIER, // Notes & Nullifiers
READL1TOL2MSG, // Messages
HEADERMEMBER, // Archive tree & Headers

// Accrued Substate
EMITUNENCRYPTEDLOG,
SENDL2TOL1MSG, // Messages

// Control Flow - Contract Calls
CALL,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -80,25 +80,25 @@ const INSTRUCTION_SET = () =>
[FeePerL1Gas.opcode, FeePerL1Gas],
[FeePerL2Gas.opcode, FeePerL2Gas],
[FeePerDAGas.opcode, FeePerDAGas],
// [Contractcalldepth.opcode, Contractcalldepth],
//[Contractcalldepth.opcode, Contractcalldepth],
// Execution Environment - Globals
[ChainId.opcode, ChainId],
[Version.opcode, Version],
[BlockNumber.opcode, BlockNumber],
[Timestamp.opcode, Timestamp],
// [Coinbase.opcode, Coinbase],
// [Blockl1gaslimit.opcode, Blockl1gaslimit],
// [Blockl2gaslimit.opcode, Blockl2gaslimit],
// [Blockdagaslimit.opcode, Blockdagaslimit],
// // Execution Environment - Calldata
//[Coinbase.opcode, Coinbase],
//[Blockl1gaslimit.opcode, Blockl1gaslimit],
//[Blockl2gaslimit.opcode, Blockl2gaslimit],
//[Blockdagaslimit.opcode, Blockdagaslimit],
// Execution Environment - Calldata
[CalldataCopy.opcode, CalldataCopy],

// //// Machine State
// // Machine State - Gas
// //[L1gasleft.opcode, L1gasleft],
// //[L2gasleft.opcode, L2gasleft],
// //[Dagasleft.opcode, Dagasleft],
// //// Machine State - Internal Control Flow
// Machine State
// Machine State - Gas
//[L1gasleft.opcode, L1gasleft],
//[L2gasleft.opcode, L2gasleft],
//[Dagasleft.opcode, Dagasleft],
// Machine State - Internal Control Flow
[Jump.opcode, Jump],
[JumpI.opcode, JumpI],
[InternalCall.opcode, InternalCall],
Expand All @@ -107,27 +107,29 @@ const INSTRUCTION_SET = () =>
[Mov.opcode, Mov],
[CMov.opcode, CMov],

// //// World State
// //[Blockheaderbynumber.opcode, Blockheaderbynumber],
// World State
[SLoad.opcode, SLoad], // Public Storage
[SStore.opcode, SStore], // Public Storage
// //[Readl1tol2msg.opcode, Readl1tol2msg], // Messages
[SendL2ToL1Message.opcode, SendL2ToL1Message], // Messages
//[NoteHashExists.opcode, NoteHashExists], // Notes & Nullifiers
[EmitNoteHash.opcode, EmitNoteHash], // Notes & Nullifiers
//[NullifierExists.opcode, NullifierExists], // Notes & Nullifiers
[EmitNullifier.opcode, EmitNullifier], // Notes & Nullifiers
//[Readl1tol2msg.opcode, Readl1tol2msg], // Messages
//[HeaderMember.opcode, HeaderMember], // Header

// //// Accrued Substate
// Accrued Substate
[EmitUnencryptedLog.opcode, EmitUnencryptedLog],
[SendL2ToL1Message.opcode, SendL2ToL1Message],

// //// Control Flow - Contract Calls
// Control Flow - Contract Calls
[Call.opcode, Call],
[StaticCall.opcode, StaticCall],
[Return.opcode, Return],
[Revert.opcode, Revert],

// //// Gadgets
// //[Keccak.opcode, Keccak],
// //[Poseidon.opcode, Poseidon],
// Gadgets
//[Keccak.opcode, Keccak],
//[Poseidon.opcode, Poseidon],
]);

interface Serializable {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -49,14 +49,16 @@ export enum Opcode {
SET,
MOV,
CMOV,
BLOCKHEADERBYNUMBER,
SLOAD, // Public Storage
SSTORE, // Public Storage
READL1TOL2MSG, // Messages
SENDL2TOL1MSG, // Messages
EMITNOTEHASH, // Notes & Nullifiers
EMITNULLIFIER, // Notes & Nullifiers
SLOAD,
SSTORE,
NOTEHASHEXISTS,
EMITNOTEHASH,
NULLIFIEREXISTS,
EMITNULLIFIER,
READL1TOL2MSG,
HEADERMEMBER,
EMITUNENCRYPTEDLOG,
SENDL2TOL1MSG,
CALL,
STATICCALL,
RETURN,
Expand Down
84 changes: 51 additions & 33 deletions yellow-paper/docs/public-vm/avm.md
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ The entirety of a contract's public code is represented as a single block of byt
Many terms and definitions here are borrowed from the [Ethereum Yellow Paper](https://ethereum.github.io/yellowpaper/paper.pdf).
:::

Initialized by a contract call, an **execution context** includes the information necessary to initiate AVM execution along with all state maintained by the AVM throughout execution:
An **execution context** includes the information and state relevant to a contract call's execution. When a contract call is made, an execution context is initialized as specified in the ["Initial contract calls"](#initial-contract-calls) and ["Nested contract calls"](#nested-contract-calls) sections.

#### _AvmContext_
| Field | Type |
Expand All @@ -62,7 +62,7 @@ Initialized by a contract call, an **execution context** includes the informatio

### Execution Environment

A context's **execution environment** remains constant throughout the context's execution. When a contract call initializes its execution context, it fully specifies the execution environment.
A context's **execution environment** remains constant throughout a contract call's execution. When a contract call initializes its execution context, it fully specifies the execution environment. This is expanded on in the ["Initial contract calls"](#initial-contract-calls) and ["Nested contract calls"](#nested-contract-calls) sections.

#### _ExecutionEnvironment_
| Field | Type | Description |
Expand All @@ -87,10 +87,10 @@ A context's **execution environment** remains constant throughout the context's
Finally, when a contract call halts, it sets the context's **contract call results** to communicate results to the caller.

#### _ContractCallResults_
| Field | Type | Description |
| --- | --- | --- |
| `reverted` | `boolean` | |
| `output` | `[field; <output-length>]` | |
| Field | Type | Description |
| --- | --- | --- |
| reverted | `boolean` | |
| output | `[field; <output-length>]` | |

## Execution

Expand Down Expand Up @@ -210,9 +210,9 @@ The AVM's exceptional halting conditions area listed below:
1. **World state modification attempt during a static call**
```
assert !environment.isStaticCall
OR environment.bytecode[machineState.pc].opcode not in WS_MODIFYING_OPS
OR environment.bytecode[machineState.pc].opcode not in WS_AS_MODIFYING_OPS
```
> Definition: `WS_MODIFYING_OPS` represents the list of all opcodes corresponding to instructions that modify world state.
> Definition: `WS_AS_MODIFYING_OPS` represents the list of all opcodes corresponding to instructions that modify world state or accrued substate.
1. **Maximum contract call depth (1024) exceeded**
```
assert environment.contractCallDepth <= 1024
Expand All @@ -231,35 +231,57 @@ The AVM's exceptional halting conditions area listed below:
assert environment.bytecode[machineState.pc].opcode != INTERNALCALL
OR environment.contractCallDepth < 1024
```
1. **Maximum world state accesses (1024-per-type) exceeded**
1. **Maximum world state accesses (1024-per-category) exceeded**
```
assert publicStorageAccesses.length <= 1024
AND l1ToL2MessagesReads.length <= 1024
AND newL2ToL1Messages.length <= 1024
AND newNoteHashes.length <= 1024
AND newNullifiers.length <= 1024
assert worldStateAccessTrace.publicStorageReads.length <= 1024
AND worldStateAccessTrace.publicStorageWrites.length <= 1024
AND worldStateAccessTrace.noteHashChecks.length <= 1024
AND worldStateAccessTrace.newNoteHashes.length <= 1024
AND worldStateAccessTrace.nullifierChecks.length <= 1024
AND worldStateAccessTrace.newNullifiers.length <= 1024
AND worldStateAccessTrace.l1ToL2MessageReads.length <= 1024
AND worldStateAccessTrace.archiveChecks.length <= 1024
// Storage
assert environment.bytecode[machineState.pc].opcode not in {SLOAD, SSTORE}
OR publicStorageAccesses.length < 1024
// L1 to L2 messages
assert environment.bytecode[machineState.pc].opcode != GETL1TOL2MSG
OR l1ToL2MessagesReads.length < 1024
// L2 to L1 messages
assert environment.bytecode[machineState.pc].opcode != SENDL2TOL1MSG
OR newL2ToL1Messages.length < 1024
assert environment.bytecode[machineState.pc].opcode != SLOAD
OR worldStateAccessTrace.publicStorageReads.length < 1024
assert environment.bytecode[machineState.pc].opcode != SSTORE
OR worldStateAccessTrace.publicStorageWrites.length < 1024
// Note hashes
assert environment.bytecode[machineState.pc].opcode != NOTEHASHEXISTS
OR noteHashChecks.length < 1024
assert environment.bytecode[machineState.pc].opcode != EMITNOTEHASH
OR newNoteHashes.length < 1024
// Nullifiers
assert environment.bytecode[machineState.pc].opcode != NULLIFIEREXISTS
OR nullifierChecks.length < 1024
assert environment.bytecode[machineState.pc].opcode != EMITNULLIFIER
OR newNullifiers.length < 1024
// Read L1 to L2 messages
assert environment.bytecode[machineState.pc].opcode != READL1TOL2MSG
OR worldStateAccessTrace.l1ToL2MessagesReads.length < 1024
// Archive tree & Headers
assert environment.bytecode[machineState.pc].opcode != HEADERMEMBER
OR archiveChecks.length < 1024
```
1. **Maximum accrued substate entries (per-category) exceeded**
```
> Definition: `WS_MODIFYING_OPS` represents the list of all opcodes corresponding to instructions that modify world state.
assert accruedSubstate.unencryptedLogs.length <= MAX_UNENCRYPTED_LOGS
AND accruedSubstate.sentL2ToL1Messages.length <= MAX_SENT_L2_TO_L1_MESSAGES
// Unencrypted logs
assert environment.bytecode[machineState.pc].opcode != ULOG
OR unencryptedLogs.length < MAX_UNENCRYPTED_LOGS
// Sent L2 to L1 messages
assert environment.bytecode[machineState.pc].opcode != SENDL2TOL1MSG
OR sentL2ToL1Messages.length < MAX_SENT_L2_TO_L1_MESSAGES
```
> Note that ideally the AVM should limit the _total_ accrued substate entries per-category instead of the entries per-call.
## Initial contract calls

Expand All @@ -273,8 +295,8 @@ context = AvmContext {
environment = INITIAL_EXECUTION_ENVIRONMENT,
machineState = INITIAL_MACHINE_STATE,
worldState = <latest world state>,
worldStateAccessTrace = { [], [], ... [] } // all trace vectors empty,
accruedSubstate = INITIAL_ACCRUED_SUBSTATE,
worldStateAccessTrace = { [], [], ... [] }, // all trace vectors empty,
accruedSubstate = { [], ... [], }, // all substate vectors empty
results = INITIAL_CONTRACT_CALL_RESULTS,
}
```
Expand Down Expand Up @@ -310,10 +332,6 @@ INITIAL_MACHINE_STATE = MachineState {
memory = [0, ..., 0], // all 2^32 entries are initialized to zero
}
INITIAL_ACCRUED_SUBSTATE = AccruedSubstate {
unencryptedLogs = [], // initialized as empty
}
INITIAL_CONTRACT_CALL_RESULTS = ContractCallResults {
reverted = false,
output = [], // initialized as empty
Expand All @@ -334,7 +352,7 @@ nestedContext = AvmContext {
machineState: nestedMachineState, // defined below
worldState: callingContext.worldState,
worldStateAccessTrace: callingContext.worldStateAccessTrace,
accruedSubstate: INITIAL_ACCRUED_SUBSTATE,
accruedSubstate = { [], ... [], }, // all substate vectors empty
results: INITIAL_CONTRACT_CALL_RESULTS,
}
```
Expand Down Expand Up @@ -425,7 +443,7 @@ if !nestedContext.results.reverted AND instr.opcode != STATICCALL_OP:
Regardless of whether a nested context has reverted, its [world state access trace](./state#world-state-access-trace) updates are absorbed into the calling context along with a new `contractCalls` entry.
```
context.worldStateAccessTrace = nestedContext.worldStateAccessTrace
context.worldStateAccessTrace.contractCalls.append({nestedContext.address, clk})
context.worldStateAccessTrace.contractCalls.append({nestedContext.address, nestedContext.storageAddress, clk})
```

> Reminder: a nested call cannot make updates to the world state or accrued substate if it is a [`STATICCALL`](./instruction-set/#isa-section-staticcall).
Loading

0 comments on commit 913f4bd

Please sign in to comment.