format: clarify inline activation reconstruction (push/pop vs membership)

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

@@ -125,7 +125,23 @@ uniform whether or not the call was inlined:
 
 - **Push** an activation when an `invoke` context is encountered
   and **pop** it when the matching `return` context is
-  encountered, in trace order.
+  encountered, in trace order. The `invoke` opens the activation
+  inclusive of its instruction; the `return` closes it after its
+  instruction, so the instruction bearing `return` is still inside
+  the activation.
+
+Because push/pop is driven by where the `invoke` and `return`
+contexts sit, a compiler must emit them as a **bracket**: the
+`invoke` on the first instruction of the body and the `return` on
+its last. A compiler must **not** duplicate `invoke` or `return`
+across a body's interior instructions — repeating them would push
+or pop spurious activations. The sole exception is a body that
+compiles to a **single instruction**, whose entry and exit
+coincide: that one instruction legitimately carries both `invoke`
+and `return`, and a debugger processes them in order (push, then
+pop). This bracket rule is what keeps the guarantee below —
+that a debugger ignoring `transform` still sees a coherent
+`invoke`/`return` pair — true for inlined calls.
 
 An inlined callee therefore appears on the call stack exactly as a
 non-inlined one does. Two kinds of activation differ only in how
@@ -147,6 +163,12 @@ transform marker — **not** by whether `target` is present:
 
 ### Activation membership
 
+Push/pop and membership answer two different questions. Push/pop
+(above) determines **when** a virtual activation is open — its
+lifetime on the call stack. Membership determines **which** open
+activation a given instruction belongs to. The two are
+independent, and a debugger uses both.
+
 An instruction belongs to the innermost open virtual activation if
 and only if its context carries an `inline` identifier in its
 transform list — so composed markers such as `["inline", "fold"]`
@@ -158,6 +180,14 @@ optimization passes may relocate or interleave an inlined body, so
 a positional "everything between the invoke and the return" rule
 would be unsound.
 
+This is why membership is separate from lifetime. An activation
+opened by an `invoke` stays open until its `return`, even across
+instructions that are **not** its members — for example, caller
+code an optimizer interleaved into the body's trace span. Such a
+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.
+
 ### Identity and values
 
 Every function-identity field (`identifier`, `declaration`,