From 9cff57c14316580f1aaaf37a8853b7708a11314e Mon Sep 17 00:00:00 2001 From: "g. nicholas d'andrea" Date: Wed, 5 Aug 2026 18:03:09 -0400 Subject: [PATCH 1/2] format: state the postcondition convention for instruction contexts MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The instruction context description carried one sentence framing pointers as resolving against the pre-execution ("trace step") state, contradicting the rest of the same description ("following the execution"), the program-example walkthrough, and compiler emission — all of which treat a context as a postcondition. This states the intended convention plainly. - program/instruction: a context holds following the instruction's execution; both its semantic facts and its pointers resolve against the post-execution state. Contexts form a chain — the program-level context is the precondition before the first instruction, each instruction's context is its postcondition (and the next instruction's precondition), and a debugger paused about to execute instruction i reads instruction i-1's context. - program: the program-level context description now names its role as the base case of that chain (the precondition to the first instruction). - program example: under the postcondition reading the Incrementer example was correct except at the ADD and the following PUSH0, where it still listed localValue on the stack after ADD had consumed it (leaving only storedValue + 1). localValue is now dropped from those two contexts. Also removes a stale 'value = tmp;' line from the pseudo-code. --- schemas/program.schema.yaml | 15 +++++++-------- schemas/program/instruction.schema.yaml | 19 +++++++++++++------ 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/schemas/program.schema.yaml b/schemas/program.schema.yaml index 1426dd577d..4539900027 100644 --- a/schemas/program.schema.yaml +++ b/schemas/program.schema.yaml @@ -36,8 +36,11 @@ properties: context: description: | - The context known to exist prior to the execution of the first - instruction in the bytecode. + The context that holds prior to the execution of the first + instruction in the bytecode. This is the base case of the context + chain — the precondition to the first instruction — from which each + instruction's own `context` follows as a postcondition (see + **ethdebug/format/program/instruction**). This field is **optional**. Omitting it is equivalent to specifying the empty context value (`{}`). @@ -71,7 +74,6 @@ examples: # code { # let localValue = storedValue; # storedValue += 1; - # value = tmp; # }; # ``` contract: @@ -126,20 +128,17 @@ examples: - offset: 4 operation: mnemonic: ADD + # ADD consumes localValue, leaving storedValue + 1 on the stack, + # so localValue is no longer observable from this point on. context: variables: - *stored-value - - *local-value - offset: 5 operation: mnemonic: PUSH0 context: variables: - *stored-value - - <<: *local-value - pointer: - location: stack - slot: 1 - offset: 6 operation: diff --git a/schemas/program/instruction.schema.yaml b/schemas/program/instruction.schema.yaml index 12640502c6..122cb9176f 100644 --- a/schemas/program/instruction.schema.yaml +++ b/schemas/program/instruction.schema.yaml @@ -42,12 +42,19 @@ properties: context: description: | - The context known to exist following the execution of this instruction. - "Following execution" means the context's semantic facts (source - location, variables in scope, function invocation, etc.) hold from - this point forward. Pointers within the context reference the machine - state at this instruction's trace step, which is the state a debugger - observes when it encounters the instruction. + The context that holds **following** the execution of this + instruction. Both its semantic facts (source location, variables in + scope, function invocation, etc.) and any pointers it contains resolve + against the machine state **after** the instruction has executed + (its postcondition). + + Instruction contexts form a chain. The program-level `context` is the + base case: the precondition that holds before the first instruction + executes. Each instruction's context is then the postcondition of that + instruction, which is in turn the precondition of the next. A debugger + paused at the trace step about to execute instruction *i* therefore + reads the context of instruction *i − 1* — or, before the first + instruction, the program-level `context`. This field is **optional**. Omitting it is equivalent to specifying the empty context value (`{}`). From 1d0d8f2677f25d8d12ad77a64ebdff8460fe3379 Mon Sep 17 00:00:00 2001 From: "g. nicholas d'andrea" Date: Wed, 5 Aug 2026 18:32:27 -0400 Subject: [PATCH 2/2] format: note the no-special-case chain formulation for contexts MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the equivalent trace-position framing to the instruction context description: prepending the program-level context to the sequence of instruction contexts gives one sequence indexed by trace position, so the context in effect before executing the instruction at position i is element i — no special case for the first instruction. --- schemas/program/instruction.schema.yaml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/schemas/program/instruction.schema.yaml b/schemas/program/instruction.schema.yaml index 122cb9176f..ee361407df 100644 --- a/schemas/program/instruction.schema.yaml +++ b/schemas/program/instruction.schema.yaml @@ -54,7 +54,11 @@ properties: instruction, which is in turn the precondition of the next. A debugger paused at the trace step about to execute instruction *i* therefore reads the context of instruction *i − 1* — or, before the first - instruction, the program-level `context`. + instruction, the program-level `context`. Equivalently, prepending + the program-level `context` to the sequence of instruction contexts + yields a single sequence indexed by trace position, with no special + case: the context in effect when about to execute the instruction at + position *i* is element *i* of that sequence. This field is **optional**. Omitting it is equivalent to specifying the empty context value (`{}`).