Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

Harden linearity for universal activation, part 2 — #55 cutover precondition #57

New Issue
Closed
opened 2026-06-01 16:54:14 +02:00 by Brummel · 1 comment
Brummel commented 2026-06-01 16:54:14 +02:00
Owner
Copy Link
Copy Source

Discovered while executing the #55 cutover (plan 0121, Task 4 Phase A): the cutover's central precondition — that deleting ParamMode::Implicit turns the strict linearity check on universally and the migrated corpus passes cleanly — is false. #56 (spec 0063) closed two false-positive classes (value-type params; application-is-a-borrow). Universal activation surfaces at least three more false-positive classes plus one genuine corpus over-consume. Migrating the corpus to explicit modes (so the check activates everywhere) and applying the plan's mechanical own→borrow rule clears only the read-only-heap params; 11 fixtures stay hard-RED on shapes no mode annotation can fix.

The cutover was correctly stopped before the irreversible variant deletion (main untouched). This is the "#56 part 2" hardening that must land before #55 can ship.

Blocking classes

  1. Local HOF function params. callee_arg_modes resolves only global fns, never local function-typed params (crates/ailang-check/src/linearity.rs:755 — "Locals never carry fn-types in 18c.2"). So (app p h) with p a local (borrow a) predicate param treats h as consumed regardless of p's declared borrow slot. std_list.filter reuses h after (app p h) → false use-after-consume. Blocks std_list.ail + 7 importers.

  2. Let-alias of a borrowed value. Term::Let walks its value in Position::Consume (linearity.rs:506); design/contracts/0008-memory-model.md:340 documents this propagation as explicitly not shipped. rc_let_alias_implicit_param.pin_aliased does (let a t (match a …)) over a value the recursive loop must reuse → false consume-while-borrowed.

  3. Inferred value-typed let-binders. Conservatively tracked as heap (aaa70d4 scope decision: "value-typed let-binders stay conservatively tracked as heap; their type is inferred, not annotated, and the linearity walk does not re-run inference"). eqord_3_newton_sqrt.iterate binds (let xnew (app / …) …) (a Float) and uses it twice → false use-after-consume. Not a param; no mode annotation applies.

  4. Genuine double-consume needing a body rewrite (corpus bug, not a false positive). std_either_list.partition_eithers projects both (app Pair.fst rest) and (app Pair.snd rest) from one owned Pair; fst/snd move their field out, so each consumes the Pair. The fix is a body rewrite ((match rest (case (MkPair ls rs) …)) — destructure once), out of the migration's mechanical scope.

Classes 1–3 are check false positives (the check is not yet precise enough for shapes that Implicit's gated-off activation was hiding); class 4 is a real fixture over-consume.

Direction (for brainstorm, not decided here)

Re-brainstorm spec 0062 (or a dedicated hardening spec). The cutover needs check-hardening for classes 1–3 (local-HOF-param mode resolution + let-alias / value-let-binder propagation) and the class-4 body rewrite scoped in, before the irreversible deletion. Do not patch a fifth phase onto plan 0121 (project rule: 2+ blocking classes = spec defect).

Plan 0121's Tasks 1 (borrow-return reject) and 3 (throwaway ail migrate-modes tool) already landed on main (e1c9089, 39b674c) and are unaffected — they are additive and green. Only Task 4 (the cutover) is blocked on this.

Blocks #55.

Discovered while executing the #55 cutover (plan 0121, Task 4 Phase A): the cutover's central precondition — that deleting `ParamMode::Implicit` turns the strict linearity check on universally **and the migrated corpus passes cleanly** — is **false**. #56 (spec 0063) closed two false-positive classes (value-type params; application-is-a-borrow). Universal activation surfaces at least three more false-positive classes plus one genuine corpus over-consume. Migrating the corpus to explicit modes (so the check activates everywhere) and applying the plan's mechanical `own→borrow` rule clears only the read-only-heap params; 11 fixtures stay hard-RED on shapes no mode annotation can fix. The cutover was correctly stopped **before** the irreversible variant deletion (main untouched). This is the "#56 part 2" hardening that must land before #55 can ship. ## Blocking classes 1. **Local HOF function params.** `callee_arg_modes` resolves only global fns, never local function-typed params (`crates/ailang-check/src/linearity.rs:755` — "Locals never carry fn-types in 18c.2"). So `(app p h)` with `p` a local `(borrow a)` predicate param treats `h` as consumed regardless of `p`'s declared borrow slot. `std_list.filter` reuses `h` after `(app p h)` → false `use-after-consume`. Blocks `std_list.ail` + 7 importers. 2. **Let-alias of a borrowed value.** `Term::Let` walks its value in `Position::Consume` (`linearity.rs:506`); `design/contracts/0008-memory-model.md:340` documents this propagation as explicitly **not shipped**. `rc_let_alias_implicit_param.pin_aliased` does `(let a t (match a …))` over a value the recursive loop must reuse → false `consume-while-borrowed`. 3. **Inferred value-typed let-binders.** Conservatively tracked as heap (`aaa70d4` scope decision: "value-typed let-binders stay conservatively tracked as heap; their type is inferred, not annotated, and the linearity walk does not re-run inference"). `eqord_3_newton_sqrt.iterate` binds `(let xnew (app / …) …)` (a Float) and uses it twice → false `use-after-consume`. Not a param; no mode annotation applies. 4. **Genuine double-consume needing a body rewrite** (corpus bug, not a false positive). `std_either_list.partition_eithers` projects both `(app Pair.fst rest)` and `(app Pair.snd rest)` from one owned `Pair`; `fst`/`snd` move their field out, so each consumes the Pair. The fix is a body rewrite (`(match rest (case (MkPair ls rs) …))` — destructure once), out of the migration's mechanical scope. Classes 1–3 are check false positives (the check is not yet precise enough for shapes that Implicit's gated-off activation was hiding); class 4 is a real fixture over-consume. ## Direction (for brainstorm, not decided here) Re-brainstorm spec 0062 (or a dedicated hardening spec). The cutover needs check-hardening for classes 1–3 (local-HOF-param mode resolution + let-alias / value-let-binder propagation) and the class-4 body rewrite scoped in, **before** the irreversible deletion. Do not patch a fifth phase onto plan 0121 (project rule: 2+ blocking classes = spec defect). Plan 0121's Tasks 1 (borrow-return reject) and 3 (throwaway `ail migrate-modes` tool) already landed on main (e1c9089, 39b674c) and are unaffected — they are additive and green. Only Task 4 (the cutover) is blocked on this. Blocks #55.
Brummel added the feature label 2026-06-01 16:54:14 +02:00
Brummel commented 2026-06-01 20:29:51 +02:00
Author
Owner
Copy Link
Copy Source

Resolved. Spec 0064 (the #56 part-2 hardening) landed in four iterations plus a drift-clean audit (dfdc65f):

  • iter 1 (47964ab): teed a (def,binder)->Type table out of the typecheck pass and exempted value-typed let-binders from consume-tracking (class 3).
  • iter 2 (cc5991e): resolve local function-typed binder modes in callee_arg_modes (class 1, local HOF function params).
  • iter 3 (be259f9): let-alias borrow propagation via an alias-redirect map; closed the design/contracts/0008-memory-model.md let-alias carve-out (class 2).
  • iter 4 (2769e50): rewrote std_either_list.partition_eithers to destructure its recursive result once, removing the one genuine corpus double-consume (class 4); pinned both the rejected and accepted shapes.

All four false-positive / over-consume classes that universal linearity activation surfaced are closed. The analysis is now correct on its own terms — it fixed real misfires in the linearity check — independent of the cutover it was scoped as a precondition for. Bench gates green (check.py 34/34, compile_check.py 24/24).

Context: #55 (the narrow ParamMode::Implicit-deletion cutover) is closed; the broader runtime-axis rethink is captured in design/models/0009-explicit-rc.md (a design exploration, not an approved milestone). This hardening stands on its own merits regardless of how or when the implicit-ownership default is eventually removed.

Resolved. Spec 0064 (the #56 part-2 hardening) landed in four iterations plus a drift-clean audit (dfdc65f): - iter 1 (47964ab): teed a (def,binder)->Type table out of the typecheck pass and exempted value-typed let-binders from consume-tracking (class 3). - iter 2 (cc5991e): resolve local function-typed binder modes in callee_arg_modes (class 1, local HOF function params). - iter 3 (be259f9): let-alias borrow propagation via an alias-redirect map; closed the design/contracts/0008-memory-model.md let-alias carve-out (class 2). - iter 4 (2769e50): rewrote std_either_list.partition_eithers to destructure its recursive result once, removing the one genuine corpus double-consume (class 4); pinned both the rejected and accepted shapes. All four false-positive / over-consume classes that universal linearity activation surfaced are closed. The analysis is now correct on its own terms — it fixed real misfires in the linearity check — independent of the cutover it was scoped as a precondition for. Bench gates green (check.py 34/34, compile_check.py 24/24). Context: #55 (the narrow ParamMode::Implicit-deletion cutover) is closed; the broader runtime-axis rethink is captured in design/models/0009-explicit-rc.md (a design exploration, not an approved milestone). This hardening stands on its own merits regardless of how or when the implicit-ownership default is eventually removed.
Sign in to join this conversation.
No Branch/Tag Specified
Branches Tags
Labels
Clear labels
BLOCKER
Core functionality broken — takes precedence over everything else in the queue. /boss preempts current work to handle it
 bug
Observable misbehaviour — surface inconsistency, false positive, wrong output
 feature
Smaller addition inside a milestone, no full spec
 idea
Not yet decision-ready, no commitment
No Label feature
Milestone
No items
No Milestone
Projects
Clear projects
No project
Assignees
Clear assignees
claude (Claude) Brummel
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: Brummel/AILang#57
Delete Branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?