Skip to content

Commit 6384826

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
fix(quantity): scaled Let rule + L-to-R eval_list — closes BUG-001/002/003
Two soundness fixes that share a single test infrastructure pass. BUG-001 (high severity, soundness — ω-let smuggles linear values): The quantity-checking Let case now implements the QTT-orthodox scaled Let rule per ADR-002: Γ₁ ⊢ e₁ : A (Γ₂, x:^q A) ⊢ e₂ : B ───────────────────────────────────── q·Γ₁ + Γ₂ ⊢ let x :^q = e₁ in e₂ : B Implementation: snapshot the env, walk e1 (which records usages into the live env), compute the per-variable delta, scale each delta by q via the new scale_usage helper, restore the snapshot, and re-apply the scaled deltas as additions. Then walk e2 normally. The interesting case is q = ω: scale_usage QOmega UOne = UMany, which causes a linear variable consumed in e1 to be reported as "used multiple times" once viewed through the @unrestricted binder. This is what closes BUG-001. BUG-002 (medium, semantics — :0 lets do not erase their RHS): Closed transitively by the same scaling code path. scale_usage QZero _ = UZero, so RHS contributions to outer linear variables are correctly dropped under @Erased binders. The optional interpreter-side erasure (skipping eval entirely) is a separate optimisation, deferred. BUG-003 (medium, semantics — eval_list right-to-left): lib/interp.ml eval_list rewritten from List.fold_right (which is right-to-left under OCaml's strict monadic bind) to an explicit L-to-R recursive loop with terminal List.rev. Per ADR-003. Brings ExprApp/ExprTuple/ExprArray/ExprRecord into agreement with ExprBinary, which was already left-to-right. Error vocabulary updated: format_quantity_error now speaks @linear/@erased/@unrestricted regardless of which surface form the user wrote, via canonical_quantity_name and usage_in_words helpers. Source vocabulary and diagnostic vocabulary stay aligned per ADR-007. Four behavioural regression fixtures and test cases: - bug_001_omega_let_smuggles_linear.affine (Option C, must reject) - bug_001_sugar_form.affine (Option B, must reject) - affine_let_valid.affine (Option C, must accept) - affine_let_valid_sugar.affine (Option B, must accept) All four pass. Test count 64 → 68. The 22 pre-existing baseline failures are unchanged (zero new regressions, zero accidentally resolved). BUG-003 lacks a behavioural fixture in this commit because observable order verification requires the let-mut interpreter path, which is broken in baseline (root cause of several pre- existing failing interp tests). The fix is verified by code review against ADR-003. Refs ADR-002, ADR-003, ADR-007. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 9d8be1b commit 6384826

7 files changed

Lines changed: 251 additions & 13 deletions

File tree

‎lib/interp.ml‎

Lines changed: 15 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -343,13 +343,22 @@ let rec eval (env : env) (expr : expr) : value result =
343343
| ExprSpan (e, _) ->
344344
eval env e
345345

346-
(** Evaluate a list of expressions *)
346+
(** Evaluate a list of expressions strictly left-to-right.
347+
348+
Per ADR-003, all n-ary expression forms (application arguments, tuple
349+
components, array elements, record fields) evaluate their subexpressions
350+
in source order. The previous implementation used [List.fold_right] with
351+
monadic bind, which under OCaml's strict evaluation visited elements
352+
right-to-left — inconsistent with [ExprBinary] and a latent divergence
353+
point for future affine enforcement and effect handlers. *)
347354
and eval_list (env : env) (exprs : expr list) : value list result =
348-
List.fold_right (fun expr acc ->
349-
let* vals = acc in
350-
let* v = eval env expr in
351-
Ok (v :: vals)
352-
) exprs (Ok [])
355+
let rec loop acc = function
356+
| [] -> Ok (List.rev acc)
357+
| expr :: rest ->
358+
let* v = eval env expr in
359+
loop (v :: acc) rest
360+
in
361+
loop [] exprs
353362

354363
(** Evaluate match arms *)
355364
and eval_match_arms (env : env) (scrut_val : value) (arms : match_arm list) : value result =

‎lib/quantity.ml‎

Lines changed: 110 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,32 @@ let add_usage (u1 : usage) (u2 : usage) : usage =
103103
| (UZero, u) | (u, UZero) -> u
104104
| _ -> UMany
105105

106+
(** Scale a usage by a quantity — implements the q·u operation that
107+
the QTT-orthodox Let rule needs to scale the value-context Γ₁ by
108+
the binder's quantity q.
109+
110+
Per ADR-002, [let x :^q = e1 in e2] is type-checked under
111+
[q·Γ₁ + Γ₂ ⊢ ...]. The semiring action on usages is:
112+
113+
0 · u = UZero (erased — usage is annihilated)
114+
1 · u = u (linear — usage passes through unchanged)
115+
ω · UZero = UZero (no use stays no use)
116+
ω · UOne = UMany (a single use, replicated, becomes many)
117+
ω · UMany = UMany (many stays many)
118+
119+
The interesting case is [ω · UOne = UMany]: it is the rule that
120+
closes BUG-001. A linear variable consumed in [e1] under an
121+
ω-binder gets its usage promoted to UMany, which the
122+
[check_quantity] step then catches as
123+
[LinearVariableUsedMultiple]. *)
124+
let scale_usage (q : quantity) (u : usage) : usage =
125+
match (q, u) with
126+
| (QZero, _) -> UZero
127+
| (QOne, u) -> u
128+
| (QOmega, UZero) -> UZero
129+
| (QOmega, UOne) -> UMany
130+
| (QOmega, UMany) -> UMany
131+
106132
(* {1 Errors} *)
107133

108134
(** Quantity checking errors with precise descriptions. *)
@@ -120,21 +146,44 @@ type quantity_error =
120146
(** Result type carrying a quantity error paired with a source span. *)
121147
type 'a result = ('a, quantity_error * Span.t) Result.t
122148

123-
(** Format a quantity error for human-readable output. *)
149+
(** Pretty-print a quantity using the canonical Option C surface form
150+
from ADR-007. Used in error messages so source vocabulary and
151+
diagnostic vocabulary stay aligned. *)
152+
let canonical_quantity_name (q : quantity) : string =
153+
match q with
154+
| QZero -> "@erased"
155+
| QOne -> "@linear"
156+
| QOmega -> "@unrestricted"
157+
158+
(** Pretty-print a usage count in plain English. *)
159+
let usage_in_words (u : usage) : string =
160+
match u with
161+
| UZero -> "never used"
162+
| UOne -> "used exactly once"
163+
| UMany -> "used multiple times"
164+
165+
(** Format a quantity error for human-readable output. Per ADR-007, all
166+
diagnostic text uses the @linear/@erased/@unrestricted vocabulary,
167+
even when the source program used the :1/:0/:ω sugar form. The
168+
user reads consistent words regardless of which surface they wrote. *)
124169
let format_quantity_error (err : quantity_error) : string =
125170
match err with
126171
| LinearVariableUnused id ->
127-
Printf.sprintf "Linear variable '%s' must be used exactly once, but was never used"
172+
Printf.sprintf
173+
"@linear binding '%s' must be used exactly once, but was never used"
128174
id.name
129175
| LinearVariableUsedMultiple id ->
130-
Printf.sprintf "Linear variable '%s' must be used exactly once, but was used multiple times"
176+
Printf.sprintf
177+
"@linear binding '%s' must be used exactly once, but was used multiple times"
131178
id.name
132179
| ErasedVariableUsed id ->
133-
Printf.sprintf "Erased variable '%s' (quantity 0) must not be used at runtime"
180+
Printf.sprintf
181+
"@erased binding '%s' must not be used at runtime"
134182
id.name
135183
| QuantityMismatch (id, q, u) ->
136-
Printf.sprintf "Quantity mismatch for '%s': declared %s but used %s"
137-
id.name (show_quantity q) (show_usage u)
184+
Printf.sprintf
185+
"quantity mismatch for '%s': declared %s but %s"
186+
id.name (canonical_quantity_name q) (usage_in_words u)
138187

139188
(* {1 Quantity environment} *)
140189

@@ -249,7 +298,41 @@ let rec infer_usage_expr (env : env) (expr : expr) : unit =
249298
infer_usage_expr env lam.elam_body
250299

251300
| ExprLet lb ->
301+
(* ADR-002 / ADR-007: Let value context is scaled by the binder's
302+
quantity. Concretely:
303+
q·Γ₁ ⊢ e1 : A (Γ₂, x:^q A) ⊢ e2 : B
304+
─────────────────────────────────────
305+
q·Γ₁ + Γ₂ ⊢ let x :^q = e1 in e2 : B
306+
For the usage analysis we implement this as: snapshot the env,
307+
walk e1 (which records usages into the live env), compute the
308+
per-variable delta added by walking e1, scale each delta entry
309+
by q, restore the snapshot, and re-apply the scaled deltas as
310+
additions. Then walk e2 normally. *)
311+
let q = Option.value lb.el_quantity ~default:QOmega in
312+
let before_value = env_snapshot env in
252313
infer_usage_expr env lb.el_value;
314+
let after_value = env_snapshot env in
315+
env_restore env before_value;
316+
(* Re-apply scaled deltas. *)
317+
Hashtbl.iter (fun name after_u ->
318+
let before_u =
319+
Hashtbl.find_opt before_value name |> Option.value ~default:UZero
320+
in
321+
(* Compute the delta usage added by walking el_value. We model
322+
delta as: how many additional uses occurred during the walk.
323+
Since usage is a 3-point lattice, the simplest sound rule is
324+
"if the walk increased the usage at all, the delta is the
325+
after-value's contribution beyond the before-value." We
326+
implement this by treating any rise from before to after as
327+
the delta usage to scale. *)
328+
let delta =
329+
if equal_usage before_u after_u then UZero
330+
else after_u
331+
in
332+
let scaled = scale_usage q delta in
333+
let merged = add_usage before_u scaled in
334+
Hashtbl.replace env.usages name merged
335+
) after_value;
253336
Option.iter (infer_usage_expr env) lb.el_body
254337

255338
| ExprIf ei ->
@@ -369,7 +452,27 @@ and infer_usage_block (env : env) (blk : block) : unit =
369452
and infer_usage_stmt (env : env) (stmt : stmt) : unit =
370453
match stmt with
371454
| StmtLet sl ->
372-
infer_usage_expr env sl.sl_value
455+
(* Same scaling treatment as ExprLet — see ADR-002 commentary
456+
there. The statement form has no body to walk afterward;
457+
subsequent statements in the enclosing block are walked
458+
independently by infer_usage_block. *)
459+
let q = Option.value sl.sl_quantity ~default:QOmega in
460+
let before_value = env_snapshot env in
461+
infer_usage_expr env sl.sl_value;
462+
let after_value = env_snapshot env in
463+
env_restore env before_value;
464+
Hashtbl.iter (fun name after_u ->
465+
let before_u =
466+
Hashtbl.find_opt before_value name |> Option.value ~default:UZero
467+
in
468+
let delta =
469+
if equal_usage before_u after_u then UZero
470+
else after_u
471+
in
472+
let scaled = scale_usage q delta in
473+
let merged = add_usage before_u scaled in
474+
Hashtbl.replace env.usages name merged
475+
) after_value
373476
| StmtExpr e ->
374477
infer_usage_expr env e
375478
| StmtAssign (lhs, _, rhs) ->

‎test/e2e/fixtures/affine_let_valid.affine‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// ADR-002 / ADR-007 valid case (Option C primary form).
3+
//
4+
// `r` is @linear (must be used exactly once). It is bound under a
5+
// @linear let, so the value context scales by 1 (identity). The let-
6+
// bound alias `s` is then used exactly once in the body. This must
7+
// pass the quantity checker.
8+
9+
fn forward(@linear r: Int) -> Int {
10+
@linear let s = r;
11+
s
12+
}

‎test/e2e/fixtures/affine_let_valid_sugar.affine‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// ADR-002 / ADR-007 valid case — Option B sugar form.
3+
// Identical semantics to affine_let_valid.affine, written with :1
4+
// numeric quantity sugar in place of @linear.
5+
6+
fn forward(@linear r: Int) -> Int {
7+
let s :1 = r;
8+
s
9+
}

‎test/e2e/fixtures/bug_001_omega_let_smuggles_linear.affine‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// BUG-001 regression: ω-let must NOT smuggle a linear value through.
3+
//
4+
// `consume` declares its parameter as @linear, so within consume's body
5+
// the parameter `r` is a linear binding. The body binds `r` under an
6+
// @unrestricted let — per the QTT-orthodox scaled Let rule (ADR-002),
7+
// the value context for `e1` is scaled by ω, which promotes any linear
8+
// usage in `e1` to UMany. The quantity checker must then reject this
9+
// program because `r` is now considered "used multiple times" inside a
10+
// @linear binding.
11+
//
12+
// This fixture uses Option C surface syntax (@unrestricted, @linear).
13+
// The dual sugar-form fixture is bug_001_sugar_form.affine.
14+
15+
fn consume(@linear r: Int) -> Int {
16+
@unrestricted let alias = r;
17+
alias + alias
18+
}

‎test/e2e/fixtures/bug_001_sugar_form.affine‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// BUG-001 regression — Option B sugar form. Same program as
3+
// bug_001_omega_let_smuggles_linear.affine but written with the
4+
// :1 / :ω numeric quantity sugar instead of @linear / @unrestricted.
5+
// Both surface forms must produce identical enforcement: the quantity
6+
// checker must reject this for the same reason.
7+
8+
fn consume(@linear r: Int) -> Int {
9+
let alias :ω = r;
10+
alias + alias
11+
}

‎test/test_e2e.ml‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -435,10 +435,86 @@ let test_quantity_erased_violation () =
435435
Alcotest.(check bool) "error mentions erased"
436436
true (String.length msg > 0)
437437

438+
(* ──── BUG-001 / ADR-007 regression cases ──────────────────────────────────
439+
The four fixtures cover the cross product of {must-reject, must-accept}
440+
× {Option C @linear primary form, Option B :1 sugar form}. Both surface
441+
forms must produce identical enforcement, which proves the hybrid
442+
syntax is wired through the same code path. *)
443+
444+
let test_bug_001_smuggles_linear_attr_form () =
445+
match parse_fixture (fixture "bug_001_omega_let_smuggles_linear.affine") with
446+
| Error msg -> Alcotest.fail msg
447+
| Ok prog ->
448+
match resolve_program prog with
449+
| Error msg -> Alcotest.fail msg
450+
| Ok (ctx, _) ->
451+
match Typecheck.check_program ctx.symbols prog with
452+
| Ok _ ->
453+
Alcotest.fail "BUG-001 (attr form): expected quantity rejection of \
454+
@unrestricted let smuggling a @linear value, but the \
455+
checker accepted the program"
456+
| Error e ->
457+
let msg = Typecheck.format_type_error e in
458+
Alcotest.(check bool) "error mentions @linear vocabulary" true
459+
(try let _ = Str.search_forward (Str.regexp "@linear") msg 0 in true
460+
with Not_found -> false)
461+
462+
let test_bug_001_smuggles_linear_sugar_form () =
463+
match parse_fixture (fixture "bug_001_sugar_form.affine") with
464+
| Error msg -> Alcotest.fail msg
465+
| Ok prog ->
466+
match resolve_program prog with
467+
| Error msg -> Alcotest.fail msg
468+
| Ok (ctx, _) ->
469+
match Typecheck.check_program ctx.symbols prog with
470+
| Ok _ ->
471+
Alcotest.fail "BUG-001 (sugar form): expected quantity rejection of \
472+
:ω let smuggling a @linear value, but the checker \
473+
accepted the program"
474+
| Error e ->
475+
let msg = Typecheck.format_type_error e in
476+
Alcotest.(check bool) "error mentions @linear vocabulary" true
477+
(try let _ = Str.search_forward (Str.regexp "@linear") msg 0 in true
478+
with Not_found -> false)
479+
480+
let test_affine_let_valid_attr_form () =
481+
match parse_fixture (fixture "affine_let_valid.affine") with
482+
| Error msg -> Alcotest.fail msg
483+
| Ok prog ->
484+
match resolve_program prog with
485+
| Error msg -> Alcotest.fail msg
486+
| Ok (ctx, _) ->
487+
match Typecheck.check_program ctx.symbols prog with
488+
| Ok _ -> ()
489+
| Error e ->
490+
Alcotest.fail (Printf.sprintf
491+
"valid @linear let case rejected: %s"
492+
(Typecheck.format_type_error e))
493+
494+
let test_affine_let_valid_sugar_form () =
495+
match parse_fixture (fixture "affine_let_valid_sugar.affine") with
496+
| Error msg -> Alcotest.fail msg
497+
| Ok prog ->
498+
match resolve_program prog with
499+
| Error msg -> Alcotest.fail msg
500+
| Ok (ctx, _) ->
501+
match Typecheck.check_program ctx.symbols prog with
502+
| Ok _ -> ()
503+
| Error e ->
504+
Alcotest.fail (Printf.sprintf
505+
"valid :1 let case rejected: %s"
506+
(Typecheck.format_type_error e))
507+
438508
let quantity_tests = [
439509
Alcotest.test_case "valid affine usage" `Quick test_quantity_affine_valid;
440510
Alcotest.test_case "affine double use" `Quick test_quantity_affine_violation;
441511
Alcotest.test_case "erased usage" `Quick test_quantity_erased_violation;
512+
Alcotest.test_case "BUG-001 attr form rejects ω-let smuggling @linear"
513+
`Quick test_bug_001_smuggles_linear_attr_form;
514+
Alcotest.test_case "BUG-001 sugar form rejects :ω let smuggling @linear"
515+
`Quick test_bug_001_smuggles_linear_sugar_form;
516+
Alcotest.test_case "valid @linear let accepts" `Quick test_affine_let_valid_attr_form;
517+
Alcotest.test_case "valid :1 let accepts" `Quick test_affine_let_valid_sugar_form;
442518
]
443519

444520
(* ============================================================================

0 commit comments

Comments
 (0)