format: resolve external-call invoke operands before the instruction

[gnidan]

#281 made instruction contexts postconditions, pointers included. ethdebug/format/program/context/function/invoke kept the sentence that placed pointers "at the instruction's trace step", and its CALL, DELEGATECALL and CREATE2 examples point at stack operands that those instructions consume, so the examples were wrong under the rule that the instruction schema states.

The invoke context stays on the call instruction, because the invocation occurs when that instruction executes. What changes is the stated reading of its pointer fields: target, gas, value, input and salt of a message or create invocation describe the operands of the marked instruction, so they resolve against the machine state immediately before it executes. This is the same shape as DWARF call-site parameters, whose values are defined at the time of the call. ethdebug/format/program/instruction now names this as the one exception to the postcondition rule. Internal calls need no exception: the invoke sits on the callee's entry JUMPDEST, which leaves the stack unchanged.

• invoke — the description and the ExternalCall and ContractCreation definitions state the operand rule; the example comments say "the state before the CALL executes" rather than "the pre-execution state visible in the trace step". The JUMPDEST guidance is reworded to stand under postconditions.
• instruction — the context description points at the exception.
• return — the external-call example no longer leans on the pre-state reading: its pointers resolve after the marked instruction, as with any context.
• The spec pages for invoke and return carry the same wording.

No schema keyword changes, and no example value changes. No producer emits message or create invokes today (bugc emits internal calls only; solc emits no function contexts yet), and no consumer resolves these pointers (soldb reads only identifier, declaration and activation), so nothing in the reference implementation needs to follow.

The spec changelog gets an Unreleased entry: no change for producers, and required: for consumers, who resolve these operand pointers before the marked instruction. It also re-wraps one overlong line in the changelog intro.

Fixes #302

[github-actions]

PR Preview Action v1.8.1
Preview removed because the pull request was closed.
2026-09-17 06:30 UTC