diff --git a/lib/borrow.ml b/lib/borrow.ml index 1d7dc35..0b85ed1 100644 --- a/lib/borrow.ml +++ b/lib/borrow.ml @@ -94,6 +94,19 @@ type state = { *caller-owned* referents and are deliberately absent here — returning a borrow of them is sound. CORE-01 pt2 / #177 (return-escape). *) mutable callee_owned_params : Symbol.symbol_id list; + + (** Sym-ids of bindings declared @linear (`QOne`) in the current + function — surfaced as explicit `@linear` annotations on lets/params + and as inferred `QOne` from a [Cmd _] type annotation. Maintained + alongside the quantity checker's per-block linear-tracking so the + borrow checker can reject *capture* of these bindings by a closure: + a closure can be called 0..N times, so capturing a linear binding + makes its consumption count unprovable at borrow time. The quantity + checker also catches this via [QOmega] scaling of captures, but the + borrow-side error fires earlier in the pipeline and points at the + *lambda* span (the capture site) rather than at a downstream "used + multiple times" diagnostic. CORE-01 pt3 Slice D / #177. *) + mutable linear_bindings : Symbol.symbol_id list; } (** Borrow checker errors *) @@ -108,6 +121,11 @@ type borrow_error = (** use of [place] (at the trailing span) while a still-live exclusive borrow holds it — the shared-XOR-exclusive aliasing rule, enforced at use sites, not only at borrow creation. CORE-01 / #177. *) + | LinearCapturedByClosure of string * Span.t + (** the named @linear binding has been captured as a closure free + variable at the lambda's span — capturing extends consumption + beyond what the @linear contract can be checked at borrow time + (a closure may be called 0..N times). CORE-01 pt3 Slice D / #177. *) [@@deriving show] type 'a result = ('a, borrow_error) Result.t @@ -152,8 +170,27 @@ let create () : state = ref_bindings = []; block_local_syms = []; callee_owned_params = []; + linear_bindings = []; } +(** Mirror of [Quantity.quantity_of_ty_annotation]: returns [QOne] when the + given type annotation is a [Cmd _] application (linear by construction + per ADR-002 / Stage 11), [QOmega] otherwise. Duplicated here so + [Borrow] does not depend on [Quantity]; the canonical helper still + lives in [quantity.ml]. CORE-01 pt3 Slice D / #177. *) +let borrow_quantity_of_ty (te_opt : type_expr option) : quantity = + match te_opt with + | Some (TyApp ({ name = "Cmd"; _ }, _)) -> QOne + | _ -> QOmega + +(** Returns true if a let-binding declared with the given explicit-quantity + annotation and type annotation should be tracked as @linear (QOne) by + the borrow checker. CORE-01 pt3 Slice D / #177. *) +let let_is_linear (q_opt : quantity option) (ty_opt : type_expr option) : bool = + match q_opt with + | Some q -> q = QOne + | None -> borrow_quantity_of_ty ty_opt = QOne + (** Add a function signature to context *) let add_fn_signature (ctx : context) (fd : fn_decl) : unit = let sig_ = { @@ -369,6 +406,13 @@ let format_borrow_error (e : borrow_error) : string = exclusive borrow (id %d) taken at %s is still live" (format_place place) (format_span use_span) b.b_id (format_span b.b_span) + | LinearCapturedByClosure (name, lam_span) -> + Printf.sprintf + "cannot capture @linear binding `%s` in a closure (at %s)\n \ + a closure may be called zero or many times, so capturing a \ + @linear binding makes its consumption count unprovable. \ + Inline the use, or move the binding into the closure body." + name (format_span lam_span) (** Get span from an expression *) let rec expr_span (expr : expr) : Span.t = @@ -937,9 +981,24 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr : ) acc ops in let free_names = collect_free [] lam.elam_body in + let borrow_span = expr_span (ExprLambda lam) in + (* CORE-01 pt3 Slice D / #177: reject capture of a @linear binding. + A closure may be called 0..N times, so capturing a linear + binding lifts its consumption count out of what the borrow + checker can prove finite-once. The quantity checker also + catches this via [QOmega] scaling, but the borrow-side error + (a) fires earlier in the pipeline and (b) names the lambda + span — the actual capture site — rather than a downstream + "used multiple times" diagnostic. *) + let* () = List.fold_left (fun acc name -> + let* () = acc in + match lookup_symbol_by_name symbols name with + | Some sym when List.mem sym.Symbol.sym_id state.linear_bindings -> + Error (LinearCapturedByClosure (name, borrow_span)) + | _ -> Ok () + ) (Ok ()) free_names in (* Create a Shared borrow for each captured free variable. If a borrow conflict or use-after-move is detected, fail immediately. *) - let borrow_span = expr_span (ExprLambda lam) in let* () = List.fold_left (fun acc name -> let* () = acc in match expr_to_place symbols (ExprVar { name; span = borrow_span }) with @@ -959,7 +1018,11 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr : | PatVar id -> begin match lookup_symbol_by_name symbols id.name with | Some sym -> - state.block_local_syms <- sym.Symbol.sym_id :: state.block_local_syms + state.block_local_syms <- sym.Symbol.sym_id :: state.block_local_syms; + (* Slice D / #177: record @linear let-bindings for the + capture-rejection check on subsequent ExprLambda's. *) + if let_is_linear lb.el_quantity lb.el_ty then + state.linear_bindings <- sym.Symbol.sym_id :: state.linear_bindings | None -> () end | _ -> () @@ -1337,7 +1400,11 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt | PatVar id -> begin match lookup_symbol_by_name symbols id.name with | Some sym -> - state.block_local_syms <- sym.Symbol.sym_id :: state.block_local_syms + state.block_local_syms <- sym.Symbol.sym_id :: state.block_local_syms; + (* Slice D / #177: track @linear let-bindings for the + capture-rejection check on subsequent ExprLambda's. *) + if let_is_linear sl.sl_quantity sl.sl_ty then + state.linear_bindings <- sym.Symbol.sym_id :: state.linear_bindings | None -> () end | _ -> () @@ -1519,7 +1586,12 @@ let check_function (ctx : context) (symbols : Symbol.t) (fd : fn_decl) : unit re | None | Some Own -> state.callee_owned_params <- sym.sym_id :: state.callee_owned_params - | Some Ref | Some Mut -> ()) + | Some Ref | Some Mut -> ()); + (* Slice D / #177: track @linear-annotated params for the + capture-rejection check on subsequent ExprLambda's. *) + if p.p_quantity = Some QOne then + state.linear_bindings <- + sym.sym_id :: state.linear_bindings | None -> ()) ) fd.fd_params; match fd.fd_body with @@ -1634,6 +1706,20 @@ let check_program (symbols : Symbol.t) (program : program) : unit result = so legitimate re-init loops still accept while loops with an unrestored body-move reject. + CORE-01 pt3 Slice D (2026-05-26): borrow-side rejection of + @linear-binding capture by a closure. A closure may be called + 0..N times, so capturing a [@linear] (`QOne`) binding lifts its + consumption count out of what the borrow checker can prove + finite-once. The quantity checker also rejects this via [QOmega] + scaling of lambda captures (quantity.ml ExprLambda), but the + borrow-side error fires earlier in the pipeline (Typecheck → + Borrow → Quantity) and names the *lambda* span as the capture + site rather than producing a downstream "used multiple times" + diagnostic. [state.linear_bindings] is populated from + [@linear] / `Cmd _` annotations on params, `let`-statements, and + `let`-expressions; [ExprLambda] then rejects free-vars whose + sym-id is in that set with [LinearCapturedByClosure]. + Still deferred: - Origin/region variables (true Polonius surface) — a region var on each [TyRef]/[TyMut] with subset constraints and a diff --git a/test/e2e/fixtures/slice_d_captured_linear_let_rejected.affine b/test/e2e/fixtures/slice_d_captured_linear_let_rejected.affine new file mode 100644 index 0000000..6bf2c44 --- /dev/null +++ b/test/e2e/fixtures/slice_d_captured_linear_let_rejected.affine @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// CORE-01 pt3 Slice D / #177: a closure that captures a @linear +// let-binding must be rejected by the borrow checker — a closure +// may be called 0..N times, so capturing a @linear binding lifts +// its consumption count out of finite-once provability. +// Expected: Error LinearCapturedByClosure. + +module SliceDCapturedLinearLetRejected; + +fn capture_linear_let() -> Int { + @linear let x = 42; + let f = fn() => x + 1; + f() +} diff --git a/test/e2e/fixtures/slice_d_captured_linear_param_rejected.affine b/test/e2e/fixtures/slice_d_captured_linear_param_rejected.affine new file mode 100644 index 0000000..3eca30d --- /dev/null +++ b/test/e2e/fixtures/slice_d_captured_linear_param_rejected.affine @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// CORE-01 pt3 Slice D / #177: a closure that captures a @linear +// function parameter is rejected at the borrow checker for the +// same reason as the let-binding case — a closure may be called +// 0..N times. Pre-Slice-D this would have surfaced only at the +// quantity checker (as "used multiple times via QOmega scaling"); +// now it surfaces at borrow check with a span pointing at the +// closure. Expected: Error LinearCapturedByClosure. + +module SliceDCapturedLinearParamRejected; + +fn capture_linear_param(@linear y: Int) -> Int { + let f = fn() => y + 1; + f() +} diff --git a/test/e2e/fixtures/slice_d_captured_nonlinear_ok.affine b/test/e2e/fixtures/slice_d_captured_nonlinear_ok.affine new file mode 100644 index 0000000..8d17c9d --- /dev/null +++ b/test/e2e/fixtures/slice_d_captured_nonlinear_ok.affine @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// CORE-01 pt3 Slice D / #177: anti-regression — capturing a +// non-linear (unannotated → defaults to QOmega) binding by a +// closure must still pass. This pins that the new rejection is +// scoped to @linear captures, not any free-var capture. Expected: Ok. + +module SliceDCapturedNonlinearOk; + +fn capture_nonlinear() -> Int { + let x = 7; + let f = fn() => x + 1; + f() +} diff --git a/test/test_e2e.ml b/test/test_e2e.ml index 998620e..2a51bbe 100644 --- a/test/test_e2e.ml +++ b/test/test_e2e.ml @@ -4574,6 +4574,46 @@ let test_slice_c_prime_loop_move_persists () = silently accepted — the 2-iteration pass did not \ catch the unrestored move on `x`" +(* CORE-01 pt3 Slice D / #177 — borrow-side rejection of @linear + capture by a closure. The quantity checker already rejected + these via QOmega scaling, but the borrow-side error fires + earlier (Typecheck → Borrow → Quantity) and points at the + lambda span. Three tests pin: (1) @linear let captured; + (2) @linear param captured; (3) anti-regression — non-linear + capture must still pass. *) +let test_slice_d_captured_linear_let_rejected () = + match borrow_result (fixture "slice_d_captured_linear_let_rejected.affine") with + | Error (Borrow.LinearCapturedByClosure (name, _)) -> + Alcotest.(check string) "captured name surfaced in error" "x" name + | Error e -> + Alcotest.fail ("Slice D: expected LinearCapturedByClosure on `|| x + 1` \ + capture of @linear let x, got: " + ^ Borrow.format_borrow_error e) + | Ok () -> + Alcotest.fail "Slice D regressed: @linear let-binding was silently \ + captured by closure — multi-call would break linear \ + contract" + +let test_slice_d_captured_linear_param_rejected () = + match borrow_result (fixture "slice_d_captured_linear_param_rejected.affine") with + | Error (Borrow.LinearCapturedByClosure (name, _)) -> + Alcotest.(check string) "captured param name surfaced" "y" name + | Error e -> + Alcotest.fail ("Slice D: expected LinearCapturedByClosure on `|| y + 1` \ + capture of @linear param y, got: " + ^ Borrow.format_borrow_error e) + | Ok () -> + Alcotest.fail "Slice D regressed: @linear param was silently captured \ + by closure" + +let test_slice_d_captured_nonlinear_ok () = + match borrow_result (fixture "slice_d_captured_nonlinear_ok.affine") with + | Ok () -> () + | Error e -> + Alcotest.fail ("Slice D anti-regression: non-linear capture was \ + spuriously rejected — the new rule must scope to \ + @linear only: " ^ Borrow.format_borrow_error e) + let borrow_tests = [ Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block" `Quick test_borrow_outlives_owner; @@ -4625,6 +4665,12 @@ let borrow_tests = [ `Quick test_slice_c_prime_loop_reinit_ok; Alcotest.test_case "Slice C' anti-regression: multi-iter move rejected (#177 pt3)" `Quick test_slice_c_prime_loop_move_persists; + Alcotest.test_case "Slice D: @linear let captured by closure rejected (#177 pt3)" + `Quick test_slice_d_captured_linear_let_rejected; + Alcotest.test_case "Slice D: @linear param captured by closure rejected (#177 pt3)" + `Quick test_slice_d_captured_linear_param_rejected; + Alcotest.test_case "Slice D anti-regression: non-linear capture still OK (#177 pt3)" + `Quick test_slice_d_captured_nonlinear_ok; ] (* ============================================================================