Commit 7497943
groove: adopt the Ranked-Ownership Cleave spec (B2 cleave) — standard… (#552)
…s#386
Canonical normative spec for groove teardown: the discipline by which a
groove connection closes cleanly and provably leaves zero residue (⊥).
Covers the B2 (live-governance / lifecycle-residue) layer only.
- groove-protocol/spec/GROOVE-RANKED-OWNERSHIP-CLEAVE-SPEC.adoc —
v0.2.0-draft.1: two well-founded measures (occupancy = renewable lease;
discharge = residue→⊥), cycle-freedom from well-foundedness of `owns`,
edge classification (owns=linear / borrow=affine /
observe|peer=unrestricted), partial-order fidelity
(children-before-parent; Dershowitz–Manna multiset), ordinals only
static-at-connect (ε₀+ forbidden), joint completion +
survivor-owns-the-wipe rupture policy, and 13 normative invariants
RC-1…RC-13 each with a falsifier.
- groove-protocol/README.adoc — cleave-surface layering (A/B1/B2/C1/C2)
+ index.
- Pointer from the superseded groove-browser-harness template.
Provenance corrections folded in (verified against the gossamer tree):
host proof is ResourceCleanup.idr (not GrooveTermination.idr); `owns` is
linear not affine; the graph invariants are VACUOUSLY satisfied today
(flat groove array, no owns graph) — a green checker is not yet a real
guarantee. Addresses gossamer#82 item 6.
<!--
SPDX-License-Identifier: CC-BY-SA-4.0
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-->
## Summary
<!-- What does this PR do, and why? -->
Closes #
## Type of change
- [ ] 🐛 Bug fix (non-breaking change that fixes an issue)
- [ ] ✨ New feature (non-breaking change that adds functionality)
- [ ] 💥 Breaking change (would change existing behaviour)
- [ ] 🕳️ Soundness fix (fixes a checker/proof false-negative)
- [ ] 📖 Documentation
- [ ] 🧹 Refactor / tech debt (behaviour-preserving)
- [ ] ⚡ Performance
- [ ] 🔧 Build / CI / tooling
## How has this been verified?
<!-- Establish ground truth: which tool did you RUN, and what did it
report?
Don't cite a status doc — cite the command and its output. -->
## Checklist
- [ ] My commits are **signed** (`git commit -S`).
- [ ] I ran the project's own checks/tests locally and they pass.
- [ ] New files carry the correct `SPDX-License-Identifier` (code/config
`MPL-2.0`,
prose `CC-BY-SA-4.0`); I did not relicense existing files.
- [ ] Docs are updated, and no public claim now overstates what the code
does.
- [ ] I have not introduced a soundness hole (or I have flagged where I
might have).
## Notes for reviewers
<!-- Anything that needs special attention, follow-up, or context. -->
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>1 parent 9620f97 commit 7497943
0 file changed
0 commit comments