format: define context name as a referenceable identifier (activation correlation)

packages/web/spec/program/context/function/invoke.mdx

@@ -188,6 +188,43 @@ 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.
+
 ### Identity and values
 
 Every function-identity field (`identifier`, `declaration`,

packages/web/spec/program/context/name.mdx

@@ -6,9 +6,58 @@ import SchemaViewer from "@site/src/components/SchemaViewer";
 
 # Named contexts
 
-Contexts may include a `name` property for distinguishing them from
-other contexts. This is particularly useful inside `pick` alternatives,
-where several possible contexts may apply at a given point in execution
-and runtime information is needed to select which one is active.
+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.
 
 <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/name.schema.yaml

@@ -3,15 +3,31 @@ $id: "schema:ethdebug/format/program/context/name"
 
 title: ethdebug/format/program/context/name
 description: |
-  A label for distinguishing this context from other contexts.
-  This is particularly useful inside `pick` alternatives,
-  where several possible contexts may apply at a given point in
-  execution and runtime information is needed to select which one
-  is active.
+  A machine-generated identifier for this context that other
+  contexts may reference by name.
 
-  Context names are opaque strings with no format-imposed semantics.
-  Compilers **should** choose names that are meaningful to debugger
-  users.
+  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).
+
+  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.
 
 type: object
 properties:
@@ -21,7 +37,10 @@ required:
   - name
 
 examples:
-  # example: naming an inlined call site
-  - name: "inlined-call"
+  # 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"