Skip to content

Commit 8b040aa

Browse files
committed
Merge origin/main into claude/upbeat-gauss-D5f72
Reconciles PR #336 (CORE-02 / #234 / ADR-016 truth ledger to DELIVERED) with two intervening main commits: f45afa1 feat(borrow): NLL last-use expiry for ref-bindings (CORE-01 pt3 Slice A, Refs #177) (#335) 99ae5e3 feat(stdlib): STDLIB-04a — Mut effect externs (make_ref/get/set) → real impl (Closes #328) (#334) Single conflict, docs/TECH-DEBT.adoc — HEAD updated CORE-02 (now CLOSED 2026-05-19 with full ADR-016 S1..S4 narrative); origin/main (#335) updated CORE-01 (Part 3 Slice A NLL last-use expiry LANDED). Independent adjacent rows; resolution takes both — neither side loses information. The PR's comment edits in lib/codegen.ml, lib/effect_sites.ml, lib/typecheck.ml, and the test/test_main.ml suite-label change all survive intact through the merge. Pure documentation + merge content. Zero behavioural risk.
2 parents 4116a1a + f45afa1 commit 8b040aa

10 files changed

Lines changed: 436 additions & 19 deletions

.machine_readable/6a2/STATE.a2ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ test-files = 54
6868
# the feature is not enforced on user programs through the CLI pipeline.
6969
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.)"
7070
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."
71-
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."
71+
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."
7272
row-polymorphism = "60% (records + effects rows implemented in typecheck/unify; not fully exercised end-to-end)"
7373
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."
7474
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

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -84,16 +84,26 @@ enforced. Handlers: *interpreter-complete*; WasmGC dispatch is
8484
`UnsupportedFeature` pending the EH proposal or the CPS transform (the #225
8585
CPS line is closing the async slice of this).
8686

87-
|Borrow checker |*partial — graph validation landed (CORE-01 pt 1)* |
87+
|Borrow checker |*partial — graph validation + NLL last-use landed
88+
(CORE-01 pts 1–3 Slice A)* |
8889
Place/borrow/move infra + use-after-move, conflicting-borrow,
8990
move-while-borrowed, lambda-capture. *CORE-01 part 1* (PR #240, Refs #177,
9091
gate 263/263): borrow-graph validation wired — `BorrowOutlivesOwner` now
9192
emitted (`&local` escaping its block); shared-XOR-exclusive enforced at
9293
*use* sites (`UseWhileExclusivelyBorrowed`); ownership now derived from the
9394
parameter *type* (`TyOwn/TyRef/TyMut`) so the owned/ref/mut discipline is
9495
actually enforced from real parsed source (closed a latent hole); call-arg
95-
borrows made temporary. *Deferred (CORE-01 pt 2+):* NLL/region inference,
96-
flow-sensitive escape via `outer = &x`, tighter quantity integration.
96+
borrows made temporary. *Part 2* (Refs #177): return-escape +
97+
`&mut e` parser surface (the exclusive borrow is finally expressible from
98+
source). *Part 3 Slice A* (Refs #177): non-lexical lifetimes —
99+
ref-bindings expire at their binder's *last use*, not at block exit
100+
(`compute_last_use_index` pre-pass + per-statement expiry in
101+
`check_block`). Patterns like `let r = &x; print(*r); x = 2` and
102+
`let m = &mut x; let y = *m; x` now type-check, while still-live borrows
103+
continue to block aliasing assignments. *Deferred (Slices B–D):*
104+
flow-sensitive escape via `outer = &x`; origin/region variables
105+
(Polonius surface) + loan-live-at-point dataflow across CFG joins;
106+
tighter quantity integration for captured linears.
97107

98108
|Quantity / affine types |*enforced* |QTT semiring in `lib/quantity.ml`,
99109
invoked inside the standard CLI pipeline. `@linear`/`@erased`/`@unrestricted`

docs/TECH-DEBT.adoc

Lines changed: 40 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -110,12 +110,23 @@ typed/codegen'd like `&e` — exclusivity is a static borrow property).
110110
`&`-in-`#{` literals and bare block-statements already parse on `main`;
111111
`-> &T`/`&T` *type* sigil deliberately **not** added — `ref T`/`mut T`
112112
keyword types already express reference types; a `&T` sigil is duplicate
113-
surface (ADR territory, not a soundness gap). *Part 2 residual — now the
114-
analysis, not surface:* NLL/region inference (Polonius) + flow-sensitive
115-
escape via `outer = &x` are now *expressible* (surface unblocked); the
116-
remaining work is the dataflow analysis itself. |S1 |pt1 #240 + pt2
117-
return-escape + `&mut` surface DONE (Refs #177); residual = NLL analysis
118-
— issue #177
113+
surface (ADR territory, not a soundness gap). *Part 3 Slice A — NLL
114+
last-use expiry LANDED* (Refs #177): a forward pre-pass
115+
(`compute_last_use_index`) maps each symbol to the greatest statement
116+
index that mentions it; after each statement, `check_block` expires any
117+
ref-binding introduced in that block whose binder is now dead, releasing
118+
the underlying borrow. Unblocks the canonical NLL patterns
119+
(`let r = &x; print(*r); x = 2`; `let m = &mut x; let y = *m; x`) while
120+
preserving soundness — the anti-aliasing rules still fire against
121+
statements that *do* use the binder (3 hermetic tests in "E2E Borrow
122+
Graph", two positive + one anti-regression). *Slices B–D residual:*
123+
flow-sensitive escape via assignment to an outer mutable
124+
(`outer = &x`); origin/region variables (Polonius surface) + loan-live-
125+
at-point dataflow across CFG joins; tighter quantity integration for
126+
captured linears. |S1 |pt1 #240 + pt2 return-escape + `&mut` surface +
127+
pt3 Slice A NLL last-use DONE (Refs #177); residual = Slices B–D
128+
(flow-sensitive escape, origin variables, quantity integration) —
129+
issue #177
119130
|CORE-02 |Effect-handler dispatch on WasmGC (was `UnsupportedFeature`;
120131
the chosen path is CPS over the EH proposal). The #225 CPS line closed
121132
the async slice; #234 generalised the boundary recogniser from a
@@ -169,7 +180,29 @@ complete; convergence ABI shared w/ Ephapax
169180
insert/set/remove/keys/values; AOT-gated (#136). Closes ESC-03 #247 (the
170181
#229 `Dict.t` target); unblocks the additive `Http.affine` headers→Dict
171182
upgrade
172-
|STDLIB-04 |Residual `extern` builtins → real implementations |S3 |open
183+
|STDLIB-04 |Residual `extern` builtins → real implementations (umbrella;
184+
split into 04a–04e 2026-05-24 per per-extern audit, one row per PR) |S3
185+
|open (5 sub-rows)
186+
|STDLIB-04a |Mut effect externs (`make_ref`/`get`/`set`) — *LANDED*
187+
(Refs #328): interp uses `VMut` cell (`lib/interp.ml`); Deno codegen
188+
lowers to `{__cell: x}` single-field object (`lib/codegen_deno.ml`);
189+
3 hermetic e2e tests in "E2E STDLIB-04a Mut #328" (Int + String
190+
round-trips + Deno codegen __cell-shape assertion) |S3 |DONE
191+
2026-05-24 (Refs #328)
192+
|STDLIB-04b |Throws extern `error<T>` — missing in all backends
193+
(`lib/interp.ml`, `lib/js_codegen.ml`, `lib/codegen_deno.ml`); sibling
194+
`panic` is wired and `error` should mirror it (divergent `T`) |S3 |open
195+
— issue #329
196+
|STDLIB-04c |`string_concat` extern — no direct wiring found; `++`
197+
operator independently lowered. Decide: remove (operator-only) or wire
198+
to mirror `++` |S3 |open — issue #330
199+
|STDLIB-04d |IO externs (`print`/`println`/`read_line`/`read_file`/
200+
`write_file`) — wired on all backends but no dedicated hermetic e2e
201+
tests; test-debt, not impl-debt |S3 |open — issue #331
202+
|STDLIB-04e |Pure externs (`int_to_string`/`string_to_int`/
203+
`string_length`) — real + tested (`lib/interp.ml:615-633`,
204+
`lib/codegen_deno.ml:263-272`); bookkeeping to mark DONE |S3 |open —
205+
issue #332
173206
|===
174207

175208
== Section D — INT (ecosystem integration)

lib/borrow.ml

Lines changed: 160 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -562,6 +562,113 @@ let check_return_escape (state : state) (symbols : Symbol.t)
562562
Error (BorrowOutlivesOwner (b, owner))
563563
| _ -> Ok ())
564564

565+
(** NLL last-use pre-pass (CORE-01 pt3 / #177 Slice A).
566+
567+
Returns a map [sym_id -> max statement index at which the symbol is
568+
mentioned anywhere inside [blk] (including nested blocks, lambda
569+
bodies, handler arms, etc.)]. Statement indices are 0-based; the
570+
block's tail expression, if any, is treated as the [n]-th "statement"
571+
(where [n = List.length blk.blk_stmts]).
572+
573+
Used by [check_block] to expire ref-bindings introduced in this block
574+
once their binder is dead, instead of holding them until lexical block
575+
exit. The expiry releases the underlying borrow, so subsequent
576+
statements may legally read or assign through the (no-longer-borrowed)
577+
owner — the canonical Rust-style "non-lexical lifetime" win.
578+
579+
A symbol that never appears is simply absent from the table; callers
580+
treat that as [-1] (last-use precedes the first statement → expire
581+
immediately after the declaration). *)
582+
let compute_last_use_index (symbols : Symbol.t) (blk : block)
583+
: (Symbol.symbol_id, int) Hashtbl.t =
584+
let tbl : (Symbol.symbol_id, int) Hashtbl.t = Hashtbl.create 8 in
585+
let bump (sym : Symbol.symbol_id) (idx : int) : unit =
586+
match Hashtbl.find_opt tbl sym with
587+
| Some cur when cur >= idx -> ()
588+
| _ -> Hashtbl.replace tbl sym idx
589+
in
590+
let mark_var (idx : int) (id : ident) : unit =
591+
match lookup_symbol_by_name symbols id.name with
592+
| Some s -> bump s.Symbol.sym_id idx
593+
| None -> ()
594+
in
595+
let rec visit_expr (idx : int) (e : expr) : unit =
596+
match e with
597+
| ExprVar id -> mark_var idx id
598+
| ExprLit _ | ExprVariant _ -> ()
599+
| ExprSpan (e, _) -> visit_expr idx e
600+
| ExprApp (f, args) ->
601+
visit_expr idx f; List.iter (visit_expr idx) args
602+
| ExprField (b, _) | ExprTupleIndex (b, _) -> visit_expr idx b
603+
| ExprIndex (b, i) -> visit_expr idx b; visit_expr idx i
604+
| ExprTuple es | ExprArray es -> List.iter (visit_expr idx) es
605+
| ExprRecord r ->
606+
List.iter (fun (_, eo) -> match eo with Some e -> visit_expr idx e | None -> ()) r.er_fields;
607+
(match r.er_spread with Some e -> visit_expr idx e | None -> ())
608+
| ExprRowRestrict (e, _) -> visit_expr idx e
609+
| ExprBinary (l, _, r) -> visit_expr idx l; visit_expr idx r
610+
| ExprUnary (_, e) -> visit_expr idx e
611+
| ExprLet lb ->
612+
visit_expr idx lb.el_value;
613+
(match lb.el_body with Some b -> visit_expr idx b | None -> ())
614+
| ExprIf ei ->
615+
visit_expr idx ei.ei_cond; visit_expr idx ei.ei_then;
616+
(match ei.ei_else with Some e -> visit_expr idx e | None -> ())
617+
| ExprMatch em ->
618+
visit_expr idx em.em_scrutinee;
619+
List.iter (fun arm ->
620+
(match arm.ma_guard with Some g -> visit_expr idx g | None -> ());
621+
visit_expr idx arm.ma_body
622+
) em.em_arms
623+
| ExprBlock blk -> visit_block idx blk
624+
| ExprLambda lam -> visit_expr idx lam.elam_body
625+
| ExprReturn (Some e) -> visit_expr idx e
626+
| ExprReturn None -> ()
627+
| ExprHandle eh ->
628+
visit_expr idx eh.eh_body;
629+
List.iter (fun arm ->
630+
match arm with
631+
| HandlerReturn (_, b) -> visit_expr idx b
632+
| HandlerOp (_, _, b) -> visit_expr idx b
633+
) eh.eh_handlers
634+
| ExprResume (Some e) -> visit_expr idx e
635+
| ExprResume None -> ()
636+
| ExprTry et ->
637+
visit_block idx et.et_body;
638+
(match et.et_catch with
639+
| Some arms ->
640+
List.iter (fun arm ->
641+
(match arm.ma_guard with Some g -> visit_expr idx g | None -> ());
642+
visit_expr idx arm.ma_body) arms
643+
| None -> ());
644+
(match et.et_finally with Some b -> visit_block idx b | None -> ())
645+
| ExprUnsafe ops ->
646+
List.iter (fun op ->
647+
match op with
648+
| UnsafeRead e -> visit_expr idx e
649+
| UnsafeWrite (a, b) -> visit_expr idx a; visit_expr idx b
650+
| UnsafeOffset (a, b) -> visit_expr idx a; visit_expr idx b
651+
| UnsafeTransmute (_, _, e) -> visit_expr idx e
652+
| UnsafeForget e -> visit_expr idx e
653+
) ops
654+
and visit_stmt (idx : int) (s : stmt) : unit =
655+
match s with
656+
| StmtLet sl -> visit_expr idx sl.sl_value
657+
| StmtExpr e -> visit_expr idx e
658+
| StmtAssign (lhs, _, rhs) -> visit_expr idx lhs; visit_expr idx rhs
659+
| StmtWhile (c, b) -> visit_expr idx c; visit_block idx b
660+
| StmtFor (_, it, b) -> visit_expr idx it; visit_block idx b
661+
and visit_block (idx : int) (b : block) : unit =
662+
List.iter (visit_stmt idx) b.blk_stmts;
663+
match b.blk_expr with Some e -> visit_expr idx e | None -> ()
664+
in
665+
List.iteri (fun i s -> visit_stmt i s) blk.blk_stmts;
666+
let tail_idx = List.length blk.blk_stmts in
667+
(match blk.blk_expr with
668+
| Some e -> visit_expr tail_idx e
669+
| None -> ());
670+
tbl
671+
565672
(** Check borrows in an expression *)
566673
let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr : expr) : unit result =
567674
match expr with
@@ -1000,10 +1107,41 @@ and check_block (ctx : context) (state : state) (symbols : Symbol.t) (blk : bloc
10001107
ref-bindings introduced here do not leak past block exit. CORE-01. *)
10011108
let block_locals_at_entry = state.block_local_syms in
10021109
let ref_bindings_at_entry = state.ref_bindings in
1003-
let* () = List.fold_left (fun acc stmt ->
1004-
let* () = acc in
1005-
check_stmt ctx state symbols stmt
1006-
) (Ok ()) blk.blk_stmts in
1110+
(* NLL last-use pre-pass (CORE-01 pt3 / #177 Slice A): compute the last
1111+
statement index at which each symbol is mentioned. After each
1112+
statement we expire any ref-binding introduced in *this* block whose
1113+
binder's last use has already passed, releasing the underlying
1114+
borrow. This is the non-lexical-lifetimes win — patterns like
1115+
[let r = &x; print(*r); x = 2] now type-check, while the
1116+
anti-aliasing rules remain sound because the borrow is still live
1117+
across statements that *do* use the binder. *)
1118+
let last_use = compute_last_use_index symbols blk in
1119+
let last_use_of (sym : Symbol.symbol_id) : int =
1120+
match Hashtbl.find_opt last_use sym with
1121+
| Some i -> i
1122+
| None -> -1
1123+
in
1124+
let is_outer_binding (sym : Symbol.symbol_id) : bool =
1125+
List.exists (fun (sym', _) -> sym' = sym) ref_bindings_at_entry
1126+
in
1127+
let expire_dead_ref_bindings (stmt_idx : int) : unit =
1128+
let dying, still_live =
1129+
List.partition (fun (sym, _b) ->
1130+
(not (is_outer_binding sym)) && last_use_of sym <= stmt_idx
1131+
) state.ref_bindings
1132+
in
1133+
List.iter (fun (_sym, b) -> end_borrow state b) dying;
1134+
state.ref_bindings <- still_live
1135+
in
1136+
let* () =
1137+
let indexed = List.mapi (fun i s -> (i, s)) blk.blk_stmts in
1138+
List.fold_left (fun acc (i, stmt) ->
1139+
let* () = acc in
1140+
let* () = check_stmt ctx state symbols stmt in
1141+
expire_dead_ref_bindings i;
1142+
Ok ()
1143+
) (Ok ()) indexed
1144+
in
10071145
let* () = match blk.blk_expr with
10081146
| Some e -> check_expr ctx state symbols e
10091147
| None -> Ok ()
@@ -1190,10 +1328,24 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
11901328
bare block-statements already parsed; the `-> &T`/`&T` *type* sigil was
11911329
deliberately not added (`ref T`/`mut T` keyword types already exist).
11921330
1193-
Still deferred — now the *analysis*, no longer parser-gated:
1194-
- Non-lexical lifetimes with region inference (Polonius-style).
1331+
CORE-01 pt3 Slice A (NLL last-use): ref-bindings introduced in a
1332+
block now expire at the binder's *last use*, not at block exit. A
1333+
forward pre-pass (compute_last_use_index) maps each symbol to the
1334+
greatest statement index that mentions it (the tail expression
1335+
counts as the n-th statement); after each statement, check_block
1336+
releases the underlying borrow of any in-block ref-binding whose
1337+
binder is now dead. Unblocks the canonical NLL patterns
1338+
([let r = &x; print(*r); x = 2] and [let m = &mut x; let y = *m; x]),
1339+
while still rejecting real conflicts (the anti-aliasing rules fire
1340+
against statements that *do* use the binder, before expiry).
1341+
Outer-block ref-bindings are deliberately preserved — they expire
1342+
only at their own block's exit.
1343+
1344+
Still deferred — region-/flow-sensitive remainder:
11951345
- Flow-sensitive escape via assignment to an outer mutable
1196-
(`outer = &x`) — now *expressible* (`&mut`, assignment, blocks all
1197-
parse); the remaining work is the dataflow analysis itself.
1346+
(`outer = &x`): the assignment must update the borrow graph the
1347+
way [let r = &x] already does.
1348+
- Origin/region variables (Polonius surface) + loan-live-at-point
1349+
dataflow across CFG joins (Slice C).
11981350
- Tighter integration with the quantity checker for captured linears.
11991351
*)

lib/codegen_deno.ml

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -275,6 +275,16 @@ let () =
275275
b "int_to_char" (fun a -> Printf.sprintf "__as_intToChar(%s)" (arg 0 a));
276276
b "show" (fun a -> Printf.sprintf "__as_show(%s)" (arg 0 a));
277277
b "panic" (fun a -> Printf.sprintf "(() => { throw new Error(%s); })()" (arg 0 a));
278+
(* Mut effect builtins (STDLIB-04a, Refs #328) — runtime mutable cells.
279+
Distinct from borrow-checker [&]/[&mut] references: these back the
280+
[stdlib/effects.affine] [Ref<T>] type declared `/ Mut`. Lowered as
281+
a single-field object so [get]/[set] are O(1) field access; comma-
282+
expression in [set] returns Unit (null) to match the extern's
283+
signature `(Ref<T>, T) -> Unit / Mut`. *)
284+
b "make_ref" (fun a -> Printf.sprintf "({__cell: %s})" (arg 0 a));
285+
b "get" (fun a -> Printf.sprintf "((%s).__cell)" (arg 0 a));
286+
b "set" (fun a -> Printf.sprintf "(((%s).__cell = %s), null)"
287+
(arg 0 a) (arg 1 a));
278288
(* ---- Http (issue #160) ---- *)
279289
(* `await` is legal: every caller of `http_request` is declared
280290
`/ Net, Async` and so is emitted as an `async function`

0 commit comments

Comments
 (0)