docs(design): refine the ownership-totality model from design discussion (0008)

A design discussion on 0008 surfaced four refinements; this records them
in the exploratory model. Still design exploration, not a spec commitment.

- §3.4 (new): the keywords are adjectival, not verbal. `own`/`borrow`
  are acquisition verbs — native on a parameter (the callee acquires),
  backwards on a return (the callee disposes; §3.1's own text switches
  feet between the two readings). Naming the mode adjectivally
  (`owned`/`borrowed`) describes the value the receiver holds and is
  position-independent, strengthening §3's uniformity rather than
  breaking it. Carries a safety stake, not only readability: a wrong
  `own` is the double-free (§6), and the verb form is a mis-annotation
  pump pointed that way. Notes the corroborating `ret_mode: ParamMode`
  type-name smell (a return mode is a covariant promise, not a
  contravariant param demand).

- §4.4: "fixed modes suffice" is contingent on the point-free cut, not a
  standalone theorem. Adds the structural discriminator — today's HOFs
  control both ends of their seam, so the seam mode is determinate; only
  the wire-two-black-boxes kind (point-free) needs a mode variable.

- §5.1–5.3 (new): a tuple question exposed that `ret_mode` is flat but
  ownership is a tree over the type — a single top-level `Own` on a
  mixed Pair (owned field + borrowed field) decs borrowed data on drop.
  Resolved to regime A (borrows may not escape into an escaping heap
  structure → transitive ownership → flat `ret_mode` sound), not a
  per-field mode tree (regime B = lifetimes). For compound returns,
  verification is constitutive of the flat representation's meaning, not
  a separable phase — sharpening Q2 to "must" there. Multi-return is the
  ownership-honest return path (flat per-position modes, no reachability
  pass) but does not subsume the typed boxed aggregate; the boxing point
  is the ownership commit.

- §7: Q2 sharpened (compound returns force it), Q3 rewritten (adjectival
  keywords + the pre-cutover timing, since a post-cutover rename is a
  second irreversible hash reset), Q4 added (multi-return adoption);
  resolved-footer extended with regime A and multi-return≠tuple.

- §8 (new): relation to Rust. Concedes the primitive-level convergence
  (own/borrow ≈ move/borrow, regime A ≈ Rust's escape rule, unboxed
  product ≈ tuple, RC ≈ Rc/Arc), then names what AILang drops and why:
  no lifetime polymorphism (the point-free cut removes the pressure that
  makes Rust carry it), no `&mut`/shared-XOR-mutable (no shared mutable
  refs; mutation rides uniqueness, the Clean lineage), no elision (§2's
  no-defaults is the opposite of Rust's elision). Scoped to the
  totality-relevant divergences; the broader memory-model lineage is
  cross-referenced to 0004 rather than duplicated.

design/models/0008-ownership-totality.md

@@ -12,6 +12,12 @@ shape before committing it. When a direction here is chosen, it becomes
 one or more specs under `docs/specs/`, and the current-state facts
 migrate into the contract ledger.
 
+*Refined 2026-06-01 by design discussion: §3.4 (the keywords are
+adjectival, not verbal), §4.4 (the no-mode-polymorphism result is
+contingent on the point-free cut), §5.1–5.3 (compound returns are an
+ownership tree; multi-return is the ownership-honest return path), and
+the sharpened §7 questions, and §8 (relation to Rust).*
+
 ---
 
 ## 1. The leak that motivates it
@@ -110,6 +116,53 @@ metadata fields on `Type::Fn` (`param_modes`, `ret_mode`), not new
 fn-parameter positions, not to types in general). There is **no** mode
 variable and **no** third polymorphic axis — see §4.
 
+### 3.4 The keywords are adjectival, not verbal
+
+`own` and `borrow` are *acquisition verbs* — they name what the
+receiver at a position does. On a parameter the receiver is the callee
+and the verb reads natively: `borrow param` = "I borrow this, the
+caller keeps it"; `own param` = "I take ownership." On a *return* the
+receiver flips to the caller, and the same verb reads backwards from the
+author's viewpoint: `own ret` means "I *hand* ownership away," `borrow
+ret` means "I *lend* a view" — the author is the lender, not the
+borrower. The same word names opposite roles on the two sides. §3.1's
+own text shows the seam: it glosses `own` as "ownership is handed to the
+caller" (the return reading) but states the authoring rule as "reach for
+`borrow` only when reading a value you were lent" (the param reading).
+The polarity reframe unifies the *bit* (transfer vs. alias) but not the
+*verb*.
+
+The fix is to name the mode adjectivally — as a property of the value
+the receiver holds, not an act of acquisition. `owned` / `borrowed`
+(past participles, i.e. adjectives) are position-independent because an
+adjective describes the thing, not the directed act: `(param (owned
+Str))` and `(ret (owned Str))` both read as "an owned Str"; `(ret
+(borrowed Str))` reads as "returns a borrowed Str" — the idiomatic form,
+where the bare imperative `borrow` does not. The deep invariant §3 wants
+to unify (transfer vs. alias is a property of the value) was always
+position-independent; only the verb form obscured it, so the participle
+*strengthens* the uniformity argument rather than breaking it. §3.2's
+value-type rule is unaffected: `(borrowed (con Int))` is as plainly an
+error as `(borrow (con Int))`. And the Rust-familiarity that the
+feature-acceptance gate rewards is preserved — the idiomatic English is
+already "returns a *borrowed* str / an *owned* String," never "returns
+*borrow* str."
+
+This is not merely aesthetic. §6 names a wrong `own` (declared own,
+actually an alias) as the double-free — the dangerous direction, and the
+one totality pushes authors toward. If `own` on a return connotes "I
+take ownership" to an author when it means "I give ownership away," the
+verb form is a mis-annotation pump pointed straight at the double-free.
+The choice carries a safety stake, not only a readability one.
+
+A corroborating code smell: `ret_mode` today has the *type* `ParamMode`
+(`crates/ailang-core/src/ast.rs`). A return mode is not a param mode — a
+param mode is a *demand on the caller* (contravariant), a return mode is
+a *promise to the caller* (covariant): the same two-element lattice read
+in opposite variance. That is why one verb fits both badly. The shared
+type wants a position-neutral name (`Ownership`, `TransferMode`) rather
+than the param-centric one. The naming question is tracked in §7 Q3.
+
 ## 4. Fixed modes suffice — why there is no mode-polymorphism
 
 A natural objection: passthrough functions — `id`, projections, `apply`
@@ -190,6 +243,22 @@ The discipline leans entirely on features the language already has:
 `ParamMode` stays binary; "every position carries a concrete
 `own`/`borrow`" holds literally, with no third-axis footnote.
 
+One honesty caveat on §4 as a whole: "fixed modes suffice" is
+*contingent on the point-free cut*, not independent of it. §4.2 already
+says the duality "bites only in code AILang does not have" — the
+load-bearing word is *have*. If AILang ever un-cut higher-order routing
+combinators (`compose`, `apply`, `id`-as-argument — the HOFs that
+control *neither* end of their seam and merely wire two black-box
+functions whose modes come from the caller), the reuse-across-modes
+clash returns and the mode-variable question reopens. The honest
+statement is "*given* the point-free cut, fixed modes suffice" — a
+dependency, not a standalone theorem. The structural discriminator that
+makes today's HOFs safe is that each (`map`, `fold`, `find`,
+`map_first`) controls *both* ends of its seam — it reads the element out
+of the container it owns and builds the result — so the seam mode is
+determinate per definition; only the wire-two-black-boxes kind needs a
+mode variable, and that kind *is* point-free.
+
 ## 5. Two orthogonal axes: totality vs soundness
 
 These must not be conflated:
@@ -215,6 +284,100 @@ propose each parameter's correct mode. The *return* side is the half
 with no verification yet; it needs new return-provenance ("escape")
 analysis.
 
+### 5.1 Compound returns: ownership is a tree, `ret_mode` is flat
+
+The orthogonality above is clean for a *scalar* return. It frays for a
+*compound* one. A returned `(Pair a b)` is a single heap node, and
+`ret_mode == Own` says the caller owns the *box* — but the two fields
+carry their own ownership. A function returning a Pair of {a fresh
+`Str`, a view into a borrowed argument} has an owned box, an owned field
+0, and a *borrowed* field 1. A single top-level `Own` directs the caller
+to recursively `dec` the whole box, whose drop decs field 1 → **dec of
+borrowed data → use-after-free.** Ownership is a property of every heap
+node in the type tree; one bit at the root cannot describe the interior.
+This is not return-specific — a `Pair`-typed *parameter* has the same
+interior that the flat `param_modes` entry does not cover; it is
+sharpest on returns because returns escape.
+
+There are two regimes, and the choice decides whether a flat `ret_mode`
+is enough:
+
+- **(A) Borrows may not escape into an escaping heap structure.** Then
+  every field of a returned box is necessarily owned, ownership is
+  transitive from the root, and the flat `ret_mode` is sufficient *and
+  sound* — precisely because the mixed case is forbidden at
+  construction. The price: to return a view as part of a structure, you
+  must `clone` it to owned first. This is Rust's "cannot return a struct
+  borrowing a local," minus lifetime variables.
+- **(B) Borrows may escape, tracked per field.** Then the mode
+  annotation becomes a *tree mirroring the type tree*, and to verify a
+  borrowed field you must name *what it borrows from* — i.e. lifetime
+  parameters. That is a different, much larger language, and it fails
+  the "no human-hostile complexity without enough correctness gain"
+  gate.
+
+AILang takes (A). §3.1's own gloss ("a view into data owned upstream")
+already points there: for an escaping box field, "upstream" is gone once
+the caller holds the box, so the borrow concept is ill-defined.
+
+### 5.2 For compound returns, verification is constitutive, not phased
+
+This is where §5's "two orthogonal axes" claim needs a caveat. The flat
+`ret_mode == Own` on a Pair *means* "the caller may recursively free"
+only if it is guaranteed that nothing borrowed is reachable from the
+box. That guarantee **is** the escape analysis. So the return-side pass
+is not the first-order "is this return fresh?" of §5/§6 — it is "is
+*everything reachable from this return* owned?", and it is not a
+*separable, deferrable* axis: it is what makes the flat `ret_mode` a
+sound representation at all. For compound returns, representation and
+verification are a *coupled pair*. This pushes §7 Q2 from "should
+return-verification land with the cutover" to "*must*, for any cutover
+that lets `Own` stand on a boxed return" — an unverified `Own` on a
+mixed Pair is not merely untrusted, it is unsound by construction.
+
+### 5.3 Multi-return is the ownership-honest return path
+
+An *unboxed multi-return* (several results handed back in registers, no
+heap node) dissolves the tree problem for the return case. With no box
+there is no "owned box / borrowed field" interior: each returned value
+is its own top-level position with its own mode — `ret_mode` becomes a
+`Vec<ParamMode>`, symmetric with `param_modes`. A `(owned Str, borrowed
+Str)` multi-return is flat and sound *without* the reachability pass,
+because the borrow flows *alongside* the owned value, not *inside* it
+(it aliases an argument the caller still holds); only the scalar
+return-provenance check applies, per position, never the reachability
+check. The boxed Pair forces homogenisation toward owned (regime A's
+mandatory `clone`); multi-return does not, because no shared box forces
+the values to share a fate. So on the ownership axis multi-return is
+strictly the *simpler* side.
+
+Multi-return does **not** subsume the tuple. They answer orthogonal
+questions: multi-return is an ABI for one position; a `data` aggregate
+is a *value* with a *type*, and only a typed value can be a list
+element, a constructor field, instantiate `forall a`, or be held across
+iterations. The moment aggregation is structural or durable, the box is
+required. The two compose: a multi-return *position* may itself be a
+Pair, which then takes the transitive treatment while its siblings stay
+flat — orthogonal layers, not competitors.
+
+The boundary between them is a meaningful authored decision, not a
+routing detail — symmetric with the §4.2 consume/preserve split. Boxing
+*is* the ownership commit: "do I box these?" = "do I commit them to one
+owned aggregate that outlives the call?", and under regime A that is
+exactly the point a borrowed member must `clone` to owned. Multi-return
+= results not yet committed, each keeping its mode; `data`-boxing =
+commit to a single owned aggregate.
+
+Whether AILang *adds* multi-return is a feature-gate question separate
+from totality, but the gate's answer leans yes: the present idiom
+"allocate a Pair, then `match` it apart at the call site" is a
+measurable redundancy (a heap alloc + dec for a value that never lived
+as an aggregate), and multi-return is the only ownership-honest way to
+return heterogeneous modes. It never removes the need for the boxed
+aggregate; it shrinks what the return-side escape pass must cover (only
+boxed returns need the reachability check of §5.2), which is an argument
+to weigh it *before* fixing the escape-analysis scope.
+
 ## 6. Costs and consequences (named honestly)
 
 - **Total migration.** Every signature in the corpus and prelude gains
@@ -257,15 +420,86 @@ scope entirely — a saving, not a debt.
 2. **Verification sequencing.** Is require-and-trust an acceptable
    interim on the soundness axis, given the double-free risk of a wrong
    `own`? Or should return-side `own`-verification land *with* the
-   totality cutover rather than after it?
+   totality cutover rather than after it? §5.2 partly forces this: for
+   *compound* returns, verification is constitutive of the flat
+   `ret_mode`'s meaning, so "with the cutover" is mandatory wherever
+   `Own` may stand on a boxed return — the open part is only the
+   *scalar* return.
 
-3. **Naming.** If this lands, the glossary should pin the vocabulary
+3. **Naming.** §3.4 argues the keywords should be adjectival
-   (mode, `own`/`borrow`, trivial-`own`, the projection/extraction/clone
+   (`owned`/`borrowed`), not the acquisition verbs (`own`/`borrow`) that
-   rule) before drift sets in.
+   read backwards on returns, and that the shared `ParamMode` type wants
+   a position-neutral name (`Ownership`). Open: adopt the participle
+   form, or keep the bare Rust-familiar verbs? Either way the choice
+   should land *before* the cutover — the §6 hash reset is the one
+   irreversible step, and renaming the keyword post-cutover would be a
+   second one. The glossary should then pin the vocabulary (mode, the
+   chosen keywords, trivial-`own`, the projection/extraction/clone rule)
+   before drift sets in.
+
+4. **Multi-return adoption.** Should AILang add unboxed multi-return
+   alongside boxed aggregates (§5.3)? It is the ownership-honest return
+   path (flat per-position modes, no reachability pass) and removes the
+   allocate-then-immediately-`match` redundancy, but it is a second
+   return mechanism with its own surface syntax and a `Vec` `ret_mode`.
+   Its scope interacts with the cutover: adopting it shrinks what the
+   return-side escape pass must cover, so it is worth deciding *before*
+   fixing the escape-analysis scope.
 
 **Resolved by the converged shape above** (no longer open): re-scope to
 totality (§2), value-type mode policy → trivial-`own` (§3.2),
-mode-polymorphism → not adopted; fixed modes suffice (§4).
+mode-polymorphism → not adopted; fixed modes suffice (§4);
+compound-return ownership → regime A, a flat `ret_mode` + transitivity
+rather than a per-field mode tree (§5.1); multi-return does not subsume
+the boxed tuple (§5.3).
+
+## 8. Relation to Rust (and why this is not a rebuild)
+
+The vocabulary here is Rust's, and pretending otherwise would violate
+the honesty rule: `own`/`borrow` ≈ move/borrow, a borrowed return ≈
+`&T`, regime A (§5.1) ≈ Rust's "cannot return a struct borrowing a
+local," the unboxed heterogeneous product (§5.3) ≈ a Rust tuple,
+ownership recovery via `clone` ≈ `.clone()`, RC ≈ `Rc`/`Arc`. An LLM
+author reaches for these *because* it has read Rust; inventing fresh
+names for the same concepts would be vanity and worse for the author.
+
+But adopting the vocabulary is not rebuilding the language. The bulk of
+Rust's complexity is machinery AILang's identity removes the pressure
+for, and the removals are principled, not effort-driven:
+
+- **No lifetime/mode polymorphism.** Rust's lifetime *variables* — with
+  their variance, subtyping, `for<'a>` (HRTB), reborrowing, NLL — exist
+  largely so a human can write one reusable generic abstraction across
+  many lifetime instantiations. That is the exact analogue of the
+  mode-polymorphism §4 declines, and for the same reason: AILang cut
+  point-free (§4.4), so the pressure that forces Rust to carry lifetime
+  variables evaporates. "Rust without lifetimes" is something Rust
+  itself cannot be, because its human audience demands the combinator
+  style AILang forbids.
+- **No `&mut`, no shared-XOR-mutable.** The genuinely hard part of
+  Rust's borrow checker — policing aliased mutation — is out of scope:
+  the memory model has no shared mutable references
+  (`../contracts/0008-memory-model.md`), and `borrow` is a read-only
+  view. In-place update rides *uniqueness/linearity* (update iff
+  statically unique — the Clean/linear-types lineage), not exclusive
+  borrows. AILang draws its mutation-safety from a different tradition
+  than its borrow vocabulary; see `0004-rc-uniqueness.md`.
+- **No elision; the opposite of Rust on defaults.** Rust *has* lifetime
+  elision — a default that omits annotations for human convenience.
+  §2's totality is the opposite stance: nothing is defaulted, because a
+  default is the trust break local reasoning forbids. On the default
+  question AILang is *stricter* than Rust, not a copy of it.
+
+So this is not "Rust" but the *fixed-mode, monomorphic,
+read-only-borrow, elision-free fragment* of Rust's ownership
+vocabulary, with mutation-safety from the uniqueness tradition and RC as
+the floor (`0004-rc-uniqueness.md`) — a hybrid none of the source
+languages is. The transferable parts (ownership is binary
+transfer-vs-alias; borrows must not escape; recovering a view costs a
+`clone`) are not Rust inventions but the physics of refcount-free
+memory, which one adopts rather than rebuilds. One would be rebuilding
+Rust only by *also* taking the lifetime apparatus — and §2, §3.4, and §4
+are jointly the argument for why this does not.
 
 ---