docs(design): reconcile models 0008/0009 STATUS with the shipped #55 cutover

The 0008 totality core shipped via #55 (spec 0062, 76b21c0), but both
model whitepapers still claimed "nothing here is shipped" — drift the
architect would flag.

- 0008: STATUS now "partially realised". Records what landed (binary
  ParamMode, value-type trivial-own, no mode-polymorphism, the hash
  reset) and points at the contract ledger for current-state facts.
  Marks §3.4/Q3 naming as resolved (verbal own/borrow kept, user
  decision); leaves the return-side escape axis (§5.1-5.2), multi-return
  (§5.3), and Q2/Q4 as the genuine remainder. escape.rs is named as the
  opt-only stack-promotion pass, not the §5.2 reachability check.
- 0009: STATUS stays "nothing shipped" (true), but the runtime-axis-dual
  paragraph now notes 0008's annotation axis landed, so 0009's
  precondition is met rather than hypothetical; the §8-Q3 coupling to
  0008's unshipped return-escape pass is flagged as still ahead.

Contract 0008-memory-model.md needed no change — already current.

design/models/0008-ownership-totality.md

@@ -1,16 +1,29 @@
 # Ownership totality — authored own/borrow everywhere whitepaper
 
-**STATUS.** *Design exploration — NOT current state, NOT an approved
+**STATUS.** *Partially realised — the totality core shipped; the
-milestone.* Nothing here is shipped; the present surface still has
+return-side soundness tail is still exploration.* The
-`ParamMode::Implicit` as the parser default on both parameters and
+annotation-totality direction this whitepaper converged on **landed**
-returns. This whitepaper records the **converged shape** of a possible
+via #55 (spec `../../docs/specs/0062-eliminate-implicit-mode.md`, commit
-direction — the points the design discussion has settled — and isolates
+`76b21c0`, 2026-06-02): `ParamMode::Implicit` is deleted, `ParamMode` is
-the genuinely-open questions in §7. The honesty rule
+binary `{Own, Borrow}` (§3.3), every fn-type slot carries an explicit
-(`../contracts/0007-honesty-rule.md`) governs the contract ledger, not
+mode including value-type slots (§3.2 trivial-`own`, `(borrow Int)` an
-this exploratory model: this file exists precisely to fix a future
+error), mode-polymorphism was not adopted (§4), and the one-time
-shape before committing it. When a direction here is chosen, it becomes
+canonical-hash reset (§6) is done. Those current-state facts now live in
-one or more specs under `docs/specs/`, and the current-state facts
+the contract ledger (`../contracts/0008-memory-model.md`), per the
-migrate into the contract ledger.
+honesty rule (`../contracts/0007-honesty-rule.md`) — read the contract,
+not this model, for what the compiler does today.
+
+What remains **exploration, not shipped**: the return-side soundness
+axis (§5.1–5.2 — the escape / return-provenance reachability pass). The
+cutover sidestepped it by *rejecting* `(ret (borrow T))` outright (spec
+0062 "Out of scope") rather than verifying it; `escape.rs` is the older
+opt-only stack-promotion pass, not this check. Multi-return (§5.3) is
+likewise unbuilt. The §3.4 / §7-Q3 naming question is **resolved, not
+open**: the keywords stay the verbal `own`/`borrow` (user decision
+2026-06-01, spec 0062 scope decision 1); the adjectival `owned`/`borrowed`
+was declined, so §3.4 is recorded rationale for a road not taken. The
+remaining §7 open questions are Q2 (scalar return-verification
+sequencing) and Q4 (multi-return adoption).
 
 *Refined 2026-06-01 by design discussion: §3.4 (the keywords are
 adjectival, not verbal), §4.4 (the no-mode-polymorphism result is

design/models/0009-explicit-rc.md

@@ -17,13 +17,21 @@ shape before committing it. If adopted, it revises the floor recorded in
 
 This is the **runtime-axis dual** of ownership totality
 (`0008-ownership-totality.md`). That whitepaper makes the *annotation*
-total — every position carries `own`/`borrow`, no `Implicit`. This one
+total — every position carries `own`/`borrow`, no `Implicit` — and its
-asks the question totality makes askable: once ownership is authored on
+core **shipped** via #55 (spec 0062, commit `76b21c0`, 2026-06-02), so
-every position, does the *runtime discipline* still have to be universal
+the precondition this proposal needs is now met, not hypothetical. This
-RC, or can it follow the annotation — affine values drop deterministically
+one asks the question that totality, now in place, makes askable: once
-with no refcount, and RC narrows to the positions that actually declare
+ownership is authored on every position, does the *runtime discipline*
-sharing? The two compose: 0008 makes ownership total in the type; 0009
+still have to be universal RC, or can it follow the annotation — affine
-makes the runtime mechanism track the type.
+values drop deterministically with no refcount, and RC narrows to the
+positions that actually declare sharing? The two compose: 0008 makes
+ownership total in the type; 0009 makes the runtime mechanism track the
+type. **Nothing in 0009 is built** — universal RC + uniqueness-elision
+(§1) is still the floor; what changed is only that 0008 cleared its
+runway. One coupling carried over intact: 0009's transitive `box`-drop
+(§8 Q3) leans on 0008's return-side escape pass, which 0008 did *not*
+ship (borrow-returns are rejected, not verified), so that dependency is
+still entirely ahead.
 
 ---