format: correct activation correlation — activation id inside invoke/return/revert, scope name to pick

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
 

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.
 
 <SchemaViewer schema={{ id: "schema:ethdebug/format/program/context/name" }} />
-
-## 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.

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)

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:

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:

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<T=bytes32>"
   # example: distinguishing a `pick` alternative
   - name: "storage-layout-v2"
+  # example: naming a generic instantiation
+  - name: "Array<T=bytes32>"