diff --git a/docs/specs/2026-05-12-effect-op-borrow.md b/docs/specs/2026-05-12-effect-op-borrow.md
new file mode 100644
index 0000000..6a6c170
--- /dev/null
+++ b/docs/specs/2026-05-12-effect-op-borrow.md
@@ -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.