Skip to content

docs(tech-debt): mark CORE-01 (S1) borrow-checker Phase-3 DONE — closes #177 #473

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
hyperpolymath wants to merge 1 commit into
base: main
Choose a base branch
from
+33 −14
Open

docs(tech-debt): mark CORE-01 (S1) borrow-checker Phase-3 DONE — closes #177 #473

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 33 additions & 14 deletions docs/TECH-DEBT.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) │ │
Expand Down Expand Up @@ -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
Expand Down