From 913f4bde56c6602b6db6c73c4d6001bca9c46ca4 Mon Sep 17 00:00:00 2001 From: David Banks <47112877+dbanks12@users.noreply.github.com> Date: Tue, 13 Feb 2024 05:53:02 -0500 Subject: [PATCH] docs(yellowpaper): avm tree-access operations (#4552) --- avm-transpiler/src/opcodes.rs | 26 +- .../vm/avm_trace/AvmMini_opcode.cpp | 16 +- .../vm/avm_trace/AvmMini_opcode.hpp | 16 +- .../serialization/bytecode_serialization.ts | 44 +- .../instruction_serialization.ts | 16 +- yellow-paper/docs/public-vm/avm.md | 84 +-- .../docs/public-vm/gen/_InstructionSet.mdx | 521 ++++++++++++------ .../docs/public-vm/instruction-set.mdx | 2 + yellow-paper/docs/public-vm/memory-model.md | 2 +- yellow-paper/docs/public-vm/state.md | 76 +-- yellow-paper/docs/public-vm/type-structs.md | 19 +- .../InstructionSet/InstructionSet.js | 291 ++++++++-- 12 files changed, 772 insertions(+), 341 deletions(-) diff --git a/avm-transpiler/src/opcodes.rs b/avm-transpiler/src/opcodes.rs index cc3c828d2ec..6948aca6239 100644 --- a/avm-transpiler/src/opcodes.rs +++ b/avm-transpiler/src/opcodes.rs @@ -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, @@ -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", diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.cpp index 5ebc445ee9b..01f90c32c3e 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.cpp @@ -66,16 +66,18 @@ const std::unordered_map 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, }, @@ -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: diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.hpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.hpp index 5147239f0d1..634ba203205 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/AvmMini_opcode.hpp @@ -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, diff --git a/yarn-project/simulator/src/avm/serialization/bytecode_serialization.ts b/yarn-project/simulator/src/avm/serialization/bytecode_serialization.ts index 1033cb5f785..756d44e906b 100644 --- a/yarn-project/simulator/src/avm/serialization/bytecode_serialization.ts +++ b/yarn-project/simulator/src/avm/serialization/bytecode_serialization.ts @@ -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], @@ -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 { diff --git a/yarn-project/simulator/src/avm/serialization/instruction_serialization.ts b/yarn-project/simulator/src/avm/serialization/instruction_serialization.ts index 38acdf9bfdd..565fda5a832 100644 --- a/yarn-project/simulator/src/avm/serialization/instruction_serialization.ts +++ b/yarn-project/simulator/src/avm/serialization/instruction_serialization.ts @@ -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, diff --git a/yellow-paper/docs/public-vm/avm.md b/yellow-paper/docs/public-vm/avm.md index 6a955db92db..6227fef9a59 100644 --- a/yellow-paper/docs/public-vm/avm.md +++ b/yellow-paper/docs/public-vm/avm.md @@ -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 | @@ -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 | @@ -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; ]` | | +| Field | Type | Description | +| --- | --- | --- | +| reverted | `boolean` | | +| output | `[field; ]` | | ## Execution @@ -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 @@ -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 @@ -273,8 +295,8 @@ context = AvmContext { environment = INITIAL_EXECUTION_ENVIRONMENT, machineState = INITIAL_MACHINE_STATE, worldState = , - worldStateAccessTrace = { [], [], ... [] } // all trace vectors empty, - accruedSubstate = INITIAL_ACCRUED_SUBSTATE, + worldStateAccessTrace = { [], [], ... [] }, // all trace vectors empty, + accruedSubstate = { [], ... [], }, // all substate vectors empty results = INITIAL_CONTRACT_CALL_RESULTS, } ``` @@ -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 @@ -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, } ``` @@ -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). diff --git a/yellow-paper/docs/public-vm/gen/_InstructionSet.mdx b/yellow-paper/docs/public-vm/gen/_InstructionSet.mdx index 051b43bcf29..cd0ae5e96b9 100644 --- a/yellow-paper/docs/public-vm/gen/_InstructionSet.mdx +++ b/yellow-paper/docs/public-vm/gen/_InstructionSet.mdx @@ -12,11 +12,10 @@ import CodeBlock from '@theme/CodeBlock' Click on an instruction name to jump to its section. - + - @@ -24,7 +23,6 @@ Click on an instruction name to jump to its section. - @@ -32,7 +30,6 @@ Click on an instruction name to jump to its section. - @@ -40,7 +37,6 @@ Click on an instruction name to jump to its section. - @@ -48,7 +44,6 @@ Click on an instruction name to jump to its section. - @@ -56,7 +51,6 @@ Click on an instruction name to jump to its section. - @@ -64,7 +58,6 @@ Click on an instruction name to jump to its section. - @@ -72,7 +65,6 @@ Click on an instruction name to jump to its section. - @@ -80,7 +72,6 @@ Click on an instruction name to jump to its section. - @@ -88,7 +79,6 @@ Click on an instruction name to jump to its section. - @@ -96,7 +86,6 @@ Click on an instruction name to jump to its section. - @@ -104,7 +93,6 @@ Click on an instruction name to jump to its section. - @@ -112,7 +100,6 @@ Click on an instruction name to jump to its section. - @@ -120,7 +107,6 @@ Click on an instruction name to jump to its section. - @@ -128,7 +114,6 @@ Click on an instruction name to jump to its section. - @@ -136,7 +121,6 @@ Click on an instruction name to jump to its section. - @@ -144,7 +128,6 @@ Click on an instruction name to jump to its section. - @@ -152,7 +135,6 @@ Click on an instruction name to jump to its section. - @@ -160,7 +142,6 @@ Click on an instruction name to jump to its section. - @@ -168,7 +149,6 @@ Click on an instruction name to jump to its section. - @@ -176,7 +156,6 @@ Click on an instruction name to jump to its section. - @@ -184,7 +163,6 @@ Click on an instruction name to jump to its section. - @@ -192,7 +170,6 @@ Click on an instruction name to jump to its section. - @@ -200,7 +177,6 @@ Click on an instruction name to jump to its section. - @@ -208,7 +184,6 @@ Click on an instruction name to jump to its section. - @@ -216,7 +191,6 @@ Click on an instruction name to jump to its section. - @@ -224,7 +198,6 @@ Click on an instruction name to jump to its section. - @@ -232,7 +205,6 @@ Click on an instruction name to jump to its section. - @@ -240,7 +212,6 @@ Click on an instruction name to jump to its section. - @@ -248,7 +219,6 @@ Click on an instruction name to jump to its section. - @@ -256,7 +226,6 @@ Click on an instruction name to jump to its section. - @@ -264,7 +233,6 @@ Click on an instruction name to jump to its section. - @@ -272,7 +240,6 @@ Click on an instruction name to jump to its section. - @@ -280,7 +247,6 @@ Click on an instruction name to jump to its section. - @@ -288,7 +254,6 @@ Click on an instruction name to jump to its section. - @@ -296,7 +261,6 @@ Click on an instruction name to jump to its section. - @@ -304,7 +268,6 @@ Click on an instruction name to jump to its section. - @@ -312,7 +275,6 @@ Click on an instruction name to jump to its section. - - @@ -329,7 +290,6 @@ context.machineState.pc = loc`} - @@ -337,7 +297,6 @@ context.machineState.pc = loc`} - @@ -345,79 +304,112 @@ context.machineState.pc = loc`} - - - - - + + + - - - - + + + - - - - + + + - - - - + + + - - - - + + + - - - - + + + - - - - + + + - + + + + + + - - + + + + + + - + - - + - - + - - + -
OpcodeNameSummaryBit-sizeExpressionOpcodeNameSummaryExpression
0x00 [`ADD`](#isa-section-add) Addition (a + b)128 { `M[dstOffset] = M[aOffset] + M[bOffset] mod 2^k` }
0x01 [`SUB`](#isa-section-sub) Subtraction (a - b)128 { `M[dstOffset] = M[aOffset] - M[bOffset] mod 2^k` }
0x02 [`MUL`](#isa-section-mul) Multiplication (a * b)128 { `M[dstOffset] = M[aOffset] * M[bOffset] mod 2^k` }
0x03 [`DIV`](#isa-section-div) Unsigned division (a / b)128 { `M[dstOffset] = M[aOffset] / M[bOffset]` }
0x04 [`EQ`](#isa-section-eq) Equality check (a == b)128 { `M[dstOffset] = M[aOffset] == M[bOffset] ? 1 : 0` }
0x05 [`LT`](#isa-section-lt) Less-than check (a < b)128 { `M[dstOffset] = M[aOffset] < M[bOffset] ? 1 : 0` }
0x06 [`LTE`](#isa-section-lte) Less-than-or-equals check (a <= b)128 { `M[dstOffset] = M[aOffset] <= M[bOffset] ? 1 : 0` }
0x07 [`AND`](#isa-section-and) Bitwise AND (a & b)128 { `M[dstOffset] = M[aOffset] AND M[bOffset]` }
0x08 [`OR`](#isa-section-or) Bitwise OR (a | b)128 { `M[dstOffset] = M[aOffset] OR M[bOffset]` }
0x09 [`XOR`](#isa-section-xor) Bitwise XOR (a ^ b)128 { `M[dstOffset] = M[aOffset] XOR M[bOffset]` }
0x0a [`NOT`](#isa-section-not) Bitwise NOT (inversion)96 { `M[dstOffset] = NOT M[aOffset]` }
0x0b [`SHL`](#isa-section-shl) Bitwise leftward shift (a << b)128 { `M[dstOffset] = M[aOffset] << M[bOffset]` }
0x0c [`SHR`](#isa-section-shr) Bitwise rightward shift (a >> b)128 { `M[dstOffset] = M[aOffset] >> M[bOffset]` }
0x0d [`CAST`](#isa-section-cast) Type cast96 { `M[dstOffset] = cast(M[aOffset])` }
0x0e [`ADDRESS`](#isa-section-address) Get the address of the currently executing l2 contract56 { `M[dstOffset] = context.environment.address` }
0x0f [`STORAGEADDRESS`](#isa-section-storageaddress) Get the _storage_ address of the currently executing context56 { `M[dstOffset] = context.environment.storageAddress` }
0x10 [`ORIGIN`](#isa-section-origin) Get the transaction's origination address56 { `M[dstOffset] = context.environment.origin` }
0x11 [`SENDER`](#isa-section-sender) Get the address of the sender (caller of the current context)56 { `M[dstOffset] = context.environment.sender` }
0x12 [`PORTAL`](#isa-section-portal) Get the address of the l1 portal contract56 { `M[dstOffset] = context.environment.portal` }
0x13 [`FEEPERL1GAS`](#isa-section-feeperl1gas) Get the fee to be paid per "L1 gas" - constant for entire transaction56 { `M[dstOffset] = context.environment.feePerL1Gas` }
0x14 [`FEEPERL2GAS`](#isa-section-feeperl2gas) Get the fee to be paid per "L2 gas" - constant for entire transaction56 { `M[dstOffset] = context.environment.feePerL2Gas` }
0x15 [`FEEPERDAGAS`](#isa-section-feeperdagas) Get the fee to be paid per "DA gas" - constant for entire transaction56 { `M[dstOffset] = context.environment.feePerDaGas` }
0x16 [`CONTRACTCALLDEPTH`](#isa-section-contractcalldepth) Get how many contract calls deep the current call context is56 { `M[dstOffset] = context.environment.contractCallDepth` }
0x17 [`CHAINID`](#isa-section-chainid) Get this rollup's L1 chain ID56 { `M[dstOffset] = context.environment.globals.chainId` }
0x18 [`VERSION`](#isa-section-version) Get this rollup's L2 version ID56 { `M[dstOffset] = context.environment.globals.version` }
0x19 [`BLOCKNUMBER`](#isa-section-blocknumber) Get this L2 block's number56 { `M[dstOffset] = context.environment.globals.blocknumber` }
0x1a [`TIMESTAMP`](#isa-section-timestamp) Get this L2 block's timestamp56 { `M[dstOffset] = context.environment.globals.timestamp` }
0x1b [`COINBASE`](#isa-section-coinbase) Get the block's beneficiary address56 { `M[dstOffset] = context.environment.globals.coinbase` }
0x1c [`BLOCKL1GASLIMIT`](#isa-section-blockl1gaslimit) Total amount of "L1 gas" that a block can consume56 { `M[dstOffset] = context.environment.globals.l1GasLimit` }
0x1d [`BLOCKL2GASLIMIT`](#isa-section-blockl2gaslimit) Total amount of "L2 gas" that a block can consume56 { `M[dstOffset] = context.environment.globals.l2GasLimit` }
0x1e [`BLOCKDAGASLIMIT`](#isa-section-blockdagaslimit) Total amount of "DA gas" that a block can consume56 { `M[dstOffset] = context.environment.globals.daGasLimit` }
0x1f [`CALLDATACOPY`](#isa-section-calldatacopy) Copy calldata into memory120 { `M[dstOffset:dstOffset+copySize] = context.environment.calldata[cdOffset:cdOffset+copySize]` }
0x20 [`L1GASLEFT`](#isa-section-l1gasleft) Remaining "L1 gas" for this call (after this instruction)56 { `M[dstOffset] = context.machineState.l1GasLeft` }
0x21 [`L2GASLEFT`](#isa-section-l2gasleft) Remaining "L2 gas" for this call (after this instruction)56 { `M[dstOffset] = context.MachineState.l2GasLeft` }
0x22 [`DAGASLEFT`](#isa-section-dagasleft) Remaining "DA gas" for this call (after this instruction)56 { `M[dstOffset] = context.machineState.daGasLeft` }
0x23 [`JUMP`](#isa-section-jump) Jump to a location in the bytecode48 { `context.machineState.pc = loc` }
0x24 [`JUMPI`](#isa-section-jumpi) Conditionally jump to a location in the bytecode88 { `context.machineState.pc = M[condOffset] > 0 ? loc : context.machineState.pc` }
0x25 [`INTERNALCALL`](#isa-section-internalcall) Make an internal call. Push the current PC to the internal call stack and jump to the target location.48 {`context.machineState.internalCallStack.push(context.machineState.pc) context.machineState.pc = loc`} @@ -321,7 +283,6 @@ context.machineState.pc = loc`}
0x26 [`INTERNALRETURN`](#isa-section-internalreturn) Return from an internal call. Pop from the internal call stack and jump to the popped location.16 { `context.machineState.pc = context.machineState.internalCallStack.pop()` }
0x27 [`SET`](#isa-section-set) Set a memory word from a constant in the bytecode64+N { `M[dstOffset] = const` }
0x28 [`MOV`](#isa-section-mov) Move a word from source memory location to destination88 { `M[dstOffset] = M[srcOffset]` }
0x29 [`CMOV`](#isa-section-cmov) Move a word (conditionally chosen) from one memory location to another (`d = cond > 0 ? a : b`)152 { `M[dstOffset] = M[condOffset] > 0 ? M[aOffset] : M[bOffset]` }
0x2a [`BLOCKHEADERBYNUM`](#isa-section-blockheaderbynum)Get the block header as of the specified block number88{ - `M[dstOffset:dstOffset+BLOCK_HEADER_LENGTH] = context.worldState.blockHeader[M[blockNumOffset]]` - }0x2a [`SLOAD`](#isa-section-sload)Load a word from this contract's persistent public storage. Zero is loaded for unwritten slots. +{`M[dstOffset] = context.worldState.publicStorage[context.environment.storageAddress][M[slotOffset]]`} +
0x2b [`SLOAD`](#isa-section-sload)Load a word from storage88{ - `M[dstOffset] = context.worldState.publicStorage[context.environment.storageAddress, M[slotOffset]]` - }0x2b [`SSTORE`](#isa-section-sstore)Write a word to this contract's persistent public storage +{`context.worldState.publicStorage[context.environment.storageAddress][M[slotOffset]] = M[srcOffset]`} +
0x2c [`SSTORE`](#isa-section-sstore)Write a word to storage88{ - `context.worldState.publicStorage[context.environment.storageAddress, M[slotOffset]] = M[srcOffset]` - }0x2c [`NOTEHASHEXISTS`](#isa-section-notehashexists)Check whether a note hash exists in the note hash tree (as of the start of the current block) +{`exists = context.worldState.noteHashes.has({ + leafIndex: M[leafIndexOffset] + leaf: hash(context.environment.storageAddress, M[leafOffset]), +}) +M[existsOffset] = exists`} +
0x2d [`READL1TOL2MSG`](#isa-section-readl1tol2msg)Reads an L1-to-L2 message120{ - `M[dstOffset:dstOffset+msgSize] = context.worldState.l1ToL2Messages(M[msgKeyOffset])` - }0x2d [`EMITNOTEHASH`](#isa-section-emitnotehash)Emit a new note hash to be inserted into the note hash tree +{`context.worldState.noteHashes.append( + hash(context.environment.storageAddress, M[noteHashOffset]) +)`} +
0x2e [`SENDL2TOL1MSG`](#isa-section-sendl2tol1msg)Send an L2-to-L1 message88{ - `context.worldState.l2ToL1Messages.append(M[msgOffset:msgOffset+msgSize])` - }0x2e [`NULLIFIEREXISTS`](#isa-section-nullifierexists)Check whether a nullifier exists in the nullifier tree (including nullifiers from earlier in the current transaction or from earlier in the current block) +{`exists = context.worldState.nullifiers.has( + hash(context.environment.storageAddress, M[nullifierOffset]) +) +M[existsOffset] = exists`} +
0x2f [`EMITNOTEHASH`](#isa-section-emitnotehash)Emit a new note hash to be inserted into the notes tree56{ - `context.worldState.newHashes.append(M[noteHashOffset])` - }0x2f [`EMITNULLIFIER`](#isa-section-emitnullifier)Emit a new nullifier to be inserted into the nullifier tree +{`context.worldState.nullifiers.append( + hash(context.environment.storageAddress, M[nullifierOffset]) +)`} +
0x30 [`EMITNULLIFIER`](#isa-section-emitnullifier)Emit a new nullifier to be inserted into the nullifier tree56{ - `context.worldState.nullifiers.append(M[nullifierOffset])` - }0x30 [`READL1TOL2MSG`](#isa-section-readl1tol2msg)Check if a message exists in the L1-to-L2 message tree and reads it if so. +{`exists = context.worldState.l1ToL2Messages.has({ + leafIndex: M[msgLeafIndex], leaf: M[msgKeyOffset] +}) +M[existsOffset] = exists +if exists: + M[dstOffset:dstOffset+msgSize] = context.worldState.l1ToL2Messages.get({ + leafIndex: M[msgLeafIndex], leaf: M[msgKeyOffset] + })`} +
0x31 [`EMITUNENCRYPTEDLOG`](#isa-section-emitunencryptedlog)0x31 [`HEADERMEMBER`](#isa-section-headermember)Retrieve one member from a specified block's header. Revert if header does not yet exist. See ["Archive"](../state/archive) for more. +{`M[dstOffset] = context.worldState.headers.get(M[blockIndexOffset])[M[memberIndexOffset]]`} +
0x32 [`EMITUNENCRYPTEDLOG`](#isa-section-emitunencryptedlog) Emit an unencrypted log88{ - `context.accruedSubstate.unencryptedLogs.append(M[logOffset:logOffset+logSize])` - } +{`context.accruedSubstate.unencryptedLogs.append( + UnencryptedLog { + address: context.environment.address, + log: M[logOffset:logOffset+logSize], + } +)`} +
0x33 [`SENDL2TOL1MSG`](#isa-section-sendl2tol1msg)Send an L2-to-L1 message +{`context.accruedSubstate.sentL2ToL1Messages.append( + SentL2ToL1Message { + address: context.environment.address, + portal: context.environment.portal, + message: M[msgOffset:msgOffset+msgSize] + } +)`} +
0x32 [`CALL`](#isa-section-call)0x34 [`CALL`](#isa-section-call) Call into another contract248 {`M[successOffset] = call( M[gasOffset], M[gasOffset+1], M[gasOffset+2], @@ -427,9 +419,8 @@ context.machineState.pc = loc`}
0x33 [`STATICCALL`](#isa-section-staticcall)0x35 [`STATICCALL`](#isa-section-staticcall) Call into another contract, disallowing World State and Accrued Substate modifications248 {`M[successOffset] = staticcall( M[gasOffset], M[gasOffset+1], M[gasOffset+2], @@ -439,18 +430,16 @@ context.machineState.pc = loc`}
0x34 [`RETURN`](#isa-section-return)0x36 [`RETURN`](#isa-section-return) Halt execution within this context (without revert), optionally returning some data88 {`context.contractCallResults.output = M[retOffset:retOffset+retSize] halt`}
0x35 [`REVERT`](#isa-section-revert)0x37 [`REVERT`](#isa-section-revert) Halt execution within this context as `reverted`, optionally returning some data88 {`context.contractCallResults.output = M[retOffset:retOffset+retSize] context.contractCallResults.reverted = true @@ -1238,152 +1227,362 @@ Move a word (conditionally chosen) from one memory location to another (`d = con [![](./images/bit-formats/CMOV.png)](./images/bit-formats/CMOV.png) -### `BLOCKHEADERBYNUM` -Get the block header as of the specified block number - -[See in table.](#isa-table-blockheaderbynum) - -- **Opcode**: 0x2a -- **Category**: World State -- **Flags**: - - **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]`. -- **Args**: - - **blockNumOffset**: memory offset of the block number input - - **dstOffset**: memory offset specifying where to store operation's result's 0th word -- **Expression**: `M[dstOffset:dstOffset+BLOCK_HEADER_LENGTH] = context.worldState.blockHeader[M[blockNumOffset]]` -- **Tag updates**: `T[dstOffset:dstOffset+BLOCK_HEADER_LENGTh] = field` -- **Bit-size**: 88 - -[![](./images/bit-formats/BLOCKHEADERBYNUM.png)](./images/bit-formats/BLOCKHEADERBYNUM.png) - ### `SLOAD` -Load a word from storage +Load a word from this contract's persistent public storage. Zero is loaded for unwritten slots. [See in table.](#isa-table-sload) -- **Opcode**: 0x2b +- **Opcode**: 0x2a - **Category**: World State - Public Storage - **Flags**: - **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]`. - **Args**: - **slotOffset**: memory offset of the storage slot to load from - **dstOffset**: memory offset specifying where to store operation's result -- **Expression**: `M[dstOffset] = context.worldState.publicStorage[context.environment.storageAddress, M[slotOffset]]` -- **Details**: Load a word from this contract's persistent public storage into memory. +- **Expression**: + +{`M[dstOffset] = context.worldState.publicStorage[context.environment.storageAddress][M[slotOffset]]`} + +- **Details**: + +{`// Expression is short-hand for +leafIndex = hash(context.environment.storageAddress, M[slotOffset]) +exists = context.worldState.publicStorage.has(leafIndex) // exists == previously-written +if exists: + value = context.worldState.publicStorage.get(leafIndex: leafIndex) +else: + value = 0 +M[dstOffset] = value`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.publicStorageReads.append( + TracedStorageRead { + callPointer: context.environment.callPointer, + slot: M[slotOffset], + exists: exists, // defined above + value: value, // defined above + counter: clk, + } +)`} + +- **Triggers downstream circuit operations**: Storage slot siloing (hash with contract address), public data tree membership check - **Tag updates**: `T[dstOffset] = field` - **Bit-size**: 88 [![](./images/bit-formats/SLOAD.png)](./images/bit-formats/SLOAD.png) ### `SSTORE` -Write a word to storage +Write a word to this contract's persistent public storage [See in table.](#isa-table-sstore) -- **Opcode**: 0x2c +- **Opcode**: 0x2b - **Category**: World State - Public Storage - **Flags**: - **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]`. - **Args**: - **srcOffset**: memory offset of the word to store - **slotOffset**: memory offset containing the storage slot to store to -- **Expression**: `context.worldState.publicStorage[context.environment.storageAddress, M[slotOffset]] = M[srcOffset]` -- **Details**: Store a word from memory into this contract's persistent public storage. +- **Expression**: + +{`context.worldState.publicStorage[context.environment.storageAddress][M[slotOffset]] = M[srcOffset]`} + +- **Details**: + +{`// Expression is short-hand for +context.worldState.publicStorage.set({ + leafIndex: hash(context.environment.storageAddress, M[slotOffset]), + leaf: M[srcOffset], +})`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.publicStorageWrites.append( + TracedStorageWrite { + callPointer: context.environment.callPointer, + slot: M[slotOffset], + value: M[srcOffset], + counter: clk, + } +)`} + +- **Triggers downstream circuit operations**: Storage slot siloing (hash with contract address), public data tree update - **Bit-size**: 88 [![](./images/bit-formats/SSTORE.png)](./images/bit-formats/SSTORE.png) -### `READL1TOL2MSG` -Reads an L1-to-L2 message +### `NOTEHASHEXISTS` +Check whether a note hash exists in the note hash tree (as of the start of the current block) -[See in table.](#isa-table-readl1tol2msg) +[See in table.](#isa-table-notehashexists) -- **Opcode**: 0x2d -- **Category**: World State - Messaging +- **Opcode**: 0x2c +- **Category**: World State - Notes & Nullifiers - **Flags**: - **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]`. - **Args**: - - **msgKeyOffset**: memory offset of the message's key - - **dstOffset**: memory offset to place the 0th word of the message content - - **msgSize**: number of words in the message -- **Expression**: `M[dstOffset:dstOffset+msgSize] = context.worldState.l1ToL2Messages(M[msgKeyOffset])` -- **Tag updates**: `T[dstOffset:dstOffset+msgSize] = field` + - **leafOffset**: memory offset of the leaf + - **leafIndexOffset**: memory offset of the leaf index + - **existsOffset**: memory offset specifying where to store operation's result (whether the archive leaf exists) +- **Expression**: + +{`exists = context.worldState.noteHashes.has({ + leafIndex: M[leafIndexOffset] + leaf: hash(context.environment.storageAddress, M[leafOffset]), +}) +M[existsOffset] = exists`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.noteHashChecks.append( + TracedLeafCheck { + callPointer: context.environment.callPointer, + leafIndex: M[leafIndexOffset] + leaf: M[leafOffset], + exists: exists, // defined above + counter: clk, + } +)`} + +- **Triggers downstream circuit operations**: Note hash siloing (hash with storage contract address), note hash tree membership check +- **Tag updates**: `T[dstOffset] = u8` - **Bit-size**: 120 -[![](./images/bit-formats/READL1TOL2MSG.png)](./images/bit-formats/READL1TOL2MSG.png) -### `SENDL2TOL1MSG` -Send an L2-to-L1 message +### `EMITNOTEHASH` +Emit a new note hash to be inserted into the note hash tree -[See in table.](#isa-table-sendl2tol1msg) +[See in table.](#isa-table-emitnotehash) -- **Opcode**: 0x2e -- **Category**: World State - Messaging +- **Opcode**: 0x2d +- **Category**: World State - Notes & Nullifiers - **Flags**: - **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]`. - **Args**: - - **msgOffset**: memory offset of the message content - - **msgSize**: number of words in the message -- **Expression**: `context.worldState.l2ToL1Messages.append(M[msgOffset:msgOffset+msgSize])` -- **Bit-size**: 88 + - **noteHashOffset**: memory offset of the note hash +- **Expression**: + +{`context.worldState.noteHashes.append( + hash(context.environment.storageAddress, M[noteHashOffset]) +)`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.newNoteHashes.append( + TracedNoteHash { + callPointer: context.environment.callPointer, + value: M[noteHashOffset], // unsiloed note hash + counter: clk, + } +)`} + +- **Triggers downstream circuit operations**: Note hash siloing (hash with contract address), note hash tree insertion. +- **Bit-size**: 56 -[![](./images/bit-formats/SENDL2TOL1MSG.png)](./images/bit-formats/SENDL2TOL1MSG.png) +[![](./images/bit-formats/EMITNOTEHASH.png)](./images/bit-formats/EMITNOTEHASH.png) -### `EMITNOTEHASH` -Emit a new note hash to be inserted into the notes tree +### `NULLIFIEREXISTS` +Check whether a nullifier exists in the nullifier tree (including nullifiers from earlier in the current transaction or from earlier in the current block) -[See in table.](#isa-table-emitnotehash) +[See in table.](#isa-table-nullifierexists) -- **Opcode**: 0x2f +- **Opcode**: 0x2e - **Category**: World State - Notes & Nullifiers - **Flags**: - **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]`. - **Args**: - - **noteHashOffset**: memory offset of the note hash -- **Expression**: `context.worldState.newHashes.append(M[noteHashOffset])` -- **Bit-size**: 56 + - **nullifierOffset**: memory offset of the unsiloed nullifier + - **existsOffset**: memory offset specifying where to store operation's result (whether the nullifier exists) +- **Expression**: + +{`exists = context.worldState.nullifiers.has( + hash(context.environment.storageAddress, M[nullifierOffset]) +) +M[existsOffset] = exists`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.nullifierChecks.append( + TracedIndexedLeafCheck { + callPointer: context.environment.callPointer, + leaf: M[nullifierOffset], + exists: exists, // defined above + counter: clk, + } +)`} + +- **Triggers downstream circuit operations**: Nullifier siloing (hash with storage contract address), nullifier tree membership check +- **Tag updates**: `T[dstOffset] = u8` +- **Bit-size**: 88 -[![](./images/bit-formats/EMITNOTEHASH.png)](./images/bit-formats/EMITNOTEHASH.png) ### `EMITNULLIFIER` Emit a new nullifier to be inserted into the nullifier tree [See in table.](#isa-table-emitnullifier) -- **Opcode**: 0x30 +- **Opcode**: 0x2f - **Category**: World State - Notes & Nullifiers - **Flags**: - **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]`. - **Args**: - **nullifierOffset**: memory offset of nullifier -- **Expression**: `context.worldState.nullifiers.append(M[nullifierOffset])` +- **Expression**: + +{`context.worldState.nullifiers.append( + hash(context.environment.storageAddress, M[nullifierOffset]) +)`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.newNullifiers.append( + TracedNullifier { + callPointer: context.environment.callPointer, + value: M[nullifierOffset], // unsiloed nullifier + counter: clk, + } +)`} + +- **Triggers downstream circuit operations**: Nullifier siloing (hash with contract address), nullifier tree non-membership-check and insertion. - **Bit-size**: 56 [![](./images/bit-formats/EMITNULLIFIER.png)](./images/bit-formats/EMITNULLIFIER.png) +### `READL1TOL2MSG` +Check if a message exists in the L1-to-L2 message tree and reads it if so. + +[See in table.](#isa-table-readl1tol2msg) + +- **Opcode**: 0x30 +- **Category**: World State - Messaging +- **Flags**: + - **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]`. +- **Args**: + - **msgKeyOffset**: memory offset of the message's key + - **msgLeafIndex**: memory offset of the message's leaf index in the L1-to-L2 message tree + - **existsOffset**: memory offset specifying where to store operation's result (whether the message exists in the L1-to-L2 message tree) + - **dstOffset**: memory offset to place the 0th word of the message content + - **msgSize**: number of words in the message +- **Expression**: + +{`exists = context.worldState.l1ToL2Messages.has({ + leafIndex: M[msgLeafIndex], leaf: M[msgKeyOffset] +}) +M[existsOffset] = exists +if exists: + M[dstOffset:dstOffset+msgSize] = context.worldState.l1ToL2Messages.get({ + leafIndex: M[msgLeafIndex], leaf: M[msgKeyOffset] + })`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.l1ToL2MessagesReads.append( + ReadL1ToL2Message { + callPointer: context.environment.callPointer, + portal: context.environment.portal, + leafIndex: M[msgLeafIndex], + msgKey: M[msgKeyOffset], + exists: exists, // defined above + } +)`} + +- **Additional AVM circuit checks**: `msgKey == sha256_to_field(msg)` +- **Triggers downstream circuit operations**: L1-to-L2 message tree membership check +- **Tag updates**: `T[dstOffset:dstOffset+msgSize] = field` +- **Bit-size**: 184 + +[![](./images/bit-formats/READL1TOL2MSG.png)](./images/bit-formats/READL1TOL2MSG.png) + +### `HEADERMEMBER` +Retrieve one member from a specified block's header. Revert if header does not yet exist. See ["Archive"](../state/archive) for more. + +[See in table.](#isa-table-headermember) + +- **Opcode**: 0x31 +- **Category**: World State - Archive Tree & Headers +- **Flags**: + - **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]`. +- **Args**: + - **blockIndexOffset**: memory offset of the block index (same as archive tree leaf index) of the header to access + - **memberIndexOffset**: memory offset of the index of the member to retrieve from the header of the specified block + - **dstOffset**: memory offset specifying where to store operation's result (the retrieved header member) +- **Expression**: + +{`M[dstOffset] = context.worldState.headers.get(M[blockIndexOffset])[M[memberIndexOffset]]`} + +- **World State access tracing**: + +{`context.worldStateAccessTrace.archiveChecks.append( + TracedArchiveLeafCheck { + leafIndex: M[blockIndexOffset], // leafIndex == blockIndex + leaf: hash(context.worldState.headers.get(M[blockIndexOffset])), + } +)`} + +- **Additional AVM circuit checks**: Hashes entire header to archive leaf for tracing. Aggregates header accesses and so that a header need only be hashed once. +- **Triggers downstream circuit operations**: Archive tree membership check +- **Tag updates**: `T[dstOffset] = field` +- **Bit-size**: 120 + + ### `EMITUNENCRYPTEDLOG` Emit an unencrypted log [See in table.](#isa-table-emitunencryptedlog) -- **Opcode**: 0x31 +- **Opcode**: 0x32 - **Category**: Accrued Substate - Logging - **Flags**: - **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]`. - **Args**: - **logOffset**: memory offset of the data to log - **logSize**: number of words to log -- **Expression**: `context.accruedSubstate.unencryptedLogs.append(M[logOffset:logOffset+logSize])` +- **Expression**: + +{`context.accruedSubstate.unencryptedLogs.append( + UnencryptedLog { + address: context.environment.address, + log: M[logOffset:logOffset+logSize], + } +)`} + - **Bit-size**: 88 [![](./images/bit-formats/EMITUNENCRYPTEDLOG.png)](./images/bit-formats/EMITUNENCRYPTEDLOG.png) +### `SENDL2TOL1MSG` +Send an L2-to-L1 message + +[See in table.](#isa-table-sendl2tol1msg) + +- **Opcode**: 0x33 +- **Category**: Accrued Substate - Messaging +- **Flags**: + - **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]`. +- **Args**: + - **msgOffset**: memory offset of the message content + - **msgSize**: number of words in the message +- **Expression**: + +{`context.accruedSubstate.sentL2ToL1Messages.append( + SentL2ToL1Message { + address: context.environment.address, + portal: context.environment.portal, + message: M[msgOffset:msgOffset+msgSize] + } +)`} + +- **Bit-size**: 88 + +[![](./images/bit-formats/SENDL2TOL1MSG.png)](./images/bit-formats/SENDL2TOL1MSG.png) + ### `CALL` Call into another contract [See in table.](#isa-table-call) -- **Opcode**: 0x32 +- **Opcode**: 0x34 - **Category**: Control Flow - Contract Calls - **Flags**: - **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]`. @@ -1421,7 +1620,7 @@ Call into another contract, disallowing World State and Accrued Substate modific [See in table.](#isa-table-staticcall) -- **Opcode**: 0x33 +- **Opcode**: 0x35 - **Category**: Control Flow - Contract Calls - **Flags**: - **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]`. @@ -1457,7 +1656,7 @@ Halt execution within this context (without revert), optionally returning some d [See in table.](#isa-table-return) -- **Opcode**: 0x34 +- **Opcode**: 0x36 - **Category**: Control Flow - Contract Calls - **Flags**: - **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]`. @@ -1479,7 +1678,7 @@ Halt execution within this context as `reverted`, optionally returning some data [See in table.](#isa-table-revert) -- **Opcode**: 0x35 +- **Opcode**: 0x37 - **Category**: Control Flow - Contract Calls - **Flags**: - **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]`. diff --git a/yellow-paper/docs/public-vm/instruction-set.mdx b/yellow-paper/docs/public-vm/instruction-set.mdx index 1693295d2de..3b751dd3984 100644 --- a/yellow-paper/docs/public-vm/instruction-set.mdx +++ b/yellow-paper/docs/public-vm/instruction-set.mdx @@ -7,6 +7,8 @@ The following notes are relevant to the table and sections below: - Any instruction whose description does not mention a program counter change simply increments it: `context.machineState.pc++` - All instructions update `context.machineState.*GasLeft` as detailed in ["Gas limits and tracking"](./avm#gas-limits-and-tracking) - Any instruction can lead to an exceptional halt as specified in ["Exceptional halting"](./avm#exceptional-halting) +- The term `hash` used in expressions below represents a Poseidon hash operation. +- Type structures used in world state tracing operations are defined in ["Type Definitions"](./type-structs) import GeneratedInstructionSet from "./gen/_InstructionSet.mdx"; diff --git a/yellow-paper/docs/public-vm/memory-model.md b/yellow-paper/docs/public-vm/memory-model.md index d6087cba3e8..28f65c03de2 100644 --- a/yellow-paper/docs/public-vm/memory-model.md +++ b/yellow-paper/docs/public-vm/memory-model.md @@ -1,6 +1,6 @@ # Memory State Model -The goal of this note is to describe the VM state model and to specify "internal" VM abstractions that can be mapped to circuit designs. +This section describes the AVM memory model, and in particular specifies "internal" VM abstractions that can be mapped to the VM's circuit architecture. ## A memory-only state model diff --git a/yellow-paper/docs/public-vm/state.md b/yellow-paper/docs/public-vm/state.md index 87fee2a6854..78976f63e76 100644 --- a/yellow-paper/docs/public-vm/state.md +++ b/yellow-paper/docs/public-vm/state.md @@ -10,27 +10,28 @@ This section describes the types of state maintained by the AVM. | Field | Type | Description | | --- | --- | --- | -| `l1GasLeft` | `field` | Tracks the amount of L1 gas remaining at any point during execution. | -| `l2GasLeft` | `field` | Tracks the amount of L2 gas remaining at any point during execution. | -| `daGasLeft` | `field` | Tracks the amount of DA gas remaining at any point during execution. | -| `pc` | `field` | Index into the contract's bytecode indicating which instruction to execute. Initialized\* to 0. | -| `internalCallStack` | `Vector` | A stack of program counters pushed to and popped from by `INTERNALCALL` and `INTERNALRETURN` instructions. Initialized\* as empty. | -| `memory` | `[field; 2^32]` | A $2^{32}$ entry memory space accessible by user code (bytecode instructions). All 2^32 entries are initialized\* to 0. See ["Memory Model"](./memory-model) for a complete description of AVM memory. | +| `l1GasLeft` | `field` | Tracks the amount of L1 gas remaining at any point during execution. Initialized from contract call arguments. | +| `l2GasLeft` | `field` | Tracks the amount of L2 gas remaining at any point during execution. Initialized from contract call arguments. | +| `daGasLeft` | `field` | Tracks the amount of DA gas remaining at any point during execution. Initialized from contract call arguments. | +| `pc` | `field` | Index into the contract's bytecode indicating which instruction to execute. Initialized to 0 during context initialization. | +| `internalCallStack` | `Vector` | A stack of program counters pushed to and popped from by `INTERNALCALL` and `INTERNALRETURN` instructions. Initialized as empty during context initialization. | +| `memory` | `[field; 2^32]` | A $2^{32}$ entry memory space accessible by user code (bytecode instructions). All $2^{32}$ entries are assigned default value 0 during context initialization. See ["Memory Model"](./memory-model) for a complete description of AVM memory. | ## World State ### AVM's access to Aztec State -[Aztec's global state](../state) is implemented as a few merkle trees that are exposed to the AVM as follows: -| State | Tree | Tree Type | AVM Access | -| --- | --- | --- | --- | -| Note Hashes | Note Hash Tree | Append-only merkle tree | membership-checks (start-of-block), appends | -| Nullifiers | Nullifier Tree | Indexed merkle tree | membership-checks (latest), appends | -| L1-to-L2 Messages | L1-to-L2 Message Tree | Append-only (or indexed?) merkle tree | membership-checks (start-of-block), leaf-preimage-reads | -| Public Storage | Public Data Tree | Updatable merkle tree | membership-checks (latest), reads, writes | -| Headers | Archive Tree | Append-only merkle tree | membership-checks, leaf-preimage-reads | +[Aztec's global state](../state) is implemented as a few merkle trees. These trees are exposed to the AVM as follows: -> As described in ["Contract Deployment"](../contract-deployment), contracts are not stored in a dedicated tree. A [contract class](../contract-deployment/classes) is [represented](../contract-deployment/classes#registration) as an unencrypted log containing the `ContractClass` structure (which contains the bytecode) and a nullifier representing the class identifier. The `contractClasses` interface provides access to contract classes indexed by class identifier. A [contract instance](../contract-deployment/instances) is [represented](../contract-deployment/classes#registration) as an unencrypted log containing the `ContractInstance` structure and a nullifier representing the contract address. The `contractInstances` interface provides access to contract instances indexed by contract address. +| State | Tree | Merkle Tree Type | AVM Access | +| --- | --- | --- | --- | +| Public Storage | Public Data Tree | Updatable | membership-checks (latest), reads, writes | +| Note Hashes | Note Hash Tree | Append-only | membership-checks (start-of-block), appends | +| Nullifiers | Nullifier Tree | Indexed | membership-checks (latest), appends | +| L1-to-L2 Messages | L1-to-L2 Message Tree | Append-only | membership-checks (start-of-block), leaf-preimage-reads | +| Headers | Archive Tree | Append-only | membership-checks, leaf-preimage-reads | + +> As described in ["Contract Deployment"](../contract-deployment), contracts are not stored in a dedicated tree. A [contract class](../contract-deployment/classes) is [represented](../contract-deployment/classes#registration) as an unencrypted log containing the `ContractClass` structure (which contains the bytecode) and a nullifier representing the class identifier. A [contract instance](../contract-deployment/instances) is [represented](../contract-deployment/classes#registration) as an unencrypted log containing the `ContractInstance` structure and a nullifier representing the contract address. ### AVM World State @@ -42,13 +43,13 @@ As the AVM executes contract code, instructions may read or modify the world sta The following table defines an AVM context's world state interface: -| Field | AVM Instructions & Access | -| --- | --- | -| `noteHashes` | `NOTEHASHEXISTS` (membership-checks (start-of-block)), `EMITNULLIFIER` (appends) | -| `nullifiers` | `NULLIFIERSEXISTS` membership-checks (latest), `EMITNULLIFIER` (appends) | -| `l1ToL2Messages` | `READL1TOL2MSG` (membership-checks (start-of-block) & leaf-preimage-reads) | -| `publicStorage` | `SLOAD` (membership-checks (latest) & reads), `SSTORE` (writes) | -| `headers` | `HEADERMEMBER` (membership-checks & leaf-preimage-reads) | +| Field | AVM Instructions & Access | +| --- | --- | +| `publicStorage` | [`SLOAD`](./instruction-set#isa-section-sload) (membership-checks (latest) & reads), [`SSTORE`](./instruction-set#isa-section-sstore) (writes) | +| `noteHashes` | [`NOTEHASHEXISTS`](./instruction-set#isa-section-notehashexists) (membership-checks (start-of-block)), [`EMITNOTEHASH`](./instruction-set#isa-section-emitnotehash) (appends) | +| `nullifiers` | [`NULLIFIERSEXISTS`](./instruction-set#isa-section-nullifierexists) membership-checks (latest), [`EMITNULLIFIER`](./instruction-set#isa-section-emitnullifier) (appends) | +| `l1ToL2Messages` | [`READL1TOL2MSG`](./instruction-set#isa-section-readl1tol2msg) (membership-checks (start-of-block) & leaf-preimage-reads) | +| `headers` | [`HEADERMEMBER`](./instruction-set#isa-section-headermember) (membership-checks & leaf-preimage-reads) | ### World State Access Trace @@ -64,19 +65,19 @@ Each entry in the world state access trace is listed below along with its type a | Trace | Relevant State | Trace Vector Type | Instructions | | --- | --- | --- | --- | -| `publicStorageReads` | Public Storage | `Vector` | `SLOAD` | -| `publicStorageWrites` | Public Storage | `Vector` | `SSTORE` | -| `l1ToL2MessageReads` | L1-To-L2 Messages | `Vector` | `READL1TOL2MSG` | -| `noteHashChecks` | Note Hashes | `Vector` | `NOTEHASHEXISTS` | -| `newNoteHashes` | Note Hashes | `Vector` | `EMITNOTEHASH` | -| `nullifierChecks` | Nullifiers | `Vector` | `NULLIFIEREXISTS` | -| `newNullifiers` | Nullifiers | `Vector` | `EMITNULLIFIER` | -| `archiveChecks` | Headers | `Vector` | `HEADERMEMBER` | -| `contractCalls` | - | `Vector` | `*CALL` | +| `publicStorageReads` | Public Storage | `Vector` | [`SLOAD`](./instruction-set#isa-section-sload) | +| `publicStorageWrites` | Public Storage | `Vector` | [`SSTORE`](./instruction-set#isa-section-sstore) | +| `noteHashChecks` | Note Hashes | `Vector` | [`NOTEHASHEXISTS`](./instruction-set#isa-section-notehashexists) | +| `newNoteHashes` | Note Hashes | `Vector` | [`EMITNOTEHASH`](./instruction-set#isa-section-emitnotehash) | +| `nullifierChecks` | Nullifiers | `Vector` | [`NULLIFIERSEXISTS`](./instruction-set#isa-section-nullifierexists) | +| `newNullifiers` | Nullifiers | `Vector` | [`EMITNULLIFIER`](./instruction-set#isa-section-emitnullifier) | +| `l1ToL2MessageReads` | L1-To-L2 Messages | `Vector` | [`READL1TOL2MSG`](./instruction-set#isa-section-readl1tol2msg) | +| `archiveChecks` | Headers | `Vector` | [`HEADERMEMBER`](./instruction-set#isa-section-headermember) | +| `contractCalls` | - | `Vector` | [`*CALL`](./instruction-set#isa-section-call) | > The types tracked in these trace vectors are defined [here](./type-structs). -> The syntax `*CALL` is short for `CALL`/`STATICCALL`/`DELEGATECALL`. +> `*CALL` is short for `CALL`/`STATICCALL`/`DELEGATECALL`. > Aztec tree operations like membership checks, appends, or leaf updates are performed in-circuit by downstream circuits (public kernel and rollup circuits), _after_ AVM execution. The world state access trace is a list of requests made by the AVM for later circuits to perform. @@ -84,12 +85,13 @@ Each entry in the world state access trace is listed below along with its type a > The term "accrued substate" is borrowed from the [Ethereum Yellow Paper](https://ethereum.github.io/yellowpaper/paper.pdf). -**Accrued substate** is accrued throughout a context's execution, but updates to it are strictly never relevant to subsequent instructions, contract calls, or transactions. An execution context is always initialized with empty accrued substate, and instructions can append to its vectors which are _append-only_. If a contract call's execution succeeds, its accrued substate is appended to the caller's. If a contract's execution reverts, its accrued substate is ignored. There is no accrued substate "trace" that includes entries from reverted contexts. +**Accrued substate** is accrued throughout a context's execution, but updates to it are strictly never relevant to subsequent instructions, contract calls, or transactions. An execution context is always initialized with empty accrued substate. Its vectors are append-only, and the instructions listed below append to these vectors. If a contract call's execution succeeds, its accrued substate is appended to the caller's. If a contract's execution reverts, its accrued substate is ignored. #### _AccruedSubstate_ -| Field | Type | Instructions | Description | -| --- | --- | --- | --- | -| `unencryptedLogs` | `Vector` | `ULOG` | | -| `sentL2ToL1Messages` | `Vector` | `SENDL1TOL2MSG` | | + +| Field | Type | Instructions | +| --- | --- | --- | +| `unencryptedLogs` | `Vector` | [`ULOG`](./instruction-set#isa-secction-ulog) | +| `sentL2ToL1Messages` | `Vector` | [`SENDL1TOL2MSG`](./instruction-set#isa-secction-sendl2tol1msg) | > The types tracked in these vectors are defined [here](./type-structs). diff --git a/yellow-paper/docs/public-vm/type-structs.md b/yellow-paper/docs/public-vm/type-structs.md index 948497c70c7..122821a487a 100644 --- a/yellow-paper/docs/public-vm/type-structs.md +++ b/yellow-paper/docs/public-vm/type-structs.md @@ -16,11 +16,24 @@ This section lists type definitions relevant to AVM State and Circuit I/O. | --- | --- | --- | | `callPointer` | `field` | Associates this item with a `TracedContractCall` entry in `worldStateAccessTrace.contractCalls` | | `portal` | `EthAddress` | | -| `msgKey` | `field` | | +| `leafIndex` | `field` | | +| `msgKey` | `field` | The message key which is also the tree leaf value. | +| `exists` | `field` | | | `message` | `[field; MAX_L1_TO_L2_MESSAGE_LENGTH]` | **Omitted from public inputs** | | `endLifetime` | `field` | Equivalent to `endLifetime` of the containing contract call. | -#### _TracedStorageAccess_ +#### _TracedStorageRead_ + +| Field | Type | Description | +| --- | --- | --- | +| `callPointer` | `field` | Associates this item with a `TracedContractCall` entry in `worldStateAccessTrace.contractCalls`| +| `slot` | `field` | | +| `exists` | `field` | Whether this slot has ever been previously written | +| `value` | `field` | | +| `counter` | `field` | | +| `endLifetime` | `field` | Equivalent to `endLifetime` of the containing contract call. The last `counter` at which this read/write should be considered to "exist" if this call or a parent reverted. | + +#### _TracedStorageWrite_ | Field | Type | Description | | --- | --- | --- | @@ -65,8 +78,8 @@ This section lists type definitions relevant to AVM State and Circuit I/O. | Field | Type | Description | | --- | --- | --- | | `callPointer` | `field` | Associates this item with a `TracedContractCall` entry in `worldStateAccessTrace.contractCalls` | -| `leaf` | `field` | | | `leafIndex` | `field` | | +| `leaf` | `field` | | | `exists` | `field` | | | `counter` | `field` | | | `endLifetime` | `field` | Equivalent to `endLifetime` of the containing contract call. | diff --git a/yellow-paper/src/preprocess/InstructionSet/InstructionSet.js b/yellow-paper/src/preprocess/InstructionSet/InstructionSet.js index 8ccc09061b1..266ceaaf28d 100644 --- a/yellow-paper/src/preprocess/InstructionSet/InstructionSet.js +++ b/yellow-paper/src/preprocess/InstructionSet/InstructionSet.js @@ -1,10 +1,10 @@ const {instructionSize} = require('./InstructionSize'); const TOPICS_IN_TABLE = [ - "Name", "Summary", "Bit-size", "Expression", + "Name", "Summary", "Expression", ]; const TOPICS_IN_SECTIONS = [ - "Name", "Summary", "Category", "Flags", "Args", "Expression", "Details", "Tag checks", "Tag updates", "Bit-size", + "Name", "Summary", "Category", "Flags", "Args", "Expression", "Details", "World State access tracing", "Additional AVM circuit checks", "Triggers downstream circuit operations", "Tag checks", "Tag updates", "Bit-size", ]; const IN_TAG_DESCRIPTION = "The [tag/size](./memory-model#tags-and-tagged-memory) to check inputs against and tag the destination with."; @@ -729,23 +729,6 @@ context.machineState.pc = loc "Tag checks": "", "Tag updates": "`T[dstOffset] = M[condOffset] > 0 ? T[aOffset] : T[bOffset]`", }, - { - "id": "blockheaderbynum", - "Name": "`BLOCKHEADERBYNUM`", - "Category": "World State", - "Flags": [ - {"name": "indirect", "description": INDIRECT_FLAG_DESCRIPTION}, - ], - "Args": [ - {"name": "blockNumOffset", "description": "memory offset of the block number input"}, - {"name": "dstOffset", "description": "memory offset specifying where to store operation's result's 0th word"}, - ], - "Expression": "`M[dstOffset:dstOffset+BLOCK_HEADER_LENGTH] = context.worldState.blockHeader[M[blockNumOffset]]`", - "Summary": "Get the block header as of the specified block number", - "Details": "", - "Tag checks": "", - "Tag updates": "`T[dstOffset:dstOffset+BLOCK_HEADER_LENGTh] = field`", - }, { "id": "sload", "Name": "`SLOAD`", @@ -757,9 +740,32 @@ context.machineState.pc = loc {"name": "slotOffset", "description": "memory offset of the storage slot to load from"}, {"name": "dstOffset", "description": "memory offset specifying where to store operation's result"}, ], - "Expression": "`M[dstOffset] = context.worldState.publicStorage[context.environment.storageAddress, M[slotOffset]]`", - "Summary": "Load a word from storage", - "Details": "Load a word from this contract's persistent public storage into memory.", + "Expression": ` +M[dstOffset] = context.worldState.publicStorage[context.environment.storageAddress][M[slotOffset]] +`, + "Summary": "Load a word from this contract's persistent public storage. Zero is loaded for unwritten slots.", + "Details": ` +// Expression is short-hand for +leafIndex = hash(context.environment.storageAddress, M[slotOffset]) +exists = context.worldState.publicStorage.has(leafIndex) // exists == previously-written +if exists: + value = context.worldState.publicStorage.get(leafIndex: leafIndex) +else: + value = 0 +M[dstOffset] = value +`, + "World State access tracing": ` +context.worldStateAccessTrace.publicStorageReads.append( + TracedStorageRead { + callPointer: context.environment.callPointer, + slot: M[slotOffset], + exists: exists, // defined above + value: value, // defined above + counter: clk, + } +) +`, + "Triggers downstream circuit operations": "Storage slot siloing (hash with contract address), public data tree membership check", "Tag checks": "", "Tag updates": "`T[dstOffset] = field`", }, @@ -774,62 +780,126 @@ context.machineState.pc = loc {"name": "srcOffset", "description": "memory offset of the word to store"}, {"name": "slotOffset", "description": "memory offset containing the storage slot to store to"}, ], - "Expression": "`context.worldState.publicStorage[context.environment.storageAddress, M[slotOffset]] = M[srcOffset]`", - "Summary": "Write a word to storage", - "Details": "Store a word from memory into this contract's persistent public storage.", + "Expression": ` +context.worldState.publicStorage[context.environment.storageAddress][M[slotOffset]] = M[srcOffset] +`, + "Summary": "Write a word to this contract's persistent public storage", + "Details": ` +// Expression is short-hand for +context.worldState.publicStorage.set({ + leafIndex: hash(context.environment.storageAddress, M[slotOffset]), + leaf: M[srcOffset], +}) +`, + "World State access tracing": ` +context.worldStateAccessTrace.publicStorageWrites.append( + TracedStorageWrite { + callPointer: context.environment.callPointer, + slot: M[slotOffset], + value: M[srcOffset], + counter: clk, + } +) +`, + "Triggers downstream circuit operations": "Storage slot siloing (hash with contract address), public data tree update", "Tag checks": "", "Tag updates": "", }, { - "id": "readl1tol2msg", - "Name": "`READL1TOL2MSG`", - "Category": "World State - Messaging", + "id": "notehashexists", + "Name": "`NOTEHASHEXISTS`", + "Category": "World State - Notes & Nullifiers", "Flags": [ {"name": "indirect", "description": INDIRECT_FLAG_DESCRIPTION}, ], "Args": [ - {"name": "msgKeyOffset", "description": "memory offset of the message's key"}, - {"name": "dstOffset", "description": "memory offset to place the 0th word of the message content"}, - {"name": "msgSize", "description": "number of words in the message", "mode": "immediate", "type": "u32"}, + {"name": "leafOffset", "description": "memory offset of the leaf"}, + {"name": "leafIndexOffset", "description": "memory offset of the leaf index"}, + {"name": "existsOffset", "description": "memory offset specifying where to store operation's result (whether the archive leaf exists)"}, ], - "Expression": "`M[dstOffset:dstOffset+msgSize] = context.worldState.l1ToL2Messages(M[msgKeyOffset])`", - "Summary": "Reads an L1-to-L2 message", - "Details": "", + "Expression": ` +exists = context.worldState.noteHashes.has({ + leafIndex: M[leafIndexOffset] + leaf: hash(context.environment.storageAddress, M[leafOffset]), +}) +M[existsOffset] = exists +`, + "Summary": "Check whether a note hash exists in the note hash tree (as of the start of the current block)", + "World State access tracing": ` +context.worldStateAccessTrace.noteHashChecks.append( + TracedLeafCheck { + callPointer: context.environment.callPointer, + leafIndex: M[leafIndexOffset] + leaf: M[leafOffset], + exists: exists, // defined above + counter: clk, + } +) +`, + "Triggers downstream circuit operations": "Note hash siloing (hash with storage contract address), note hash tree membership check", "Tag checks": "", - "Tag updates": "`T[dstOffset:dstOffset+msgSize] = field`", + "Tag updates": "`T[dstOffset] = u8`", }, { - "id": "sendl2tol1msg", - "Name": "`SENDL2TOL1MSG`", - "Category": "World State - Messaging", + "id": "emitnotehash", + "Name": "`EMITNOTEHASH`", + "Category": "World State - Notes & Nullifiers", "Flags": [ {"name": "indirect", "description": INDIRECT_FLAG_DESCRIPTION}, ], "Args": [ - {"name": "msgOffset", "description": "memory offset of the message content"}, - {"name": "msgSize", "description": "number of words in the message", "mode": "immediate", "type": "u32"}, + {"name": "noteHashOffset", "description": "memory offset of the note hash"}, ], - "Expression": "`context.worldState.l2ToL1Messages.append(M[msgOffset:msgOffset+msgSize])`", - "Summary": "Send an L2-to-L1 message", - "Details": "", + "Expression": ` +context.worldState.noteHashes.append( + hash(context.environment.storageAddress, M[noteHashOffset]) +) +`, + "Summary": "Emit a new note hash to be inserted into the note hash tree", + "World State access tracing": ` +context.worldStateAccessTrace.newNoteHashes.append( + TracedNoteHash { + callPointer: context.environment.callPointer, + value: M[noteHashOffset], // unsiloed note hash + counter: clk, + } +) +`, + "Triggers downstream circuit operations": "Note hash siloing (hash with contract address), note hash tree insertion.", "Tag checks": "", "Tag updates": "", }, { - "id": "emitnotehash", - "Name": "`EMITNOTEHASH`", + "id": "nullifierexists", + "Name": "`NULLIFIEREXISTS`", "Category": "World State - Notes & Nullifiers", "Flags": [ {"name": "indirect", "description": INDIRECT_FLAG_DESCRIPTION}, ], "Args": [ - {"name": "noteHashOffset", "description": "memory offset of the note hash"}, + {"name": "nullifierOffset", "description": "memory offset of the unsiloed nullifier"}, + {"name": "existsOffset", "description": "memory offset specifying where to store operation's result (whether the nullifier exists)"}, ], - "Expression": "`context.worldState.newHashes.append(M[noteHashOffset])`", - "Summary": "Emit a new note hash to be inserted into the notes tree", - "Details": "", + "Expression": ` +exists = context.worldState.nullifiers.has( + hash(context.environment.storageAddress, M[nullifierOffset]) +) +M[existsOffset] = exists +`, + "Summary": "Check whether a nullifier exists in the nullifier tree (including nullifiers from earlier in the current transaction or from earlier in the current block)", + "World State access tracing": ` +context.worldStateAccessTrace.nullifierChecks.append( + TracedIndexedLeafCheck { + callPointer: context.environment.callPointer, + leaf: M[nullifierOffset], + exists: exists, // defined above + counter: clk, + } +) +`, + "Triggers downstream circuit operations": "Nullifier siloing (hash with storage contract address), nullifier tree membership check", "Tag checks": "", - "Tag updates": "", + "Tag updates": "`T[dstOffset] = u8`", }, { "id": "emitnullifier", @@ -841,12 +911,95 @@ context.machineState.pc = loc "Args": [ {"name": "nullifierOffset", "description": "memory offset of nullifier"}, ], - "Expression": "`context.worldState.nullifiers.append(M[nullifierOffset])`", + "Expression": ` +context.worldState.nullifiers.append( + hash(context.environment.storageAddress, M[nullifierOffset]) +) +`, "Summary": "Emit a new nullifier to be inserted into the nullifier tree", - "Details": "", + "World State access tracing": ` +context.worldStateAccessTrace.newNullifiers.append( + TracedNullifier { + callPointer: context.environment.callPointer, + value: M[nullifierOffset], // unsiloed nullifier + counter: clk, + } +) +`, + "Triggers downstream circuit operations": "Nullifier siloing (hash with contract address), nullifier tree non-membership-check and insertion.", "Tag checks": "", "Tag updates": "", }, + { + "id": "readl1tol2msg", + "Name": "`READL1TOL2MSG`", + "Category": "World State - Messaging", + "Flags": [ + {"name": "indirect", "description": INDIRECT_FLAG_DESCRIPTION}, + ], + "Args": [ + {"name": "msgKeyOffset", "description": "memory offset of the message's key"}, + {"name": "msgLeafIndex", "description": "memory offset of the message's leaf index in the L1-to-L2 message tree"}, + {"name": "existsOffset", "description": "memory offset specifying where to store operation's result (whether the message exists in the L1-to-L2 message tree)"}, + {"name": "dstOffset", "description": "memory offset to place the 0th word of the message content"}, + {"name": "msgSize", "description": "number of words in the message", "mode": "immediate", "type": "u32"}, + ], + "Expression": ` +exists = context.worldState.l1ToL2Messages.has({ + leafIndex: M[msgLeafIndex], leaf: M[msgKeyOffset] +}) +M[existsOffset] = exists +if exists: + M[dstOffset:dstOffset+msgSize] = context.worldState.l1ToL2Messages.get({ + leafIndex: M[msgLeafIndex], leaf: M[msgKeyOffset] + }) +`, + "Summary": "Check if a message exists in the L1-to-L2 message tree and reads it if so.", + "World State access tracing": ` +context.worldStateAccessTrace.l1ToL2MessagesReads.append( + ReadL1ToL2Message { + callPointer: context.environment.callPointer, + portal: context.environment.portal, + leafIndex: M[msgLeafIndex], + msgKey: M[msgKeyOffset], + exists: exists, // defined above + } +) +`, + "Additional AVM circuit checks": "`msgKey == sha256_to_field(msg)`", + "Triggers downstream circuit operations": "L1-to-L2 message tree membership check", + "Tag checks": "", + "Tag updates": "`T[dstOffset:dstOffset+msgSize] = field`", + }, + { + "id": "headermember", + "Name": "`HEADERMEMBER`", + "Category": "World State - Archive Tree & Headers", + "Flags": [ + {"name": "indirect", "description": INDIRECT_FLAG_DESCRIPTION}, + ], + "Args": [ + {"name": "blockIndexOffset", "description": "memory offset of the block index (same as archive tree leaf index) of the header to access"}, + {"name": "memberIndexOffset", "description": "memory offset of the index of the member to retrieve from the header of the specified block"}, + {"name": "dstOffset", "description": "memory offset specifying where to store operation's result (the retrieved header member)"}, + ], + "Expression": ` +M[dstOffset] = context.worldState.headers.get(M[blockIndexOffset])[M[memberIndexOffset]] +`, + "Summary": "Retrieve one member from a specified block's header. Revert if header does not yet exist. See [\"Archive\"](../state/archive) for more.", + "World State access tracing": ` +context.worldStateAccessTrace.archiveChecks.append( + TracedArchiveLeafCheck { + leafIndex: M[blockIndexOffset], // leafIndex == blockIndex + leaf: hash(context.worldState.headers.get(M[blockIndexOffset])), + } +) +`, + "Additional AVM circuit checks": "Hashes entire header to archive leaf for tracing. Aggregates header accesses and so that a header need only be hashed once.", + "Triggers downstream circuit operations": "Archive tree membership check", + "Tag checks": "", + "Tag updates": "`T[dstOffset] = field`", + }, { "id": "emitunencryptedlog", "Name": "`EMITUNENCRYPTEDLOG`", @@ -858,9 +1011,39 @@ context.machineState.pc = loc {"name": "logOffset", "description": "memory offset of the data to log"}, {"name": "logSize", "description": "number of words to log", "mode": "immediate", "type": "u32"}, ], - "Expression": "`context.accruedSubstate.unencryptedLogs.append(M[logOffset:logOffset+logSize])`", + "Expression": ` +context.accruedSubstate.unencryptedLogs.append( + UnencryptedLog { + address: context.environment.address, + log: M[logOffset:logOffset+logSize], + } +) +`, "Summary": "Emit an unencrypted log", - "Details": "", + "Tag checks": "", + "Tag updates": "", + }, + { + "id": "sendl2tol1msg", + "Name": "`SENDL2TOL1MSG`", + "Category": "Accrued Substate - Messaging", + "Flags": [ + {"name": "indirect", "description": INDIRECT_FLAG_DESCRIPTION}, + ], + "Args": [ + {"name": "msgOffset", "description": "memory offset of the message content"}, + {"name": "msgSize", "description": "number of words in the message", "mode": "immediate", "type": "u32"}, + ], + "Expression": ` +context.accruedSubstate.sentL2ToL1Messages.append( + SentL2ToL1Message { + address: context.environment.address, + portal: context.environment.portal, + message: M[msgOffset:msgOffset+msgSize] + } +) +`, + "Summary": "Send an L2-to-L1 message", "Tag checks": "", "Tag updates": "", },