Phase 1, Section 13: Tuple projection

StoryLM-0 wiring slice. Not a Phase 1 exit-criteria replacement. Not a tensor operator. Names the components of an already-typed tuple.

1. What this section commits to

Section 12 returns (primal, g₀, …) from reverseMode. Section 11 updates w with an explicit g. This section lets a program name those components:

let (y, g) = handle f(w) with reverseMode in
w - lr.broadcast(shape(w)) * g

The form is a destructuring let. It is not fst / snd, not numeric field access, and not an MLIR tuple.get. The right-hand side is already a flat tensor tuple (Section 12). The left-hand side binds one identifier per component, left to right.

There is no new tensor primitive and no new FFI.

2. What this section does not commit to

Nested patterns (let (y, (g0, g1)) = …). reverseMode results are already flat.
One-element patterns (let (y) = …). The surface still cannot write a one-element tuple type.
Wildcards, ascriptions on binders, or tuple-map combinators.
Differentiating through a destructuring let. The restricted AD pass still requires a let-chain of tensor nodes ending in a Var. Projection sits outside the differentiated function (after handle f(…) with reverseMode).
Changing the seed cotangent, @main arguments, AdamW, argmax, sampling, or KV-cache.

3. Typing

Γ ⊢ e : (τ₀, …, τₙ₋₁)
n ≥ 2
names = [x₀, …, xₙ₋₁]
the xᵢ are pairwise distinct
Γ, x₀:τ₀, …, xₙ₋₁:τₙ₋₁ ⊢ e' : τ
─────────────────────────────────────────
Γ ⊢ let (x₀, …, xₙ₋₁) = e in e' : τ

Arity must match exactly. A non-tuple right-hand side is a type error. Duplicate binders are a type error.

Each τᵢ may be a tensor (the StoryLM-0 case) or any other value type the elaborator already produces. This slice does not add new component types.

Unused binders are allowed. The right-hand side is still evaluated.

4. Operational meaning / lowering

A destructuring let does not compute. After the right-hand side is emitted as m SSA values (Section 12 flatten), the binder xᵢ is that i-th SSA name in the remainder.

%y, %g = …
; xᵢ ↦ that SSA name

No tuple.get, no extra copies, no new linalg op.

5. Surface

S-expression	Bootstrap `.kina`
(not required for this slice)	`let (y, g) = e in e'`

At least two binders, comma-separated. Same in terminator as an ordinary let.

The StoryLM-0 numeric instance (LM-head layout from Section 11; neg VJP from Section 10; seed ones):

let f = fn(w: tensor<F32, [4, 8], @host>) -> tensor<F32, [4, 8], @host> {
  let y = -w in
  y
} in
let step = fn(
  w: tensor<F32, [4, 8], @host>,
  lr: tensor<F32, [1, 1], @host>
) -> tensor<F32, [4, 8], @host> {
  let (y, g) = handle f(w) with reverseMode in
  let lr_b = lr.broadcast([4, 8]) in
  let update = lr_b * g in
  w - update
} in
let w = tensor<F32, [4, 8], @host> in
let lr = tensor<F32, [1, 1], @host> in
step(w, lr)

g = -ones, so w' = w + broadcast(lr). y is bound and unused. f stays a pure tensor let-chain; projection is only in step.

6. IR

Typed IR constructor

LetTuple of string list * program * program * typ

in order (names, rhs, body, result_ty). The parser produces the surface form; the elaborator constructs LetTuple when the let pattern has two or more names. Ordinary Let is unchanged.

The AD pass rewrites children of LetTuple if that node appears outside a differentiated body. A LetTuple inside a reverseMode function body is unsupported (same failure as any non-Let/Var spine).

7. Tests

ad_sgd_step.kina — §5 program; golden accepted by mlir-opt; the step fn result is tensor<4x8xf32>.
Arity mismatch (let (y, g, h) = handle f(w) with reverseMode) is rejected.
Non-tuple right-hand side (let (y, g) = w) is rejected.
Duplicate binders are rejected.
scripts/validate_ad_sgd.py compiles the example to a .so, injects patterned w / lr, and checks w' = w + lr (NumPy; PyTorch when present). This is Kina-executed loss → VJP → SGD for that instance.

8. Open issues

Nested patterns / wildcards. Not needed while reverseMode is flat.
AD through projection. Would need VJPs for Tuple / LetTuple. Not required for StoryLM-0’s “handle, then update” shape.
AdamW as a later composition using the same naming.
Decoder-graph VJPs so the named gradient can be a gather / reshape / rank-4 matmul cotangent. Specified in Section 14.