program/context/function/invoke: external-call examples contradict the postcondition rule #302

#281 settled that an instruction's context is a postcondition, pointers included: ethdebug/format/program/instruction now says that a context's facts and "any pointers it contains resolve against the machine state after the instruction has executed", and that a debugger paused about to execute instruction i reads the context of instruction i − 1.

ethdebug/format/program/context/function/invoke still says the opposite, and its external-call examples depend on the opposite.

• Its description keeps the sentence that format: state the postcondition convention for instruction contexts #281 removed from the instruction schema: "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." The spec page (packages/web/spec/program/context/function/invoke.mdx, "Pointer evaluation and instruction placement") has the same text.
• The external CALL, DELEGATECALL and CREATE2 examples place the invoke context on the call instruction itself, with pointers to stack slots 0–2 for gas, target and value. Their comments say so directly: "Stack-based pointers reference the pre-execution state visible in the trace step (CALL consumes all stack operands)."
• The external-call example in ethdebug/format/program/context/function/return has the matching pre-state reading: it "would mark an instruction after a CALL", with the success flag in slot 0.

Concretely:

offset  op      stack after it executes (top first)
  90    PUSH..  [gas, target, value, inOff, inLen, outOff, outLen]
  91    CALL    [success]

An invoke on instruction 91 whose gas pointer is stack slot 0 is right before CALL executes and wrong after it: under the postcondition rule slot 0 holds the success flag.

Internal calls are not affected. The invoke sits on the callee's entry JUMPDEST, which leaves the stack alone, so both readings agree. The reference implementation is not affected either: bugc emits no message or create invokes. This is a problem in the schema text, the examples and the spec page only.

Options

1. Move the placement and keep one rule. An external-call or create invoke goes on the instruction immediately before the CALL/CREATE. Its postcondition is the call's precondition, so the operands are on the stack, the pointer slots in the current examples stay correct as written, and a debugger paused about to execute the CALL reads exactly that context. An external return or revert goes on the CALL itself, whose post-state has the success flag in slot 0 and the returndata set. Only descriptions and example comments change, in invoke, return, revert and the spec pages.
2. Keep the placement and state an exception. The context stays on the CALL/CREATE, and the spec says that pointers in a message or create invoke resolve against the state before the marked instruction executes. The examples stay as they are; the postcondition rule is no longer uniform, and a debugger has to special-case these contexts.

Either way the leftover "trace step" sentence has to go.

Found while auditing the spec changelog in #300.