|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += Groove Ranked-Ownership Cleave Specification |
| 4 | +:doctype: book |
| 5 | +:toc: left |
| 6 | +:toclevels: 4 |
| 7 | +:sectnums: |
| 8 | +:source-highlighter: highlight.js |
| 9 | +:icons: font |
| 10 | + |
| 11 | +[.text-center] |
| 12 | +*Internet-Draft Style Specification* + |
| 13 | +*Version 0.2.0-draft.1* + |
| 14 | +*July 2026* |
| 15 | + |
| 16 | +== Abstract |
| 17 | + |
| 18 | +A _groove_ is the estate's inter-service capability-discovery and data protocol: |
| 19 | +a bidirectional interface between two systems, each usable standalone but |
| 20 | +enhanced when co-present. This document specifies the **Ranked-Ownership |
| 21 | +Cleave** — the discipline by which a groove connection closes cleanly and |
| 22 | +*provably leaves no residue*. |
| 23 | + |
| 24 | +It covers the **B2 (live-governance / lifecycle-residue)** layer of the groove |
| 25 | +cleave surface only. It deliberately does not specify **A** (discovery), **B1** |
| 26 | +(admissibility / compatibility), **C1** (logical schema), or **C2** (framing / |
| 27 | +transport); those are separate documents. |
| 28 | + |
| 29 | +== Status of This Memo |
| 30 | + |
| 31 | +This document specifies an experimental protocol for the estate. It is a |
| 32 | +normative standard in `hyperpolymath/standards`; conformance is defined in |
| 33 | +<<conformance>>. Discussion and suggestions for improvement are requested. |
| 34 | +It supersedes the ad-hoc `docs/proofs/spec-templates/T2-high/groove-browser-harness.md` |
| 35 | +as the canonical statement of groove teardown discipline. |
| 36 | + |
| 37 | +== Copyright Notice |
| 38 | + |
| 39 | +Copyright (c) 2025-2026 Jonathan D.A. Jewell. Released under CC-BY-SA-4.0. |
| 40 | + |
| 41 | +== 1. Introduction |
| 42 | + |
| 43 | +Every inter-service boundary in the estate is (or may become) a groove. Because |
| 44 | +a groove holds resources on both sides — sockets, leases, secrets, panel |
| 45 | +attachments — its *teardown* is where resource-safety is won or lost. The |
| 46 | +Ranked-Ownership Cleave gives teardown a machine-checkable meaning: a connection |
| 47 | +that has been released holds **zero residue** (`⊥`), and it does so by |
| 48 | +construction, not by discipline. |
| 49 | + |
| 50 | +The design underwrites the estate's no-GC / no-refcount posture: if ownership is |
| 51 | +a well-founded relation, ownership cycles are unrepresentable, so there is |
| 52 | +nothing for a cycle-collector to collect. |
| 53 | + |
| 54 | +== 2. Terminology |
| 55 | + |
| 56 | +The key words *MUST*, *MUST NOT*, *SHOULD*, and *MAY* are to be interpreted as |
| 57 | +in BCP 14 (RFC 2119, RFC 8174). |
| 58 | + |
| 59 | +Occupancy:: A renewable-lease measure over a live connection. It decreases on |
| 60 | +connect and is renewed by heartbeat; it bounds "quiet squatting" (a peer holding |
| 61 | +a slot without traffic). |
| 62 | + |
| 63 | +Discharge:: A teardown measure. It decreases on each release step and is bounded |
| 64 | +below by `⊥`. `⊥` denotes **zero residue**: no stored peer identity, no held |
| 65 | +secret, no reachable handle. |
| 66 | + |
| 67 | +Edge classes:: The four ways one groove party may reference another: |
| 68 | +`owns` (linear), `borrow` (affine), `observe` (unrestricted read), `peer` |
| 69 | +(unrestricted, symmetric). |
| 70 | + |
| 71 | +Residue:: Any state recoverable from a slot after its connection has been |
| 72 | +released. The cleave is sound iff residue descends to `⊥`. |
| 73 | + |
| 74 | +== 3. The ownership graph and edge classification |
| 75 | + |
| 76 | +A groove topology is a directed graph whose nodes are connection endpoints and |
| 77 | +whose edges are class-tagged. Edge classes map onto binding modes: |
| 78 | + |
| 79 | +[cols="1,1,3",options="header"] |
| 80 | +|=== |
| 81 | +| Edge | Binding | Meaning |
| 82 | + |
| 83 | +| `owns` | linear `let!` | The referent's lifetime is *subordinate*; the owner MUST release it exactly once. Only `owns` edges enter the residue proof. |
| 84 | +| `borrow` | affine `let` | A temporary, non-owning reference; MUST NOT outlive the referent; used at most once. |
| 85 | +| `observe` | unrestricted | Read-only visibility; conveys no lifetime obligation. |
| 86 | +| `peer` | unrestricted | Symmetric association between equals; neither owns the other. |
| 87 | +|=== |
| 88 | + |
| 89 | +Soundness of the whole cleave *reduces to correct classification*: if every edge |
| 90 | +that conveys a lifetime obligation is tagged `owns`, the measures below discharge |
| 91 | +all residue. |
| 92 | + |
| 93 | +== 4. Two well-founded measures |
| 94 | + |
| 95 | +Occupancy and discharge are **distinct** and both well-founded: |
| 96 | + |
| 97 | +* **Occupancy** decreases on connect and is renewed by heartbeat. A lease that |
| 98 | +lapses without renewal is reaped. This is the *liveness* half. |
| 99 | +* **Discharge** decreases on each release and is bounded below by `⊥`. This is |
| 100 | +the *teardown* half; `⊥` is the terminal, zero-residue state. |
| 101 | + |
| 102 | +Separating them prevents the classic error of proving termination of teardown |
| 103 | +while leaving a live connection able to squat indefinitely. |
| 104 | + |
| 105 | +== 5. Cycle-freedom |
| 106 | + |
| 107 | +Cycle-freedom follows from the well-foundedness of the **`owns` relation |
| 108 | +itself**, not from the termination measure. Because `owns` is well-founded, an |
| 109 | +ownership cycle (`a owns b`, `b owns a`) is unrepresentable. Consequently no |
| 110 | +reference-counting or tracing cycle-collector is required or admissible. |
| 111 | + |
| 112 | +== 6. Partial-order fidelity |
| 113 | + |
| 114 | +Teardown MUST honour the ownership partial order: **children before parents** |
| 115 | +(reverse-topological / postorder). LIFO stack discipline is only the degenerate |
| 116 | +case of a linear chain. For finite ownership trees the descent is witnessed by a |
| 117 | +Dershowitz–Manna multiset ordering, so **no ordinal is needed**. |
| 118 | + |
| 119 | +== 7. Ordinals |
| 120 | + |
| 121 | +Ordinal ranks are admitted *only* for a static-at-connect ranking over |
| 122 | +post-hoc-unbounded depth. Such a rank MUST be assigned at connect and MUST NOT |
| 123 | +increase thereafter. Ranks at or above `ε₀` are forbidden; the intended range is |
| 124 | +below `ω^ω` (finite-tree multisets in the common case). |
| 125 | + |
| 126 | +== 8. Joint completion and the scope boundary |
| 127 | + |
| 128 | +Teardown is a two-party act: |
| 129 | + |
| 130 | +* **Joint completion.** A clean disconnect completes only when *both* parties |
| 131 | +reach `⊥` and exchange acknowledgements. |
| 132 | +* **Scope boundary.** The cleave specifies *graceful* teardown only. On |
| 133 | +**rupture** (process death, connection drop, host crash, power loss) the |
| 134 | +**survivor owns the wipe**: the party that outlives the rupture reaps the shared |
| 135 | +resource; the dying party's cleanup is never depended upon. A lost acknowledgement |
| 136 | +resolves to rupture, never to an ambiguous half-state. |
| 137 | + |
| 138 | +[[invariants]] |
| 139 | +== 9. Normative invariants |
| 140 | + |
| 141 | +A conforming groove implementation MUST satisfy `RC-1`…`RC-13`. Each carries a |
| 142 | +*falsifier*: a concrete observation that would refute it. |
| 143 | + |
| 144 | +[cols="1,4,4",options="header"] |
| 145 | +|=== |
| 146 | +| ID | Invariant (MUST) | Falsifier |
| 147 | + |
| 148 | +| RC-1 | The `owns` relation is well-founded (acyclic). | A reachable cycle `a owns b … owns a`. |
| 149 | +| RC-2 | Every edge is classified as exactly one of owns/borrow/observe/peer. | An edge with no class, or two classes. |
| 150 | +| RC-3 | An `owns` capability is consumed exactly once (linear). | An `owns` edge released zero, or two-or-more, times. |
| 151 | +| RC-4 | A `borrow` is used at most once and never outlives its referent. | A borrow still reachable after its referent reached `⊥`. |
| 152 | +| RC-5 | Discharge strictly decreases per release and is bounded below by `⊥`. | A release that does not decrease discharge, or residue `> ⊥` after full teardown. |
| 153 | +| RC-6 | Occupancy is a renewable lease: down-on-connect, renewed by heartbeat, reaped on lapse. Hard grooves retain peer identity for reconnect; Soft grooves do not. | A lapsed lease not reaped, or a Soft groove retaining identity after disconnect. |
| 154 | +| RC-7 | After a clean two-party disconnect, residue = `⊥` for both parties. | Recoverable state after a graceful disconnect. |
| 155 | +| RC-8 | A Soft groove's peer identity is provably *erased* (not merely deactivated) on typed disconnect. | Peer identity recoverable from a freed Soft slot. |
| 156 | +| RC-9 | Teardown proceeds children-before-parent (reverse-topological). | A parent released while a child it owns is still live. |
| 157 | +| RC-10 | Any ordinal rank is fixed at connect, never increases, and is `< ε₀`. | A rank that increases post-connect, or `≥ ε₀`. |
| 158 | +| RC-11 | A two-party teardown completes only on mutual `⊥` + ack. | One party at `⊥` while the other holds state, with no rupture. |
| 159 | +| RC-12 | No `borrow`/`observe` edge references a party that has reached `⊥` (no dangling borrow). | A live borrow to a discharged owner. |
| 160 | +| RC-13 | Every teardown is exactly clean-XOR-rupture; a lost ack resolves to rupture. | A teardown that is neither cleanly completed nor rupture-handled (ambiguous on lost ack). |
| 161 | +|=== |
| 162 | + |
| 163 | +[[conformance]] |
| 164 | +== 10. Conformance and the vacuous-satisfaction caveat |
| 165 | + |
| 166 | +An implementation *conforms* iff it satisfies `RC-1`…`RC-13` and the `RC-N` |
| 167 | +table is wired into a machine checker (contractile / k9), so a regression is a |
| 168 | +red build. |
| 169 | + |
| 170 | +CAUTION: In the current reference implementation (`hyperpolymath/gossamer`) the |
| 171 | +groove layer is a **flat, target-id-indexed array with no `owns` graph**. The |
| 172 | +graph invariants (`RC-1`, `RC-9`, `RC-12`) are therefore satisfied *vacuously* — |
| 173 | +there is no ownership graph to violate. A green checker today is **not** a real |
| 174 | +guarantee; it becomes one when an actual `owns` graph exists. This note is |
| 175 | +retained deliberately so the distinction is not lost. |
| 176 | + |
| 177 | +== 11. Relationship to the reference implementation |
| 178 | + |
| 179 | +[cols="1,3",options="header"] |
| 180 | +|=== |
| 181 | +| Artifact (gossamer) | Role |
| 182 | + |
| 183 | +| `src/interface/abi/ResourceCleanup.idr` | Host of the residue→0 descent proof for the plain `disconnect` (RC-5, RC-7). NOTE: *not* `GrooveTermination.idr`, which is the connect-side bounded-length proof. |
| 184 | +| `src/interface/abi/GrooveResidue.idr` | Proves the Soft-groove typed-wipe leaves zero residue (RC-8), constructively. |
| 185 | +| `src/interface/abi/GrooveLinearity.idr` | The Active→Consumed linear discipline for a connection handle (RC-3). |
| 186 | +|=== |
| 187 | + |
| 188 | +`owns` is **linear** (`let!`), not affine — a common mis-statement. The residue |
| 189 | +proof consumes exactly the `owns` edges; `borrow`/`observe`/`peer` do not enter it. |
| 190 | + |
| 191 | +== 12. References |
| 192 | + |
| 193 | +* gossamer cleave-surface audit — `hyperpolymath/gossamer#82` (B-layer normative source; item 6). |
| 194 | +* `docs/proofs/spec-templates/T2-high/groove-browser-harness.md` (superseded harness template). |
| 195 | +* RFC 2119, RFC 8174 (requirement key words). |
| 196 | +* Dershowitz, Manna — _Proving termination with multiset orderings_ (CACM, 1979). |
0 commit comments