Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments

[hyperpolymath]

Stage 2 of the 4-stage Phase 3b resolution plan per #235. Parallel track — L4-driven independent of Stage 1. Owner-approved 2026-05-30.

Motivation

Phase 3b's design gap (#235) traces to a deeper L4 question: should TFunEff's R_in / R_out slots be type-level only (current state — derived from typing premises) or program-level commitments (the L4 ProgramMode labelling vector)?

L4's existing direction — type-level commitments become program-level — aligns with extending ELam to carry R_in / R_out syntactically. Stage 2 makes that extension.

AST change

(* before *)
| ELam : ty -> expr -> expr

(* after *)
| ELam : ty -> region_env -> region_env -> expr -> expr
        (*  T_param  R_in        R_out      body  *)

Required cascading changes

Layer	Change
formal/Syntax.v	ELam constructor + Fixpoints (free_vars, shift, subst, regions_introduced_by)
formal/Syntax.v	NEW declared_lambda_r_ins : expr -> list region_name Fixpoint (Stage 3 dependency)
formal/TypingL1.v	T_Lam_L1_* and T_Lam_L1_*_Eff rules: premise enforces annotation matches body's actual R_in/R_out (no drift). Programs using non-Eff lambdas can default to R_in = R, R_out = R (or [] if cleaner).
formal/Semantics.v	NOT TOUCHED per owner directive — legacy judgment stays.
formal/Semantics_L1.v	inversion (T_Lam_L1_*) patterns (~28 cases): mechanical update for the new arity. Existing proofs stay Qed.
formal/TypingL2.v	T_App_L2_Eff β-case inversion: pulls R_in/R_out from the syntactic annotation rather than the typing premise (proof simplifies).
lib/borrow.ml / Rust crates	ELam constructor in Rust AST + OCaml parser. Cross-language sync.
Codegen	typed-wasm emitter: encode R_in/R_out in the lambda's metadata (or no-op if metadata already type-derived).

Drift prevention

The typing rule premise enforces annotation ≡ derived R_in/R_out. Shifted/substituted lambdas keep their annotation (it's syntax — shift/subst pass through). Any operation that would CHANGE R_in/R_out (e.g. region-substitution during reduction) must update the annotation accordingly.

Migration path

Optional NEW constructor EAnnotLam could ship first as a graceful migration if breaking existing programs is undesirable. Owner decision: bigbang vs phased AST migration.

Out of scope

• Phase 3b lemma changes: those are Stage 3 (#TBD).
• Unconditional preservation_l2: Stage 4 (#TBD).
• Stage 2 ships only the AST + typing-rule + downstream cascading. Phase 3b's lemma continues to use Stage 1's tfuneff_lambda_free until Stage 3.

Owner-directive compliance

• ✅ Modifies TypingL1.v (post-redesign judgment) — not Typing.v (legacy).
• ✅ Does NOT touch Semantics.v / Counterexample.v (legacy).
• ✅ Does NOT introduce Axiom or Admitted.
• L4-aligned per formal/PRESERVATION-DESIGN.md §7.

References

• Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases #235 — Phase 3b design-gap finding (parent).
• formal/L4.v + formal/L4-DYADIC.md — L4 ProgramMode labelling discipline.
• formal/PRESERVATION-DESIGN.md §7 — L4 design vision.
• feedback_zig_apis_ffis_idris2_abis memory — boundary-tool philosophy (annotations as ABI commitments).

🤖 Generated with Claude Code

[hyperpolymath]

Cross-references resolved

• Stage 1: Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239 — leaf-only Phase 3b. Lands first; no dependency on this issue.
• Stage 2 (this issue): Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240 — ELam annotation extension. Parallel L4 track.
• Stage 3: Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241 — relaxed Phase 3b via declared_lambda_r_ins + CPS. Blocked on this issue.
• Stage 4: Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2 #242 — compound non-linear + unconditional preservation_l2.

Parent finding: #235.