format: resolve external-call invoke operands before the instruction

CHANGELOG.md

@@ -25,9 +25,9 @@ Each `Producers:` and `Consumers:` sub-item starts with one of three prefixes:
   sub-item says what the party may now do.
 - `required:` Output that was valid in the previous published version no longer
   validates, or the specification adds or changes a normative **must**, or the
-  meaning of data that was already valid changes. The sub-item names the schema keyword, or
-  quotes the specification prose, that imposes the obligation. Prose that says
-  **should** or "preferred" is never `required:`.
+  meaning of data that was already valid changes. The sub-item names the schema
+  keyword, or quotes the specification prose, that imposes the obligation. Prose
+  that says **should** or "preferred" is never `required:`.
 
 A consumer has an obligation only where producers can now emit something that a
 conforming consumer would otherwise misread or reject, or where the meaning of
@@ -55,6 +55,24 @@ The sections do not signal obligations; the prefixes do.
 
 ### Changed
 
+- The pointer fields of an external call or contract creation `invoke`
+  (`target`, `gas`, `value`, `input`, `salt`) describe the operands that the
+  marked CALL or CREATE instruction consumes, so they resolve against the state
+  immediately before that instruction executes. This is the one exception to
+  the rule from [#281] that a context's pointers resolve after its instruction.
+  The `invoke` description had kept the earlier "trace step" sentence, which
+  contradicted that rule; the context itself stays on the call instruction
+  ([#303]).
+  - Schemas: **ethdebug/format/program/context/function/invoke**,
+    **ethdebug/format/program/instruction**,
+    **ethdebug/format/program/context/function/return**
+  - Producers: no change needed. The `invoke` examples already placed the
+    context on the call instruction with pointers to its operands.
+  - Consumers: required: resolve the pointer fields of a `message` or `create`
+    `invoke` against the state before the marked instruction executes (a new
+    exception in the `context` description). A consumer that followed the
+    `invoke` examples already does this.
+
 - A segment's `offset` is no longer limited to a value below `$wordsize`: an
   offset at or past `$wordsize` now carries into later slots. The default
   `length` is now `$wordsize - (offset mod $wordsize)`, which runs to the end of
@@ -590,3 +608,4 @@ First published version of the specification.
 [#284]: https://github.com/ethdebug/format/pull/284
 [#285]: https://github.com/ethdebug/format/pull/285
 [#286]: https://github.com/ethdebug/format/pull/286
+[#303]: https://github.com/ethdebug/format/pull/303

packages/web/spec/program/context/function/invoke.mdx

@@ -21,23 +21,30 @@ contexts to reconstruct call stacks.
 
 ## Pointer evaluation and instruction placement
 
-An instruction's context describes what is known _following_
-that instruction's execution: the fact that a function was
-invoked holds from that point forward. Pointers within the
-context reference the machine state at the instruction's trace
-step — the state a debugger observes when it encounters the
-instruction.
+An instruction's context holds _following_ that instruction's
+execution: the fact that a function was invoked holds from that
+point forward, and pointers within the context resolve against
+the machine state after the instruction has executed (see
+[instruction](/spec/program/instruction)). The operand pointers
+of an external call or contract creation are the one exception.
 
 For **internal calls**, this context is typically placed on the
-callee's entry JUMPDEST rather than the caller's JUMP. JUMP
-consumes its destination operand from the stack; at the entry
-JUMPDEST, the remaining stack (return address followed by
-arguments) is stable and directly addressable.
+callee's entry JUMPDEST. The caller's JUMP has consumed its
+destination operand by then, and JUMPDEST leaves the stack
+unchanged, so after it executes the remaining stack (return
+address followed by arguments) is stable and directly
+addressable.
 
 For **external calls** and **contract creations**, this context
 marks the CALL/DELEGATECALL/STATICCALL/CREATE/CREATE2
-instruction itself, where the call parameters are visible on
-the stack.
+instruction itself: the invocation occurs when that instruction
+executes. The pointer fields of a `message` or `create`
+invocation (`target`, `gas`, `value`, `input`, `salt`) describe
+the operands of the marked instruction, which the instruction
+consumes. These pointers therefore resolve against the machine
+state immediately **before** the marked instruction executes. A
+debugger that is paused about to execute the CALL can resolve
+them against the state it observes.
 
 <SchemaViewer
   schema={{ id: "schema:ethdebug/format/program/context/function/invoke" }}

packages/web/spec/program/context/function/return.mdx

@@ -38,11 +38,12 @@ either return normally or revert, with no separate success flag.
 
 ## External call return
 
-An external call return marks an instruction after a CALL,
-DELEGATECALL, or STATICCALL that completed successfully. The
-EVM places a success flag on the stack (1 for success, 0 for
-failure), and the callee's output is accessible via the
-returndata buffer.
+An external call return marks an instruction on the path that
+follows a CALL, DELEGATECALL, or STATICCALL that completed
+successfully. The EVM places a success flag on the stack (1 for
+success, 0 for failure), and the callee's output is accessible
+via the returndata buffer. As with any context, the pointers
+resolve against the state after the marked instruction executes.
 
 The `success` field is specific to external call returns. It
 contains a pointer to the boolean success value on the stack,

schemas/program/context/function/invoke.schema.yaml

@@ -13,22 +13,28 @@ description: |
   such as call targets, gas, value, and input data.
 
   Per the **ethdebug/format/program/instruction** schema, an
-  instruction's context describes what is known following that
-  instruction's execution: the context's semantic facts (e.g.,
-  "a function was invoked") hold from that point forward.
-  Pointers within the context reference the machine state at
-  the instruction's trace step, which is the state a debugger
-  observes when it encounters the instruction.
+  instruction's context holds following that instruction's
+  execution: the context's semantic facts (e.g., "a function was
+  invoked") hold from that point forward, and pointers within
+  the context resolve against the machine state after the
+  instruction has executed. The operand pointers of an external
+  call or contract creation are the one exception, described
+  below.
 
   For internal calls, this context is typically placed on the
-  callee's entry JUMPDEST rather than the caller's JUMP, because
-  JUMP consumes its destination operand from the stack. At the
-  entry JUMPDEST the remaining stack (return address, arguments)
-  is stable and directly addressable.
+  callee's entry JUMPDEST. The caller's JUMP has consumed its
+  destination operand by then, and JUMPDEST leaves the stack
+  unchanged, so after it executes the remaining stack (return
+  address, arguments) is stable and directly addressable.
 
   For external calls and contract creations, this context marks
   the CALL/DELEGATECALL/STATICCALL/CREATE/CREATE2 instruction
-  itself, where the call parameters are visible on the stack.
+  itself: the invocation occurs when that instruction executes.
+  The pointer fields of a `message` or `create` invocation
+  (`target`, `gas`, `value`, `input`, `salt`) describe the
+  operands of the marked instruction, which the instruction
+  consumes. These pointers therefore resolve against the machine
+  state immediately **before** the marked instruction executes.
 
 type: object
 properties:
@@ -135,6 +141,11 @@ $defs:
       DELEGATECALL, or STATICCALL. Set `delegate` or `static` to
       `true` to indicate the call variant; if neither is present
       the call is a regular CALL.
+
+      This context marks the call instruction itself. The `target`,
+      `gas`, `value`, and `input` pointers describe that
+      instruction's operands, so they resolve against the machine
+      state immediately **before** it executes.
     type: object
     properties:
       message:
@@ -214,6 +225,11 @@ $defs:
     description: |
       A contract creation via CREATE or CREATE2. The presence
       of `salt` distinguishes CREATE2 from CREATE.
+
+      This context marks the CREATE or CREATE2 instruction itself.
+      The `value`, `salt`, and `input` pointers describe that
+      instruction's operands, so they resolve against the machine
+      state immediately **before** it executes.
     type: object
     properties:
       create:
@@ -334,9 +350,10 @@ examples:
   # -----------------------------------------------------------
   # External CALL: token.balanceOf(account)
   # -----------------------------------------------------------
-  # This context marks the CALL instruction. Stack-based
-  # pointers reference the pre-execution state visible in
-  # the trace step (CALL consumes all stack operands):
+  # This context marks the CALL instruction. Its pointers
+  # describe the operands of the CALL, so they resolve against
+  # the state before the CALL executes (CALL consumes all of
+  # its stack operands):
   #
   #   slot 0: gas to forward
   #   slot 1: target contract address
@@ -379,9 +396,10 @@ examples:
   # -----------------------------------------------------------
   # This context marks a DELEGATECALL instruction in a proxy
   # contract. The call executes the implementation's code
-  # within the proxy's storage context. Stack-based pointers
-  # reference the pre-execution state (DELEGATECALL consumes
-  # all stack operands):
+  # within the proxy's storage context. The pointers describe
+  # the operands of the DELEGATECALL, so they resolve against
+  # the state before it executes (DELEGATECALL consumes all of
+  # its stack operands):
   #
   #   slot 0: gas
   #   slot 1: implementation address
@@ -409,9 +427,10 @@ examples:
   # -----------------------------------------------------------
   # CREATE2: deploying a child contract
   # -----------------------------------------------------------
-  # This context marks the CREATE2 instruction. Stack-based
-  # pointers reference the pre-execution state (CREATE2
-  # consumes all stack operands). The EVM stack layout for
+  # This context marks the CREATE2 instruction. The pointers
+  # describe the operands of the CREATE2, so they resolve
+  # against the state before it executes (CREATE2 consumes all
+  # of its stack operands). The EVM stack layout for
   # CREATE2 (top first):
   #
   #   slot 0: value  (ETH to send to the new contract)

schemas/program/context/function/return.schema.yaml

@@ -95,10 +95,11 @@ examples:
   # -----------------------------------------------------------
   # External call return: processing result of a CALL
   # -----------------------------------------------------------
-  # This context would mark an instruction after a CALL that
-  # completed successfully. The EVM places a success flag on
-  # the stack, and the callee's return data is accessible via
-  # the returndata buffer:
+  # This context would mark an instruction on the path that
+  # follows a CALL that completed successfully. The EVM places
+  # a success flag on the stack, and the callee's return data
+  # is accessible via the returndata buffer. After the marked
+  # instruction executes:
   #
   #   stack slot 0: success flag (1 = success)
   #   returndata 0x00..0x1f: ABI-encoded return value (32 bytes)

schemas/program/instruction.schema.yaml

@@ -46,7 +46,11 @@ properties:
       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).
+      (its postcondition). The one exception is the operand pointers of
+      an external call or contract creation in
+      **ethdebug/format/program/context/function/invoke**: they describe
+      what the marked instruction consumes, so they resolve against the
+      state immediately before it executes.
 
       Instruction contexts form a chain. The program-level `context` is the
       base case: the precondition that holds before the first instruction