spec: effect-op-borrow — closing the hs RC discipline gap
hs.4 surfaced a leak the heap-str-abi spec didn't account for:
heap-Str slabs handed back by int_to_str / float_to_str and
immediately printed via io/print_str leak at scope close under
--alloc=rc. RED tests at e2e.rs (commit 592d87b) pin it.
Brainstorm settled on naming the rule rather than working
around it: Term::Do.args[*] are walked in Borrow position by
uniqueness and linearity passes, symmetric to Term::Ctor.args[*]
being walked in Consume position. The kind itself carries the
ownership default — no per-op field on EffectOpSig.
The rule alone doesn't close the leak; two heap-Str-specific
shape fixes follow (int_to_str / float_to_str gain ret_mode: Own;
drop_symbol_for_binder's App arm gets a Str carve-out symmetric
to field_drop_call's existing one). DESIGN anchor + WhatsNew +
audit-close from hs.5 roll into this milestone.
Grounding-check PASS — all nine load-bearing assumptions
ratified against currently-green tests (with the two RED tests
ratifying the leak as the spec's premise).
This commit is contained in:
@@ -0,0 +1,231 @@
|
||||
# Effect-op arguments are borrowed — Design Spec
|
||||
|
||||
**Date:** 2026-05-12
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
## Goal
|
||||
|
||||
Codify and implement the language rule that arguments to a
|
||||
`Term::Do` (effect-op call) are evaluated in **borrow** position,
|
||||
not consume position. The uniqueness and linearity passes today
|
||||
treat them as consumes, which both contradicts the intended
|
||||
semantics ("effects observe; they do not transfer ownership of
|
||||
their arguments") and produces a concrete bug: every heap-Str slab
|
||||
handed back by `int_to_str` / `float_to_str` and immediately
|
||||
printed via `io/print_str` leaks at scope close under
|
||||
`--alloc=rc`.
|
||||
|
||||
The two RED tests at `crates/ail/tests/e2e.rs::int_to_str_drop_balances_rc_stats`
|
||||
and `::str_field_in_adt_drops_heap_str_correctly` (commit
|
||||
`592d87b`) pin the leak; this milestone closes them. By doing so
|
||||
it also closes the heap-str-abi milestone's outstanding hs.5
|
||||
work (DESIGN anchor + WhatsNew + audit-close), which was held up
|
||||
waiting for this gap to be named and fixed.
|
||||
|
||||
## Architecture
|
||||
|
||||
The rule is symmetric with the already-shipped rule for
|
||||
`Term::Ctor.args`:
|
||||
|
||||
| AST node | arg position | reason |
|
||||
|-------------------|--------------|---------------------------------------------------------------------------|
|
||||
| `Term::Ctor.args` | Consume | constructor packs values into the cell; the cell owns them afterwards |
|
||||
| `Term::Do.args` | **Borrow** (new) | effect-op observes; the caller still owns whatever pointer it passed in |
|
||||
|
||||
This is a language rule, not a per-op annotation. `EffectOpSig`
|
||||
(`crates/ailang-check/src/builtins.rs:32`) deliberately stays as
|
||||
it is: no `param_modes`, no `ret_mode`. The kind *is* the
|
||||
ownership default — having an `EffectOpSig` at all means "borrow
|
||||
in, no out-ownership", just as having a `Ctor` at all means
|
||||
"consume in".
|
||||
|
||||
### The rule lives at three check-time sites
|
||||
|
||||
- **`crates/ailang-check/src/uniqueness.rs:289-292`** — today walks
|
||||
`Term::Do { args, .. }` with `Position::Consume`. Changes to
|
||||
`Position::Borrow`. Consequence: `consume_count` of a bare-`Var`
|
||||
argument is no longer bumped by the effect-op call, which is the
|
||||
signal the let-arm dec emission at
|
||||
`crates/ailang-codegen/src/lib.rs:1430-1466` reads when deciding
|
||||
whether to free the binder at scope close.
|
||||
- **`crates/ailang-check/src/linearity.rs:506-510`** — today walks
|
||||
`Term::Do { args, .. }` with `Position::Consume`. Changes to
|
||||
`Position::Borrow`. Consequence: a binder passed only to effect-ops
|
||||
no longer triggers `use-after-consume` on a second effect-op use.
|
||||
Two `io/print_str(s)` calls in sequence become a normal
|
||||
double-borrow, not a linearity error.
|
||||
- **`crates/ailang-check/src/linearity.rs:42`** — doc comment that
|
||||
lists per-arm consume/borrow positions. The bullet `Term::Ctor.args[*],
|
||||
Term::Do.args[*] — Consume` splits: `Term::Ctor.args[*]` stays
|
||||
in the Consume bullet; `Term::Do.args[*]` moves to the Borrow
|
||||
bullet alongside `Term::Match.scrutinee` and `Term::Clone.value`.
|
||||
|
||||
The third site is a doc comment, but it is part of the rule: the
|
||||
documentation that lies about the analyser is itself the bug we
|
||||
are fixing.
|
||||
|
||||
### DESIGN.md anchor
|
||||
|
||||
`docs/DESIGN.md` gets a new bullet under the
|
||||
uniqueness / effect section naming the rule symmetrically with
|
||||
the existing Ctor rule. This is the artefact the architect agent
|
||||
reads at audit time, so the rule has a single named home that
|
||||
future analyser code paths cannot accidentally diverge from.
|
||||
|
||||
### Heap-Str-specific consequences
|
||||
|
||||
The rule alone does not close the heap-Str leak. Two ABI-level
|
||||
fixes follow from the rule's interaction with hs.4's runtime
|
||||
additions:
|
||||
|
||||
1. **`int_to_str` and `float_to_str` switch to `ret_mode: Own`.**
|
||||
The two functions allocate a fresh heap-Str slab via
|
||||
`str_alloc` (runtime/str.c, iter hs.3) and hand the only
|
||||
outstanding pointer back to the caller. The codegen
|
||||
trackability gate at `crates/ailang-codegen/src/drop.rs:464-475`
|
||||
(iter 18g.2: `is_rc_heap_allocated` for a `Term::App` checks
|
||||
the callee's `ret_mode == Own`) is what tells the let-arm to
|
||||
emit a dec at scope close. Today both functions carry
|
||||
`ret_mode: Implicit` at `crates/ailang-check/src/builtins.rs:203-212`
|
||||
(and the float counterpart at `:193-202`) plus the codegen-side
|
||||
synth-replay at `crates/ailang-codegen/src/synth.rs:167-172`
|
||||
(float_to_str) and `:174-180` (int_to_str). All four sites
|
||||
switch to `Own`.
|
||||
|
||||
2. **`drop_symbol_for_binder` App arm gets a `Str` carve-out.**
|
||||
With `ret_mode: Own`, the let-binder is tracked, and at scope
|
||||
close codegen routes through
|
||||
`drop_symbol_for_binder(value=App, val_ssa=s)` at
|
||||
`crates/ailang-codegen/src/drop.rs:534-549`. That arm reads the
|
||||
call's static return type and forms `drop_<m>_<T>`. For
|
||||
`T = Str` there is no such drop fn — `Str` is a built-in
|
||||
pointer type with no recursive children, the same case the
|
||||
field-drop arm already handles at
|
||||
`crates/ailang-codegen/src/drop.rs:372-394` by returning
|
||||
`"ailang_rc_dec"`. The carve-out adds the symmetric arm in
|
||||
the App branch: `Type::Con { name: "Str", .. } → "ailang_rc_dec"`.
|
||||
|
||||
These two fixes are not part of the language rule. They are the
|
||||
shape the heap-Str realisation needs in order to *benefit* from
|
||||
the rule. A spec that named only the rule would leave the RED
|
||||
tests still red.
|
||||
|
||||
## Components
|
||||
|
||||
Touched files:
|
||||
|
||||
- `crates/ailang-check/src/uniqueness.rs:289-292` — Term::Do arg
|
||||
walk: `Position::Consume` → `Position::Borrow`.
|
||||
- `crates/ailang-check/src/linearity.rs:506-510` — Term::Do arg
|
||||
walk: `Position::Consume` → `Position::Borrow`.
|
||||
- `crates/ailang-check/src/linearity.rs:42` — doc-comment update:
|
||||
move `Term::Do.args[*]` from the Consume bullet to the Borrow
|
||||
bullet.
|
||||
- `crates/ailang-check/src/builtins.rs:193-202` — `float_to_str`
|
||||
signature: `ret_mode: Implicit` → `Own`.
|
||||
- `crates/ailang-check/src/builtins.rs:203-212` — `int_to_str`
|
||||
signature: `ret_mode: Implicit` → `Own`.
|
||||
- `crates/ailang-codegen/src/synth.rs:167-172` — `float_to_str`
|
||||
synth-replay: `ret_mode: Implicit` → `Own`.
|
||||
- `crates/ailang-codegen/src/synth.rs:174-180` — `int_to_str`
|
||||
synth-replay: `ret_mode: Implicit` → `Own`.
|
||||
- `crates/ailang-codegen/src/drop.rs:534-549` — App arm of
|
||||
`drop_symbol_for_binder`: add `Type::Con { name: "Str", .. } →
|
||||
"ailang_rc_dec"` carve-out before the generic
|
||||
`format!("drop_{m}_{name}")` fallthrough.
|
||||
- `docs/DESIGN.md` — new bullet anchoring the
|
||||
`Term::Do.args[*] = Borrow` rule under the uniqueness / effect
|
||||
section.
|
||||
- `crates/ail/tests/e2e.rs::int_to_str_drop_balances_rc_stats` —
|
||||
existing RED test; turns GREEN unchanged.
|
||||
- `crates/ail/tests/e2e.rs::str_field_in_adt_drops_heap_str_correctly`
|
||||
— existing RED test; turns GREEN unchanged.
|
||||
- `crates/ail/tests/snapshots/` — IR snapshots affected by the new
|
||||
let-arm dec at `int_to_str` callsites may need regeneration. No
|
||||
snapshot in the current `crates/ail/tests/snapshots/` directory
|
||||
invokes `int_to_str` directly, so this is expected to be a
|
||||
no-op; flagged here in case planner-recon finds otherwise.
|
||||
|
||||
## Data flow
|
||||
|
||||
The change does not affect canonical-JSON bytes. `ret_mode: Own`
|
||||
is already a serialised `ParamMode` variant; `Implicit` is the
|
||||
back-compat default which serialises via
|
||||
`skip_serializing_if = "ParamMode::is_implicit"`. Switching the
|
||||
value does not change the schema or the existing-fixture hashes,
|
||||
because no fixture in the workspace carries an explicit
|
||||
`ret_mode: Implicit` annotation on `int_to_str` or `float_to_str`
|
||||
(both are typechecker-installed, never user-written).
|
||||
|
||||
The change affects IR shape at exactly one class of callsite:
|
||||
`let x = (app int_to_str ...) in body` (and float variant). The
|
||||
new IR emits a `call void @ailang_rc_dec(ptr %x)` at scope close.
|
||||
Non-binding sites — `(do io/print_str (app int_to_str ...))`
|
||||
without an intervening let — are unaffected because no
|
||||
let-binder exists for the dec to attach to.
|
||||
|
||||
## Error handling
|
||||
|
||||
No new diagnostics. One existing diagnostic — `over-strict-mode`
|
||||
(Iter 19a / 19a.1) — becomes more sensitive: a `(own T)`
|
||||
parameter whose only use in the fn body is passing it to an
|
||||
effect-op now correctly fires the lint, because the body no
|
||||
longer counts that use as a consume.
|
||||
|
||||
This is the *intended* behaviour of the lint — the lint asks "is
|
||||
this `(own T)` annotation actually justified by a consume in the
|
||||
body?", and an effect-op call is not a consume. The flip surfaces
|
||||
parameters that were silently mis-annotated and is part of the
|
||||
milestone, not a regression.
|
||||
|
||||
Fixtures that fail the tightened lint will be re-annotated as
|
||||
part of this milestone's implementation iteration (planner will
|
||||
enumerate which ones during recon). If the planner finds the
|
||||
sweep nontrivial (more than a handful of fixtures), the
|
||||
re-annotation moves to its own follow-up iter rather than
|
||||
bloating the milestone.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
1. **Existing RED tests flip to GREEN.**
|
||||
`int_to_str_drop_balances_rc_stats` and
|
||||
`str_field_in_adt_drops_heap_str_correctly` at e2e.rs (commit
|
||||
`592d87b`). No fixture or assertion changes — the strict
|
||||
`allocs == frees && live == 0` invariants stay.
|
||||
2. **One new positive test: non-pointer effect-op arg.** Bind a
|
||||
let-Int, pass it to `io/print_int`, run with `--alloc=rc` and
|
||||
`AILANG_RC_STATS=1`. Confirms the rule does not introduce
|
||||
spurious bookkeeping on primitive arguments (Int is not a
|
||||
pointer; there is no slab to free; allocs and frees stay at
|
||||
zero).
|
||||
3. **One new positive test: repeated effect-op borrow.** Bind a
|
||||
let-Str (heap-allocated via `int_to_str`), pass it to
|
||||
`io/print_str` twice in sequence, confirm the fixture
|
||||
typechecks (no `use-after-consume`) and that the RC trace
|
||||
reports `allocs == frees && live == 0`.
|
||||
4. **Workspace-wide regression.** `cargo test --workspace`,
|
||||
`bench/cross_lang.py`, `bench/compile_check.py`,
|
||||
`bench/check.py` all green. Any `over-strict-mode`-driven
|
||||
fixture re-annotations land in the same milestone.
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
- Both existing RED tests at `crates/ail/tests/e2e.rs` pass with
|
||||
`allocs == frees && live == 0`.
|
||||
- Two new positive tests added (Int-arg primitive, repeated
|
||||
Str-arg borrow) — both green.
|
||||
- `cargo test --workspace`, `bench/cross_lang.py`,
|
||||
`bench/compile_check.py`, `bench/check.py` all green; any
|
||||
`over-strict-mode` failures resolved by fixture re-annotation
|
||||
inside the milestone.
|
||||
- `docs/DESIGN.md` carries a new bullet under the
|
||||
uniqueness / effect section naming the
|
||||
`Term::Do.args[*] = Borrow` rule, symmetric with the existing
|
||||
`Term::Ctor.args[*] = Consume` treatment.
|
||||
- `docs/WhatsNew.md` carries one entry written for the
|
||||
user-as-reader covering both the heap-Str RC close and the
|
||||
effect-op argument rule, in plain prose, no internals.
|
||||
- The heap-str-abi milestone is effectively closed by this
|
||||
milestone — hs.5's "DESIGN anchor + WhatsNew + audit-close"
|
||||
rolls in here. No separate hs.5 ships.
|
||||
Reference in New Issue
Block a user