Close Implicit on returns so heap-returning fns stop leaking #54

New Issue

2026-06-01T12:35:08+02:00

Brummel commented

2026-06-01 12:35:08 +02:00

Symptom

A fn whose return type is an RC-heap value (Str, or a boxed ADT) but
whose signature omits the return mode carries ret_mode == ParamMode::Implicit — the parser's silent default, which nothing
infers post-parse. Codegen reads Implicit faithfully: the caller does
not dec the returned slab, so the owned allocation leaks
(live = 1 under AILANG_RC_STATS).

This is currently documented as intentional under the Implicit
back-compat lane:

examples/rc_let_implicit_returning_app.ail asserts live = 1 as
the correct outcome (see its header comment).
design/contracts/0008-memory-model.md ("ret_mode —
let-binder trackability"): an Implicit-returning call is
non-trackable for scope-close drop, by contrast with an
Own-returning call.
Codegen gate: crates/ailang-codegen/src/drop.rs:469 — only
ret_mode == Own hands a fresh heap allocation to the caller and
enables the dec.

The leak is the symptom; the cause is that an ownership default exists
on the return position at all. ParamMode::Implicit is treated as
Own by the typechecker (mode_eq, crates/ailang-core/src/ast.rs)
yet read separately by codegen, which omits the caller dec — the same
fn-type read two ways.

Minimal fix

Scoped deliberately below the full ownership-totality direction in
design/models/0008-ownership-totality.md, which a critical design
review on 2026-06-01 found is not yet shippable as one atomic cutover
(borrowed returns are refcount-invisible and can outlive their source —
a use-after-free that needs a liveness/escape axis the model does not
yet have; see §1 and §8 of that whitepaper):

Close Implicit on the return position: require own or
borrow on every fn return. Parameter-side modes and value-type
uniformity stay out of scope here.
An own return needs only first-order freshness verification
("is this return actually fresh?"), not the reachability /
liveness pass.
Forbid borrow returns in this first cut. They are the
positions that need the unresolved liveness/escape axis (a
borrowed return aliasing a parameter can dangle once the caller
drops the source; RC does not back-stop it because a borrow does
no inc/dec). Re-enabling them is separate, later work.

Cost flagged

Closing Implicit on returns shifts the canonical JSON hash of every
fixture whose return mode was defaulted (ret_mode is omitted from the
hash only while Implicit — skip_serializing_if = "is_implicit",
crates/ailang-core/src/ast.rs). The hash-pin tests reset once. This
is the one irreversible step and is signed off deliberately.

Acceptance

A heap-returning fn with no return mode is a check error, not a
silent leak.
examples/rc_let_implicit_returning_app.ail is migrated to an
explicit own return and asserts live = 0.
A borrow return is rejected with a diagnostic naming the
liveness gap.

## Symptom A fn whose return type is an RC-heap value (`Str`, or a boxed ADT) but whose signature omits the return mode carries `ret_mode == ParamMode::Implicit` — the parser's silent default, which nothing infers post-parse. Codegen reads `Implicit` faithfully: the caller does **not** `dec` the returned slab, so the owned allocation leaks (`live = 1` under `AILANG_RC_STATS`). This is currently documented as intentional under the `Implicit` back-compat lane: - `examples/rc_let_implicit_returning_app.ail` asserts `live = 1` as the correct outcome (see its header comment). - `design/contracts/0008-memory-model.md` ("`ret_mode` — let-binder trackability"): an `Implicit`-returning call is non-trackable for scope-close drop, by contrast with an `Own`-returning call. - Codegen gate: `crates/ailang-codegen/src/drop.rs:469` — only `ret_mode == Own` hands a fresh heap allocation to the caller and enables the dec. The leak is the symptom; the cause is that an ownership default exists on the return position at all. `ParamMode::Implicit` is treated as `Own` by the typechecker (`mode_eq`, `crates/ailang-core/src/ast.rs`) yet read separately by codegen, which omits the caller `dec` — the same fn-type read two ways. ## Minimal fix Scoped deliberately *below* the full ownership-totality direction in `design/models/0008-ownership-totality.md`, which a critical design review on 2026-06-01 found is not yet shippable as one atomic cutover (borrowed returns are refcount-invisible and can outlive their source — a use-after-free that needs a liveness/escape axis the model does not yet have; see §1 and §8 of that whitepaper): - [ ] Close `Implicit` on the **return** position: require `own` or `borrow` on every fn return. Parameter-side modes and value-type uniformity stay out of scope here. - [ ] An `own` return needs only first-order freshness verification ("is this return actually fresh?"), not the reachability / liveness pass. - [ ] **Forbid `borrow` returns in this first cut.** They are the positions that need the unresolved liveness/escape axis (a borrowed return aliasing a parameter can dangle once the caller drops the source; RC does not back-stop it because a borrow does no inc/dec). Re-enabling them is separate, later work. ## Cost flagged Closing `Implicit` on returns shifts the canonical JSON hash of every fixture whose return mode was defaulted (`ret_mode` is omitted from the hash only while `Implicit` — `skip_serializing_if = "is_implicit"`, `crates/ailang-core/src/ast.rs`). The hash-pin tests reset once. This is the one irreversible step and is signed off deliberately. ## Acceptance - [ ] A heap-returning fn with no return mode is a `check` error, not a silent leak. - [ ] `examples/rc_let_implicit_returning_app.ail` is migrated to an explicit `own` return and asserts `live = 0`. - [ ] A `borrow` return is rejected with a diagnostic naming the liveness gap.

Brummel added the bug label 2026-06-01 12:35:08 +02:00

Brummel referenced this issue

2026-06-01 13:01:31 +02:00

Eliminate the Implicit ownership default — totality minus borrow-returns #55

Brummel commented

2026-06-01 13:02:02 +02:00

Closing: this targets the symptom (the return-position leak), not the
cause. Replaced by #55.

The whitepaper section 2 (design/models/0008-ownership-totality.md) names
the cause: an ownership default exists at all. #54 removes Implicit
only on the return position and explicitly leaves it on parameters —
which is exactly the partial default-removal section 2 calls incoherent
("the same default surviving on the input side").

Two substantive problems, beyond incompleteness:

Two irreversible hash resets. The canonical-JSON hash shifts once
when Implicit leaves a serialized position (section 6: "the one
genuinely irreversible consequence"). #54 spends that reset on returns
now; closing the parameter side later — the rest of totality — spends
a second one. One reset suffices for the whole surface.
It defers the already-finished half. The parameter side is
already verified — consume-while-borrowed, over-strict-mode, and
per-param consume_count (crates/ailang-check) police it today, and
section 5 notes the param mode is compiler-derivable from that
analysis. There is no soundness reason to hold parameters out of the
cutover; only the "returns are the hard half" framing pushed #54 to
exclude the easy, done half.

#55 keeps #54's one correct move (forbid borrow-returns behind the
unbuilt liveness axis) and drops the rest: it deletes Implicit as a
concept in one hash reset, instead of patching it per-position in two.

Closing: this targets the symptom (the return-position leak), not the cause. Replaced by #55. The whitepaper section 2 (design/models/0008-ownership-totality.md) names the cause: an ownership default exists at all. #54 removes `Implicit` only on the *return* position and explicitly leaves it on parameters — which is exactly the partial default-removal section 2 calls incoherent ("the same default surviving on the input side"). Two substantive problems, beyond incompleteness: 1. **Two irreversible hash resets.** The canonical-JSON hash shifts once when `Implicit` leaves a serialized position (section 6: "the one genuinely irreversible consequence"). #54 spends that reset on returns now; closing the parameter side later — the rest of totality — spends a second one. One reset suffices for the whole surface. 2. **It defers the already-finished half.** The parameter side is *already verified* — `consume-while-borrowed`, `over-strict-mode`, and per-param `consume_count` (crates/ailang-check) police it today, and section 5 notes the param mode is compiler-*derivable* from that analysis. There is no soundness reason to hold parameters out of the cutover; only the "returns are the hard half" framing pushed #54 to exclude the easy, done half. #55 keeps #54's one correct move (forbid borrow-returns behind the unbuilt liveness axis) and drops the rest: it deletes `Implicit` as a *concept* in one hash reset, instead of patching it per-position in two.

Brummel closed this issue

2026-06-01 13:02:02 +02:00

Brummel referenced this issue from a commit

2026-06-01 15:47:37 +02:00

spec: eliminate the Implicit ownership default (0062)

Brummel referenced this issue from a commit

2026-06-02 01:11:02 +02:00

feat(lang): eliminate the Implicit ownership default — totality + the drop-soundness it demasks (#55)

Sign in to join this conversation.