From 2ca483dbfd37e73ea9ae30b34ab7b05e5145384e Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 10:12:30 +0200 Subject: [PATCH] docs(design): reconcile models 0008/0009 STATUS with the shipped #55 cutover MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 35 ++++++++++++++++-------- design/models/0009-explicit-rc.md | 22 ++++++++++----- 2 files changed, 39 insertions(+), 18 deletions(-) diff --git a/design/models/0008-ownership-totality.md b/design/models/0008-ownership-totality.md index 8d9a4c8..29a41ba 100644 --- a/design/models/0008-ownership-totality.md +++ b/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 -milestone.* Nothing here is shipped; the present surface still has -`ParamMode::Implicit` as the parser default on both parameters and -returns. This whitepaper records the **converged shape** of a possible -direction — the points the design discussion has settled — and isolates -the genuinely-open questions in §7. The honesty rule -(`../contracts/0007-honesty-rule.md`) governs the contract ledger, not -this exploratory model: this file exists precisely to fix a future -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. +**STATUS.** *Partially realised — the totality core shipped; the +return-side soundness tail is still exploration.* The +annotation-totality direction this whitepaper converged on **landed** +via #55 (spec `../../docs/specs/0062-eliminate-implicit-mode.md`, commit +`76b21c0`, 2026-06-02): `ParamMode::Implicit` is deleted, `ParamMode` is +binary `{Own, Borrow}` (§3.3), every fn-type slot carries an explicit +mode including value-type slots (§3.2 trivial-`own`, `(borrow Int)` an +error), mode-polymorphism was not adopted (§4), and the one-time +canonical-hash reset (§6) is done. Those current-state facts now live in +the contract ledger (`../contracts/0008-memory-model.md`), per the +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 diff --git a/design/models/0009-explicit-rc.md b/design/models/0009-explicit-rc.md index 2e52b37..456e322 100644 --- a/design/models/0009-explicit-rc.md +++ b/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 -asks the question totality makes askable: once ownership is authored on -every position, does the *runtime discipline* still have to be universal -RC, or can it follow the annotation — affine 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. +total — every position carries `own`/`borrow`, no `Implicit` — and its +core **shipped** via #55 (spec 0062, commit `76b21c0`, 2026-06-02), so +the precondition this proposal needs is now met, not hypothetical. This +one asks the question that totality, now in place, makes askable: once +ownership is authored on every position, does the *runtime discipline* +still have to be universal RC, or can it follow the annotation — affine +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. ---