diff --git a/docs/TECH-DEBT.adoc b/docs/TECH-DEBT.adoc index 6e64ac7..0dc0bac 100644 --- a/docs/TECH-DEBT.adoc +++ b/docs/TECH-DEBT.adoc @@ -29,7 +29,7 @@ Stage A CLOSED ───────────────────── Stage B CLOSED (#215; residual conflicts = ADR-012 won't-fix) │ Stage C CLOSED 2026-05-18 (#128/#135 stdlib AOT) │ ▼ -Stage D ACTIVE ── CORE-01 (#177) ─┐ (base lang +Stage D CLOSED ── CORE-01 (#177) ─┐ (base lang ├─ INT-01 (#178) ──────────┼─ substrate, S1 complete) ├─ INT-02 (#179) ──┐ │ ├─ INT-03 (#180) │ │ @@ -174,19 +174,38 @@ propagation). Moves/borrows from arm i no longer pollute arm i+1; 2 hermetic tests in "E2E Borrow Graph" (positive: two catch arms can independently move the same value; anti-regression: body-side moves still propagate past the try, preserving conservative correctness). -*Residual (Slices C-full / C' / D):* true Polonius origin/region -variables on `TyRef`/`TyMut` with subset constraints and a datalog- -style loan-live-at-point solver (architectural change to the type -system; ADR-gated); loop soundness via a 2-iteration check on -`StmtWhile`/`StmtFor` (coupled to a `StmtAssign` clear-on-rewrite -fix — assignment is currently treated as a read of LHS, so the -naive 2-iter spuriously fails on legitimate re-assignment loops); -reborrow through indirection (`r = some_other_ref_var` RHS, parks -with the let-graph's same restriction); tighter quantity-checker -integration for captured linears. |S1 |pt1 #240 + pt2 return-escape -+ `&mut` surface + pt3 Slices A+B+C-light DONE (Refs #177); residual -= Slices C-full (origin variables, ADR-gated), C' (loop soundness), -D (quantity integration), plus ref-to-ref binding — issue #177 +*Part 3 ref-to-ref binding LANDED* (PR #395, Refs #177): `let r2 = r` +and `r2 = r` (where `r` is a ref-binder) extend the borrow-graph by +aliasing `r2` to the same borrow `r` holds; `ref_source_borrow` unifies +`&p` / `&mut p` / ref-var cases so `record_ref_binding` and the +`StmtAssign` reborrow block both reach through one extra level of +indirection. Closes the reborrow-through-indirection gap. +*Part 3 Slice C' LANDED* (PR #396, Refs #177): loop soundness via a +2-iteration check on `StmtWhile`/`StmtFor`. Body runs once; state-fields +snapshot; cond+body run again from the post-iter-1 state. Body-moves +that aren't restored surface as `UseAfterMove` on the 2nd pass. Pairs +with `StmtAssign` clear-on-rewrite (PR #399 `is_whole_place_write`) so +legitimate re-init loops accept while loops with unrestored body-move +reject. *Part 3 Slice D LANDED* (PR #397, Refs #177): borrow-side +rejection of `@linear`-binding capture by a closure. Closures may be +called 0..N times, so capturing a `@linear`/`QOne` binding lifts its +consumption count out of the borrow checker's finite-once proof. +`state.linear_bindings` populated from `[@linear]` / `Cmd _` annotations +on params, `let`-statements, and `let`-expressions; `ExprLambda` +rejects free-vars whose sym-id is in that set with +`LinearCapturedByClosure` (errors at the lambda span, before the +downstream quantity-checker `QOmega`-scaled "used multiple times" +diagnostic). *Residual:* true Polonius origin/region variables on +`TyRef`/`TyMut` with subset constraints and a datalog-style loan- +live-at-point solver — architectural change to the type system, +covered by ADR-022 (`docs/decisions/0022-polonius-origin-variables.adoc`, +PR #407) as a separate workstream; lexical checker is the merge oracle +through M3 per the ADR migration plan. Tighter quantity-checker +integration for captured linears is a small remaining nicety, not a +soundness gap. |S1 |*CLOSED 2026-05-30* (#177) — pt1 #240 + pt2 +return-escape + `&mut` surface + pt3 Slices A+B+C-light+C'+D + ref-to- +ref binding DONE; residual Polonius work is ADR-022 (#407), a separate +workstream |CORE-02 |Effect-handler dispatch on WasmGC (was `UnsupportedFeature`; the chosen path is CPS over the EH proposal). The #225 CPS line closed the async slice; #234 generalised the boundary recogniser from a