docs: truth CORE-01 part 1 (PR #240) in the ledger (Refs #175 #176 #177)

CORE-01 borrow-graph validation part 1 landed via PR #240. Keep the
authoritative docs in lockstep (DOC-01..09 / #176 — "docs current as you
go"):
- CAPABILITY-MATRIX.adoc borrow row: graph validation landed; remaining
  NLL/flow-sensitive deferred to part 2+.
- TECH-DEBT.adoc CORE-01: part 1 LANDED (PR #240); part 2+ scoped.
- STATE.a2ml borrow-checker feature line updated (it mirrors).

Each file stays single-owner: the compiler change is PR #240 off main;
these doc/ledger files are owned by this branch (#239).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -66,7 +66,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-in-progress (see lib/borrow.ml [IMPL-DEP: Phase 3])"
+borrow-checker = "phase-3-part-1-landed (CORE-01, PR #240 Refs #177, 2026-05-19, 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. Part 2+ deferred: NLL/region inference, flow-sensitive escape via `outer = &x`, tighter quantity integration. 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

@@ -79,12 +79,16 @@ enforced. Handlers: *interpreter-complete*; WasmGC dispatch is
 `UnsupportedFeature` pending the EH proposal or the CPS transform (the #225
 CPS line is closing the async slice of this).
 
-|Borrow checker |*partial — known soundness gap* |Place/borrow/move infra +
-use-after-move, conflicting-borrow-at-creation, move-while-borrowed,
-lambda-capture. *Borrow-graph validation is incomplete*: `BorrowOutlivesOwner`
-is defined but never emitted; shared-XOR-exclusive is not enforced at plain
-use sites. Some medium-severity aliasing bugs are not caught. This is
-CORE-01 (issue #177) — the one named base-language soundness gap.
+|Borrow checker |*partial — graph validation landed (CORE-01 pt 1)* |
+Place/borrow/move infra + use-after-move, conflicting-borrow,
+move-while-borrowed, lambda-capture. *CORE-01 part 1* (PR #240, Refs #177,
+gate 263/263): borrow-graph validation wired — `BorrowOutlivesOwner` now
+emitted (`&local` escaping its block); shared-XOR-exclusive enforced at
+*use* sites (`UseWhileExclusivelyBorrowed`); ownership now derived from the
+parameter *type* (`TyOwn/TyRef/TyMut`) so the owned/ref/mut discipline is
+actually enforced from real parsed source (closed a latent hole); call-arg
+borrows made temporary. *Deferred (CORE-01 pt 2+):* NLL/region inference,
+flow-sensitive escape via `outer = &x`, tighter quantity integration.
 
 |Quantity / affine types |*enforced* |QTT semiring in `lib/quantity.ml`,
 invoked inside the standard CLI pipeline. `@linear`/`@erased`/`@unrestricted`

docs/TECH-DEBT.adoc

@@ -81,12 +81,15 @@ MONITOR enforcement (DOC-08/09): any PR re-introducing backend-breadth,
 |===
 |ID |Item |Sev |Status
 
-|CORE-01 |Complete borrow-checker Phase-3 — borrow-graph validation.
-`lib/borrow.ml` has place/borrow/move infra but graph validation is
-incomplete: `BorrowOutlivesOwner` defined-but-never-emitted;
-shared-XOR-exclusive only enforced at borrow creation, not at use sites;
-medium-severity aliasing bugs uncaught. Add graph validation + regression
-fixtures. |S1 |open — issue #177; *next work unit* (user: soundness-first)
+|CORE-01 |Borrow-checker Phase-3 — borrow-graph validation. *Part 1
+LANDED* (PR #240, Refs #177, gate 263/263): `BorrowOutlivesOwner` emitted;
+shared-XOR-exclusive enforced at use sites
+(`UseWhileExclusivelyBorrowed`); ownership derived from the 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. *Part 2+ deferred:* NLL/region inference
+(Polonius), flow-sensitive escape via `outer = &x`, tighter quantity
+integration. |S1 |pt1 in PR #240 (open); pt2+ open — issue #177
 |CORE-02 |Effect-handler dispatch on WasmGC (currently `UnsupportedFeature`;
 EH proposal or CPS). The #225 CPS line closes the async slice. |S2 |partial
 (PR3a/b/c merged; #234 generalises the recogniser)