PR #351 documentation changes only (TECH-DEBT-alt, CAPABILITY-MATRIX, STATE.a2ml)

Extracted doc-only changes from PR #351 to avoid merge conflicts.
TECH-DEBT.adoc renamed to TECH-DEBT-alt.adoc per user request.

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -71,7 +71,7 @@ test-files = 54
 # the feature is not enforced on user programs through the CLI pipeline.
 affine-types = "wired-and-reachable (Track A Manhattan plan complete 2026-04-10. Quantity semiring in lib/quantity.ml; invoked from typecheck.ml:1206 inside the standard CLI pipeline. Surface syntax per ADR-007 hybrid: @linear/@erased/@unrestricted attributes (Option C primary) on let/stmt-let/param/lambda-param, AND :1/:0/:ω numeric sugar (Option B) on let/stmt-let. Scaled Let rule per ADR-002 implemented in lib/quantity.ml ExprLet/StmtLet — closes BUG-001 (ω-let smuggles linear values) and BUG-002 (zero-let erasure). Four regression fixtures in test/e2e/fixtures/ exercise both surface forms. Behavioural enforcement verified via E2E Quantity test suite — 4 new passing tests, 0 regressions.)"
 linear-arrows = "enforced (2026-04-11): Three-part fix landed. (1) typecheck.ml lambda synth: |@linear x: T| e now synthesises T -[1]-> U (was always QOmega). (2) typecheck.ml lambda check mode: explicit param quantity annotation validated against expected TArrow quantity; unannotated params inherit context quantity. (3) quantity.ml ExprLambda: added env.errors accumulator; annotated lambda params declared via env_declare so env_use tracks them; usage verified with check_quantity after body walk; violations pushed to env.errors and drained at end of check_function_quantities (step 4). Saved/restored env.quantities entries to prevent scope leakage. Two E2E fixtures + 2 passing tests. 75 tests total, 0 regressions. Commit d2f9b7b pushed."
-borrow-checker = "phase-3-part-3-slice-A-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted (&local escaping its block), shared-XOR-exclusive enforced at use sites (UseWhileExclusivelyBorrowed), ownership derived from param type TyOwn/TyRef/TyMut (owned/ref/mut discipline now enforced from real parsed source — closed a latent hole), call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape (return-of-ref-rooted-at-callee-owned-binding caught) + &mut e parser surface (zero Menhir conflict delta — exclusive borrow finally expressible from real source). pt3 Slice A NLL last-use expiry: forward pre-pass compute_last_use_index maps each symbol to its greatest mentioning statement index; check_block expires ref-bindings introduced in-block once their binder is dead, releasing the underlying borrow. Unblocks `let r = &x; print(*r); x = 2` and `let m = &mut x; let y = *m; x` while still rejecting same-block live aliasing (2 positive + 1 anti-regression hermetic tests in E2E Borrow Graph). Residual (Slices B–D): flow-sensitive escape via `outer = &x`, origin/region variables (Polonius surface) + loan-live-at-point dataflow across CFG joins, tighter quantity integration. Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT.adoc CORE-01."
+borrow-checker = "phase-3-parts-1-3-Slices-A-and-B-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted (&local escaping its block), shared-XOR-exclusive enforced at use sites (UseWhileExclusivelyBorrowed), ownership derived from param type TyOwn/TyRef/TyMut, call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape + &mut e parser surface (zero Menhir conflict delta — exclusive borrow finally expressible from real source). pt3 Slice A (PR #335) NLL last-use expiry: forward pre-pass compute_last_use_index maps each symbol to its greatest mentioning statement index; check_block expires ref-bindings introduced in-block once their binder is dead. Unblocks `let r = &x; print(*r); x = 2` and `let m = &mut x; let y = *m; x` (2 positive + 1 anti-regression in E2E Borrow Graph). pt3 Slice B (this PR) flow-sensitive escape via re-assignment: `outer = &y` in StmtAssign now pre-releases the held borrow and re-binds the (binder → new_borrow) ref-graph entry to the freshly-created borrow, so NLL last-use + return-escape see the *current* referent. 3 hermetic tests (2 positive + 1 anti-regression). Residual (Slices C–D): origin/region variables (Polonius surface) + loan-live-at-point dataflow for CFG joins in ExprHandle/ExprTry/loops; tighter quantity integration for captured linears; reborrow through indirection (RHS that is a ref-typed value rather than a direct &place). Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT.adoc CORE-01."
 row-polymorphism = "60% (records + effects rows implemented in typecheck/unify; not fully exercised end-to-end)"
 effects = "interpreter-complete (handler dispatch, PerformEffect propagation, ExprResume, multi-arg ops all wired in interp.ml 2026-04-11). WasmGC: ops registered as unreachable stubs; ExprHandle/ExprResume reject with UnsupportedFeature — full WASM dispatch needs EH proposal or CPS transform."
 dependent-types = "parse-only (TRefined AST node exists and refinement predicates parse, but predicates do not reduce; no SMT/decision procedure wired in)"

docs/CAPABILITY-MATRIX.adoc

@@ -100,10 +100,17 @@ ref-bindings expire at their binder's *last use*, not at block exit
 (`compute_last_use_index` pre-pass + per-statement expiry in
 `check_block`). Patterns like `let r = &x; print(*r); x = 2` and
 `let m = &mut x; let y = *m; x` now type-check, while still-live borrows
-continue to block aliasing assignments. *Deferred (Slices B–D):*
-flow-sensitive escape via `outer = &x`; origin/region variables
-(Polonius surface) + loan-live-at-point dataflow across CFG joins;
-tighter quantity integration for captured linears.
+continue to block aliasing assignments. *Part 3 Slice B* (Refs #177):
+flow-sensitive escape via re-assignment — `outer = &y` in `StmtAssign`
+now pre-releases the held borrow and re-binds the
+`(binder -> new_borrow)` ref-graph entry to the freshly-created borrow,
+so the NLL last-use + return-escape analyses see the *current* referent
+after re-assignment, not the stale original (3 hermetic tests: old
+released, new tracked by NLL, anti-regression that new borrow still
+protects). *Deferred (Slices C–D):* origin/region variables (Polonius
+surface) + loan-live-at-point dataflow across CFG joins for
+`ExprHandle`/`ExprTry`/loops; tighter quantity integration for captured
+linears; reborrow through indirection (RHS not a direct `&place`).
 
 |Quantity / affine types |*enforced* |QTT semiring in `lib/quantity.ml`,
 invoked inside the standard CLI pipeline. `@linear`/`@erased`/`@unrestricted`