format: fix invoke schema pointer semantics and examples#207
format: fix invoke schema pointer semantics and examples#207gnidan merged 3 commits intocall-returnfrom
Conversation
Align invoke context examples with the "following execution" semantics defined by instruction.schema.yaml. The internal call example previously referenced pre-JUMP stack state (destination at slot 0, arguments at slots 2-3), but JUMP consumes its destination operand. Fix the example to mark the callee's entry JUMPDEST with the correct post-JUMP stack layout: return label at slot 0, arguments at slots 1-2, and target as a code pointer to the function's entry offset. Also fix the CREATE2 example: salt was incorrectly shown at stack slot 1 instead of slot 3 (the EVM pops value, offset, length, salt in that order). Add clarifying text to the schema description and spec page explaining when internal call contexts use callee JUMPDEST placement vs. external call/create contexts on the instruction itself, and how stack-based pointers reference pre-execution state for instructions that consume their operands.
|
gnidan
left a comment
gnidan
left a comment
There was a problem hiding this comment.
Writer review — prose clarity and consistency.
Schema description (invoke.schema.yaml): The new paragraphs are clear and well-structured. The "Per the ethdebug/format/program/instruction schema" reference anchors the reader. Good.
Spec page (invoke.mdx) — "Pointer evaluation and instruction placement" section: Clear explanation of the internal call rationale (JUMP consumes destination, so JUMPDEST is the stable point). The internal call subsection update is consistent.
One concern — "following execution" tension for external calls: The instruction schema defines context as "known to exist following the execution of this instruction." For external calls, the new text says "stack-based pointers reference the pre-execution state visible in the trace step." These two statements are in tension: after CALL executes, the gas/target/value operands are consumed and replaced with a success flag. Pointers to slots 0-6 would reference the pre-execution layout, not the post-execution layout.
The PR body acknowledges this ("Addresses the spec contradiction"), but the prose in the schema description and spec page doesn't resolve it — it just restates both sides. The reader is told contexts describe state "following execution" and also that external call pointers reference "pre-execution state." Consider either:
- Clarifying that invoke contexts are an exception to the "following execution" rule (the context describes what was true at the point of invocation, not after)
- Or reframing "following execution" more broadly in the instruction schema to accommodate this case
This doesn't block the example/slot fixes, which are clearly correct. Just flagging the prose tension for the author's consideration.
Example fixes: The internal call stack layout (slot 0 = return label, slots 1-2 = arguments, target as code pointer) and CREATE2 salt slot fix are both correct.
gnidan
left a comment
gnidan
left a comment
There was a problem hiding this comment.
Style review: looks good.
- Line lengths all within 80 chars
- Prose tone matches the rest of the spec — direct, technical,
no filler - Terminology is consistent ("trace step", "pre-execution state",
"stack operands") and aligns with existing usage in the schema
descriptions - Example comment blocks follow the established
# ---separator
pattern - Stack layout corrections are accurate per EVM semantics
(CREATE2 now correctly shows all 4 operands: value, offset,
length, salt) - Schema description additions follow the
|multi-line format
used throughout
One minor note (not blocking): the new "Pointer evaluation and
instruction placement" section in invoke.mdx is more detailed
than the other spec pages (return.mdx, revert.mdx are minimal).
This is fine — invoke is the most complex variant and benefits
from the extra context — but worth noting the asymmetry.
Resolve the tension between "following execution" semantics and pointer evaluation. The instruction schema's "following execution" describes when a context's semantic facts hold (e.g., "a function was invoked"), not the machine state that pointers reference. Pointers reference the state at the instruction's trace step — the state a debugger observes when it encounters the instruction. Update instruction.schema.yaml to make this two-level model explicit. Simplify the invoke schema description and spec page to present this cleanly rather than restating the contradiction.
gnidan
left a comment
gnidan
left a comment
There was a problem hiding this comment.
The reframe resolves the tension cleanly. Separating "semantic facts hold from this point forward" from "pointers reference the trace step state" makes both statements true without contradiction. The spec page and schema description are now consistent. Reads well — no further concerns.
- Callee JUMPDEST: full invoke with arg pointers and code target (resolved at module-level patching) - Caller JUMP: identity + code target only, no arg pointers - Target pointers changed from stack to code location
* bugc: update invoke contexts per spec fix (#207) - Callee JUMPDEST: full invoke with arg pointers and code target (resolved at module-level patching) - Caller JUMP: identity + code target only, no arg pointers - Target pointers changed from stack to code location * fix: use Pointer.Region.isCode type guard in tests * programs-react: propagate arg names from callee JUMPDEST The invoke spec change moved argument pointers from the caller JUMP to the callee entry JUMPDEST. The call stack builder was updating argumentPointers from the duplicate callee step but not argumentNames, causing names to show as _0 instead of the actual parameter name. * web: propagate arg names from callee JUMPDEST in TraceDrawer Same fix as the programs-react mockTrace.ts change — the duplicated call stack builder in TraceDrawer.tsx also needs to update argumentNames from the callee entry step, not just argumentPointers.
1 participant
Summary
Addresses the spec contradiction where
instruction.schema.yamldefines "following execution" semantics but the invoke example referenced pre-JUMP stack state.