docs: refresh STATE.a2ml + ROADMAP after 2026-06-01/02 proof + stdlib wave

.machine_readable/6a2/STATE.a2ml

@@ -7,8 +7,8 @@
 @state(version="2.0"):
 phase: "implementation"
 next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
-last_action: "Phase D slice 4 Phase 3b Stage 1b LANDED (2026-05-30 PM, this PR): elegance-first path-(i) substitution-lemma + L2 β wrapper, zero axioms. (1) Syntax.v: `expr_closed_below : nat -> expr -> bool` Fixpoint (canonical CS predicate, bool per post-redesign convention); `closed_below_shift_id` (closed terms shift-invariant); `expr_closed_below_shift_mono` (closure survives shifting); `ctx_mark_used_app_lt` (mark_used commutes with context append). (2) Semantics_L1.v: `closed_below_k_typing_outer_tail_irrelevant_l1_m` (the body-transfer core — structural induction over 28+ typing rules; closed-below-k terms' typing depends only on G's first k positions); `closed_value_typing_G_poly_l1_m` (any-G' form per elegance-first 'state what's actually true'); `closed_value_typing_RG_poly_l1_m` (combined RG-poly via chain to tfuneff_lambda_retype_l1_m); `closed_value_shift_id_l1_m` (cutoff-0 wrapper); `value_TFunEff_R_subset_R_in_l1_m` (extracts R ⊆ R_in from TFunEff value typing); `sub_R_in_R_in_via_value_l1_m` (chain helper packaging count_occ_le_l1_m + R-subset for compound-rule call sites); `subst_typing_gen_l1_m_tfuneff` (~300 lines mirroring Phase 2's ground-nonlinear template; inner T_Lam_L1_*_Eff cases discharge via P1 discriminate; compound rules use closed_value_typing_RG_poly_l1_m + sub_R_in_R_in_via_value_l1_m for the G-mismatch). (3) TypingL2.v: `preservation_l2_app_eff_beta_tfuneff_l1` (β-case kernel) + `preservation_l2_app_eff_beta_tfuneff` (L2 wrapper) under the three-condition statement (P1 leaf-only + P2 regions ⊆ R_in_v + P3 closure of v2). Build oracle: coqc 8.18.0 clean across all 12 .v files; Print Assumptions on every new Qed lemma reports 'Closed under the global context' (zero new admits / axioms). Owner-directive compliance: ✅ no Semantics.v / Typing.v / Counterexample.v touch; ✅ no residual Semantics_L1.v admit closure attempted; ✅ anti-pattern detector clean. Design decisions baked in per elegance-first priority: bool predicate (matches post-redesign style), any-G' statement form (the genuinely true claim), P1 RETAINED (re-staging is owner territory), staging-as-is (PR-level decisions don't deviate from owner-approved 4-stage plan)."
-updated: 2026-05-30T20:00:00Z
+last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02."
+updated: 2026-06-02T13:30:00Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,

ROADMAP.adoc

@@ -11,14 +11,25 @@ _Linear-type language with dual formalisation (Coq + Idris2) targeting WebAssemb
 
 toc::[]
 
-== Status snapshot (2026-05-20)
+== Status snapshot (2026-06-02)
 
 Ephapax is an early-development linear-type language implemented across
 ~19 Rust crates with a two-phase compiler pipeline (Idris2 type-checking
 → Rust/WASM backend). Lexer, parser, interpreter, REPL, CLI, S-expression
 IR, two-phase pipeline, Zig FFI, and conformance test suite are
 complete. Type checker and WASM code generation are in progress.
 
+2026-06-01 → 02 proof + stdlib wave (13 PRs): canonical-forms L1
+modality-polymorphic (P43, axiom-free, prerequisite for `progress_l1`);
+Print Assumptions audit framework across L1 + L3 keystones (P10/P32);
+`step_pop_disjoint_from_type_l1` stated + EASY cases (P06, HARD cases
+blocked on issues #240/#241/#242); Rust↔Coq `is_linear_ty` bridge truth-
+table (P28); OwnershipKind from_byte/to_byte round-trip (P59, typed-wasm
+ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions
+(D04), Allen's interval algebra (D11), MessageHandle (D17), monoidal
+aggregates (D18). Stages 2-4 of the Phase 3b plan (#240/#241/#242) remain
+un-touched. See `CHANGELOG.md` for full enumeration and per-PR detail.
+
 == Four-layer redesign (2026-05-26 → )
 
 The verified preservation counterexample