diff --git a/packages/web/spec/program/context/function/invoke.mdx b/packages/web/spec/program/context/function/invoke.mdx
index 76da58aff..ffe2bc998 100644
--- a/packages/web/spec/program/context/function/invoke.mdx
+++ b/packages/web/spec/program/context/function/invoke.mdx
@@ -188,42 +188,40 @@ non-member instruction (no `inline` marker for that depth) is
attributed to the enclosing activation, not the inlined one, even
while the virtual activation remains on the stack.
-### Correlating with `name`
-
-The push/pop and membership rules above reconstruct activations
-without any correlation identifier: they rely on `invoke`/`return`
-appearing in a well-nested order and on the `inline` marker to
-attribute instructions. That is sufficient for typical compiler
-output. It has two blind spots, both arising because the marker
-alone can't tell one activation from another of the same function:
-
-- **Adjacent activations of the same function.** Two inlined
- copies of the same callee placed back-to-back, with no
- intervening caller instruction, read as one activation to a
- debugger that groups a consecutive run of `inline`-marked
- instructions.
-- **Reordered or interleaved bodies.** An optimizer that moves a
- `return` marker ahead of its `invoke`, or interleaves two
- activations non-nested, defeats strict push/pop pairing.
-
-A [`name`](/spec/program/context/name) closes both. When an
-`invoke` context carries a `name`, it **declares** that activation;
-the matching `return`, and the body instructions that belong to it,
-carry the same `name` to **reference** it. Because each name is
-declared by exactly one `invoke`, the pairing is explicit and
-order-independent: adjacent same-function activations have distinct
-names, and a reference resolves to its declaration regardless of
-trace order.
-
-When names are present they are **authoritative** for activation
-structure — which `invoke` pairs with which `return`, and which
-instructions belong to which activation. Push/pop, the `inline`
-marker, and the marker-count depth remain the fallback a name-less
-debugger uses; in well-nested output the two agree. Where they
-cannot — the two blind spots above — the names are correct. A
-compiler that emits names should therefore keep them consistent
-with the push/pop structure wherever both are determinate, so the
-two views never silently disagree.
+### Correlating with `activation`
+
+The push/pop rule above reconstructs the call stack without any
+correlation identifier: it relies on `invoke`/`return` appearing
+in a well-nested order. That is sufficient for typical compiler
+output, but it has a blind spot — push/pop alone can't tell one
+activation from another of the same function, so two inlined
+copies of a callee placed back-to-back, or an optimizer that moves
+a `return` ahead of its `invoke`, can defeat strict pairing.
+
+An **`activation`** identifier closes it. The `invoke` object that
+opens an activation and the `return` (or `revert`) that closes it
+carry the same `activation` value; distinct activations carry
+distinct values. Pairing is then explicit and order-independent —
+matching values pair an invoke with its return regardless of trace
+order, and adjacent same-function activations stay distinct because
+their identifiers differ.
+
+Unlike function [identity](#identity-and-values) (which function
+this is), `activation` identifies _which activation instance_ this
+is, so it lives **inside** the `invoke`/`return`/`revert` object
+rather than as a sibling context. Two activation facts on one instruction
+— a tail call's back-edge, which both returns from one activation
+and invokes the next — therefore stay flat, each fact carrying its
+own `activation` value, with no `gather` required.
+
+When `activation` is present it is **authoritative** for pairing —
+which `invoke` matches which `return`. Push/pop remains the fallback
+an identifier-less debugger uses; in well-nested output the two
+agree. Membership — which instructions belong to a virtual
+activation — is unaffected: it stays the per-instruction
+[`inline` marker](#activation-membership). Attributing a body that
+an optimizer relocated to a _specific_ activation would need a
+membership-level identifier; that is out of scope here.
### Identity and values
diff --git a/packages/web/spec/program/context/name.mdx b/packages/web/spec/program/context/name.mdx
index 7a247d5d6..ae28ad17e 100644
--- a/packages/web/spec/program/context/name.mdx
+++ b/packages/web/spec/program/context/name.mdx
@@ -6,58 +6,16 @@ import SchemaViewer from "@site/src/components/SchemaViewer";
# Named contexts
-A context may carry a `name`: a machine-generated identifier that gives
-the context a stable identity other contexts can reference. A name is
-what makes a **cross-context reference** possible — one context declares
-a name, and another points back to it by the same name.
-
-Names are opaque strings; the format imposes no structure on them.
-Within a single program — one [`instructions`](/spec/program)
-sequence — each name **must** be declared by exactly one context; no
-two contexts may declare the same name. Other contexts may reference
-that name freely — that repetition is how they point back — and every
-reference resolves to the single declaring context. Compilers
-**should** also choose names that are meaningful to debugger users.
+A context may carry a `name`: the identifier a
+[`pick`](/spec/program/context/pick) uses to select it. Inside a `pick`,
+several contexts may apply at a given point in execution and runtime
+information is needed to select which one is active; a `name` on each
+alternative gives the selection a stable handle for the chosen
+alternative.
+
+Names are opaque strings; the format imposes no structure on them. A
+name need only be distinct among the alternatives a `pick` must choose
+between, so that the selection is unambiguous. Compilers **should**
+choose names that are meaningful to debugger users.
-
-## Uses
-
-### Selecting `pick` alternatives
-
-Inside a [`pick`](/spec/program/context/pick), several contexts may apply
-at a given point in execution and runtime information is needed to select
-which one is active. A `name` on each alternative gives the selection
-a stable handle for the chosen alternative.
-
-### Correlating an invocation with its return
-
-A `name` lets a function invocation and its return be paired directly.
-An [`invoke`](/spec/program/context/function/invoke) context **declares**
-an activation's name; the matching
-[`return`](/spec/program/context/function/return) context — and the
-instructions belonging to that activation's body — **reference** it by
-the same name.
-
-This declaration/reference split follows the format's general
-reference-by-name idiom (as a
-[pointer template](/spec/pointer/collection/templates) is declared
-once and referenced elsewhere). It pairs a call with its return
-without relying on the trace
-being strictly nested: even when optimization reorders or interleaves
-code so that a naive "innermost open activation" rule would mispair
-them, the shared name resolves the pairing unambiguously. When two
-inlined copies of the same function appear back-to-back, their distinct
-names keep them distinct activations.
-
-Because a single context object can hold at most one `name`, two
-activation facts that must carry **different** names at the same
-instruction — for example a tail call, where one instruction both
-returns from the current activation and invokes the next — are expressed
-with a [`gather`](/spec/program/context/gather) whose members each carry
-their own name. The naming granularity therefore tracks the structure of
-the contexts themselves.
-
-See the invoke context's
-[Reconstructing activations](/spec/program/context/function/invoke#reconstructing-activations)
-for how a debugger uses these names to rebuild the call stack.
diff --git a/schemas/program/context/function/invoke.schema.yaml b/schemas/program/context/function/invoke.schema.yaml
index ebb824d07..b9d987056 100644
--- a/schemas/program/context/function/invoke.schema.yaml
+++ b/schemas/program/context/function/invoke.schema.yaml
@@ -43,6 +43,20 @@ properties:
$ref: "schema:ethdebug/format/program/context/function"
+ properties:
+ activation:
+ type: string
+ title: Activation identifier
+ description: |
+ Correlation identifier for the activation this
+ invocation opens. The `return` or `revert` that ends the
+ same activation carries this same value; distinct
+ activations carry distinct values, unique within the
+ program. Lets a debugger pair an invocation with its
+ return independent of trace order — disambiguating
+ adjacent inlined activations of the same function and
+ surviving optimizer reordering. Optional.
+
allOf:
- oneOf:
- required: [jump]
@@ -310,6 +324,10 @@ examples:
offset: 128
length: 95
jump: true
+ # Correlation id: the matching inlined `return` carries the
+ # same value, so the two pair even if `transfer` is inlined
+ # at several sites.
+ activation: "transfer#0"
# -----------------------------------------------------------
# External CALL: token.balanceOf(account)
diff --git a/schemas/program/context/function/return.schema.yaml b/schemas/program/context/function/return.schema.yaml
index 4a4376048..1be5e4864 100644
--- a/schemas/program/context/function/return.schema.yaml
+++ b/schemas/program/context/function/return.schema.yaml
@@ -49,6 +49,17 @@ properties:
required:
- pointer
+ activation:
+ type: string
+ title: Activation identifier
+ description: |
+ Correlation identifier for the activation this return
+ ends. Matches the `activation` on the `invoke` that
+ opened the same activation; distinct activations carry
+ distinct values, unique within the program. Lets a
+ debugger pair a return with its invocation independent
+ of trace order. Optional.
+
unevaluatedProperties: false
required:
diff --git a/schemas/program/context/function/revert.schema.yaml b/schemas/program/context/function/revert.schema.yaml
index 9aecc9026..5a3585783 100644
--- a/schemas/program/context/function/revert.schema.yaml
+++ b/schemas/program/context/function/revert.schema.yaml
@@ -37,6 +37,17 @@ properties:
(e.g., Solidity uses codes like 0x11 for arithmetic
overflow).
+ activation:
+ type: string
+ title: Activation identifier
+ description: |
+ Correlation identifier for the activation this revert
+ ends. Matches the `activation` on the `invoke` that
+ opened the same activation; distinct activations carry
+ distinct values, unique within the program. Lets a
+ debugger pair an abnormal exit with its invocation
+ independent of trace order. Optional.
+
unevaluatedProperties: false
required:
diff --git a/schemas/program/context/name.schema.yaml b/schemas/program/context/name.schema.yaml
index c9830fc1f..9b93ef906 100644
--- a/schemas/program/context/name.schema.yaml
+++ b/schemas/program/context/name.schema.yaml
@@ -3,31 +3,18 @@ $id: "schema:ethdebug/format/program/context/name"
title: ethdebug/format/program/context/name
description: |
- A machine-generated identifier for this context that other
- contexts may reference by name.
+ The identifier a `pick` uses to select this context.
- A `name` gives a context a stable identity that the rest of a
- program's debug information can point back to. This is what makes
- cross-context references possible. Uses include:
-
- - **Selecting `pick` alternatives.** Several contexts may apply
- at a point in execution; a `name` identifies which alternative
- is active, so runtime information can select it.
- - **Correlating an invocation with its return.** An `invoke`
- context *declares* an activation's name; the matching `return`
- context — and the instructions belonging to that activation —
- *reference* it by the same name. This pairs a call with its
- return directly, without relying on the trace being strictly
- nested (see the invoke context's activation-reconstruction
- guidance).
+ Inside a `pick`, several contexts may apply at a point in
+ execution and runtime information is needed to select which one
+ is active. A `name` on each alternative gives the selection a
+ stable handle for the chosen alternative.
Names are opaque strings; the format imposes no structure on
- them. Within a single program — one **instructions** sequence —
- each name **must** be declared by exactly one context; no two
- contexts may declare the same name. Other contexts may reference
- that name freely, and every reference resolves to the single
- declaring context. Compilers **should** also choose names that
- are meaningful to debugger users.
+ them. A name need only be distinct among the alternatives a
+ `pick` must choose between, so that the selection is unambiguous.
+ Compilers **should** choose names that are meaningful to debugger
+ users.
type: object
properties:
@@ -37,10 +24,7 @@ required:
- name
examples:
- # example: declaring an inlined activation, referenced by its
- # matching return and by the instructions of the inlined body
- - name: "inline-0"
- # example: naming a generic instantiation
- - name: "Array"
# example: distinguishing a `pick` alternative
- name: "storage-layout-v2"
+ # example: naming a generic instantiation
+ - name: "Array"