docs: Update P README and enforce consistent style

Author: the-mikedavis

p/README.md

@@ -4,7 +4,7 @@ A model of a correct-by-construction design for reclaiming a stream's remote-tie
 
 ## The design
 
-Before the very first fragment is written for a stream, the replica reader writes a dedicated anchor node in Khepri, kept alive by a keep_while condition on the queue, as a blocking step whose write commits strictly before the first S3 PUT. A sweep classifies a prefix as junk when objects are present and the anchor is absent. The keep_while removes the anchor in the same transaction that deletes the queue, so the "anchor absent" signal is produced atomically and is permanent: there is no record written at deletion time that a crash could lose.
+Before the very first fragment is written for a stream, the replica reader writes a dedicated anchor node in Khepri, kept alive by a `keep_while` condition on the queue, as a blocking step whose write commits strictly before the first S3 PUT. A sweep classifies a prefix as junk when objects are present and the anchor is absent. The `keep_while` removes the anchor in the same transaction that deletes the queue, so the "anchor absent" signal is produced atomically and is permanent: there is no record written at deletion time that a crash could lose.
 
 This is correct by construction off one ordering invariant. An object exists only after the anchor committed, and the anchor disappears only when the queue does, so there is no live state with objects but no anchor. Two properties fall out for free:
 
@@ -22,14 +22,14 @@ Each is proven necessary by a gate that must fail when the requirement is droppe
 | Consistent reads: the sweep reads the anchor with a strongly consistent (committed) read, not a stale local replica | a stale read reports the anchor absent for a stream whose anchor just committed while S3 already shows its first fragment, and the sweep reaps live data | `tcAnchorStaleReadReapsLive` (must fail) |
 | Ordering: the anchor commits before the first fragment PUT | a fragment exists before the anchor commits, so a sweep in that window reaps a live stream even with a consistent read | `tcAnchorOrderingViolated` (must fail) |
 
-The stale-read gate is the same shape as the `../gc-reset-multinode` stale-floor finding: a local replica cache that lags committed Khepri defeats an otherwise sound guard.
+The stale-read gate is the same shape as the `gc-reset-multinode` stale-floor finding: a local replica cache that lags committed Khepri defeats an otherwise sound guard.
 
 ## Tests
 
 | Test case | Expectation |
 | --- | --- |
 | `tcAnchorReclaimsAcrossCrash` | holds: consistent reads and anchor-before-fragment reclaim the junk even when a sweep crashes mid-reap, because the absence signal is permanent |
-| `tcAnchorExplore` | holds across nondeterministic replication timing and a crash mid-sweep |
+| `tcAnchorExplore` | holds: nondeterministic replication timing and a crash mid-sweep |
 | `tcAnchorStaleReadReapsLive` | fails with `INV NOREAPLIVE violated: GC reaped object ... while the stream's queue is still live` |
 | `tcAnchorOrderingViolated` | fails with the same counterexample, from the ordering violation |
 
@@ -45,4 +45,4 @@ p check -tc tcAnchorOrderingViolated    -i 2000   # 1 bug: fragment before ancho
 
 ## What the model does not cover
 
-The anchor's absence is a correct classifier but not a work-list. Finding the orphan prefixes still needs the deletion trigger for the prompt path (hung on the anchor node it fires for never-committed streams too) or a periodic S3-prefix scan as a backstop, which is now safe because the decision is by construction. Those provide discovery latency, not correctness.
+The anchor's absence is a correct classifier but not a work-list. Finding the orphan prefixes still needs the deletion trigger for the prompt path (hung on the anchor node, which it fires for never-committed streams too) or a periodic S3-prefix scan as a backstop, which is now safe because the decision is by construction. Those provide discovery latency, not correctness.

p/delete-stream-anchor/README.md

@@ -1,36 +1,36 @@
 # Integrated GC reap-decision
 
-A model of the whole rabbitmq_stream_s3_gc decision in one state space. The other GC models each prove a single guard in isolation and collapse the remaining axes into a constant: gc-reset proves still_dangling re-reads the live floor, gc-reset-multinode proves build_lookup gates on the cache epoch, gc-leading-group and gc-reset-leading-group prove the leading-group carve-out. This model composes all three classify reasons and all the guards together so they can interact, with two stores that lag independently and a sweep a reset can interleave into. The point is the interactions, not re-proving each guard.
+A model of the whole `rabbitmq_stream_s3_gc` decision in one state space. The other GC models each prove a single guard in isolation and collapse the remaining axes into a constant: `gc-reset` proves `still_dangling` re-reads the live floor, `gc-reset-multinode` proves `build_lookup` gates on the cache epoch, `gc-leading-group` and `gc-reset-leading-group` prove the leading-group carve-out. This model composes all three classify reasons and all the guards together so they can interact, with two stores that lag independently and a sweep a reset can interleave into. The point is the interactions, not re-proving each guard.
 
 ## The decision, as the code runs it
 
 The sweep is three phases, each reading a different store, mirrored from the module:
 
-1. build_lookup reads the committed epoch with a quorum read (db:get_consistent) and reads the floor and the leading-group carve-out from the local manifest_replica cache (get_manifest_and_epoch). It proceeds only when the cache epoch equals the committed epoch, and snapshots the committed epoch together with the cached floor and carve-out.
-2. classify flags an object against that snapshot: a data fragment below the snapshot floor, a group below the floor that is neither the referenced leading group nor in skip-groups mode, or a manifest below the committed epoch.
-3. still_dangling re-validates each candidate immediately before deleting it. A stale-epoch candidate is deleted with no re-check because the epoch is monotonic. A below-floor candidate re-reads the live cache: it compares the offset to the live floor (get_manifest) and re-derives the leading-group carve-out from the live manifest.
+1. `build_lookup` reads the committed epoch with a quorum read (`db:get_consistent`) and reads the floor and the leading-group carve-out from the local `manifest_replica` cache (`get_manifest_and_epoch`). It proceeds only when the cache epoch equals the committed epoch, and snapshots the committed epoch together with the cached floor and carve-out.
+2. `classify` flags an object against that snapshot: a data fragment below the snapshot floor, a group below the floor that is neither the referenced leading group nor in skip-groups mode, or a manifest below the committed epoch.
+3. `still_dangling` re-validates each candidate immediately before deleting it. A stale-epoch candidate is deleted with no re-check because the epoch is monotonic. A below-floor candidate re-reads the live cache: it compares the offset to the live floor (`get_manifest`) and re-derives the leading-group carve-out from the live manifest.
 
-The committed manifest truth is carried only by the authoritative referenced and unreferenced announcements, exactly as in gc-reset-multinode. The cache is the single materialized copy the sweep reads, and it may lag. A reap is a bug only when it deletes a currently referenced object.
+The committed manifest truth is carried only by the authoritative referenced and unreferenced announcements, exactly as in `gc-reset-multinode`. The cache is the single materialized copy the sweep reads, and it may lag. A reap is a bug only when it deletes a currently referenced object.
 
 ## The four guards
 
 Three are shipped. Each gate turns one off and reproduces a live deletion, so the model proves it load-bearing in the composed decision rather than in isolation.
 
 | Guard | Where | If removed | Gate |
 | --- | --- | --- | --- |
-| A epoch gate | build_lookup: skip unless cache epoch equals committed epoch | a node that has not applied a reset sweeps against a stale-high floor and the live re-read confirms it | `tcGcCrossNodeStaleUnguarded` |
-| B live-floor re-read | still_dangling: compare to the live floor, not the snapshot floor | a reset that lowers the floor between snapshot and execute lets the stale-high snapshot reap a re-tiered live fragment | `tcGcNoReread` |
-| C live carve-out | still_dangling: re-derive the leading group from the live manifest | a reset plus forward retention installs a new referenced leading group below the live floor that the stale snapshot carve-out deletes | `tcGcNoLeadingReread` |
+| A epoch gate | `build_lookup`: skip unless cache epoch equals committed epoch | a node that has not applied a reset sweeps against a stale-high floor and the live re-read confirms it | `tcGcCrossNodeStaleUnguarded` |
+| B live-floor re-read | `still_dangling`: compare to the live floor, not the snapshot floor | a reset that lowers the floor between snapshot and execute lets the stale-high snapshot reap a re-tiered live fragment | `tcGcNoReread` |
+| C live carve-out | `still_dangling`: re-derive the leading group from the live manifest | a reset plus forward retention installs a new referenced leading group below the live floor that the stale snapshot carve-out deletes | `tcGcNoLeadingReread` |
 
 The fourth guard is proposed, not shipped, and is the result the model exists to surface.
 
 ## The gap the integration surfaces
 
-With all three shipped guards on, the model still reaches a live deletion when a reset commits after the sweep has snapshotted. build_lookup samples the committed epoch once, at the start. still_dangling re-reads only the floor (get_manifest drops the epoch), so it never notices that the committed epoch has moved. On a node whose cache has not applied the reset sync, the sweep snapshots epoch N with a matching cache and an honest floor, a reset to N+1 then commits and re-tiers a live fragment below the old floor, and the live re-read returns the same stale-high floor. The epoch gate has already passed and the floor re-read defends nothing. The sweep deletes the re-tiered live fragment.
+With all three shipped guards on, the model still reaches a live deletion when a reset commits after the sweep has snapshotted. `build_lookup` samples the committed epoch once, at the start. `still_dangling` re-reads only the floor (`get_manifest` drops the epoch), so it never notices that the committed epoch has moved. On a node whose cache has not applied the reset sync, the sweep snapshots epoch N with a matching cache and an honest floor, a reset to N+1 then commits and re-tiers a live fragment below the old floor, and the live re-read returns the same stale-high floor. The epoch gate has already passed and the floor re-read defends nothing. The sweep deletes the re-tiered live fragment.
 
-gc-reset-multinode closed the mirror image of this, where the reset commits before the snapshot so get_consistent returns the new epoch and the gate skips. Its single scenario fixed the reset-before-snapshot ordering and did not exercise reset-after-snapshot. The dangerous path is the operator CLI full sweep (run/1 to build_lookup), which pins no writer epoch and relies on the consistent read and the cache-epoch gate, both sampled once.
+`gc-reset-multinode` closed the mirror image of this, where the reset commits before the snapshot so `get_consistent` returns the new epoch and the gate skips. Its single scenario fixed the reset-before-snapshot ordering and did not exercise reset-after-snapshot. The dangerous path is the operator CLI full sweep (`run/1` to `build_lookup`), which pins no writer epoch and relies on the consistent read and the cache-epoch gate, both sampled once.
 
-The proposed guard D re-validates freshness at the point of deletion: still_dangling re-reads the committed epoch and the cache epoch and fails closed when they differ. This requires still_dangling to use the epoch-aware read (get_manifest_and_epoch) plus a fresh get_consistent. Where that re-check lands in real code (per candidate, per list page, or once per stream before execute) is an implementation choice; the model proves only that the logical re-validation closes the window. With guard D on the model holds across the reset timing and sync delivery; with it off the shipped behavior reaps the live fragment.
+The proposed guard D re-validates freshness at the point of deletion: `still_dangling` re-reads the committed epoch and the cache epoch and fails closed when they differ. This requires `still_dangling` to use the epoch-aware read (`get_manifest_and_epoch`) plus a fresh `get_consistent`. Where that re-check lands in real code (per candidate, per list page, or once per stream before execute) is an implementation choice; the model proves only that the logical re-validation closes the window. With guard D on the model holds across the reset timing and sync delivery; with it off the shipped behavior reaps the live fragment.
 
 ## Tests
 
@@ -64,4 +64,4 @@ p check -tc tcGcCrossNodeStaleUnguarded   -i 2000   # 1 bug
 
 ## What the model does not cover
 
-The stale-epoch reap path deletes with no re-check, and its safety rests on epoch monotonicity, which is the subject of the writer-fencing model rather than this one. The model is one stream and one sweeping node, with the rest of the cluster represented by the committed-truth announcements and the lagging cache. The fail-closed-on-quorum-error path (a partitioned node that cannot reach a quorum) is covered by gc-reset-multinode and is not repeated here.
+The stale-epoch reap path deletes with no re-check, and its safety rests on epoch monotonicity, which is the subject of the `writer-fencing` model rather than this one. The model is one stream and one sweeping node, with the rest of the cluster represented by the committed-truth announcements and the lagging cache. The fail-closed-on-quorum-error path (a partitioned node that cannot reach a quorum) is covered by `gc-reset-multinode` and is not repeated here.

p/gc-decision/README.md

@@ -1,48 +1,32 @@
 # GC leading-group carve-out
 
-Models the second, independent live-deletion guard in `rabbitmq_stream_s3_gc`:
-`classify_group` and the `referenced_group_key` carve-out.
+Models the second, independent live-deletion guard in `rabbitmq_stream_s3_gc`: `classify_group` and the `referenced_group_key` carve-out.
 
-## The bug class
+## The bug
 
-A group object below `first_offset` is normally a dead orphan and is deleted by
-the offset heuristic. There is one exception: the *leading* group. On partial
-expiry retention advances `first_offset` *into* the leading group, so that group
-still sits below the floor yet remains referenced (its surviving fragments are at
-or above the floor). `leading_group_info/2` records that group's key as
-`referenced_group_key`, and `classify_group` skips it.
+A group object below `first_offset` is normally a dead orphan and is deleted by the offset heuristic. There is one exception, the leading group. On partial expiry retention advances `first_offset` into the leading group, so that group still sits below the floor yet remains referenced (its surviving fragments are at or above the floor). `leading_group_info/2` records that group's key as `referenced_group_key`, and `classify_group` skips it.
 
-Removing the carve-out (treating every group below the floor as a deletable
-orphan) deletes a live group - a dangling reference: a consumer reading the
-surviving offsets in that group can no longer fetch it.
+Removing the carve-out treats every group below the floor as a deletable orphan and deletes a live group, a dangling reference: a consumer reading the surviving offsets in that group can no longer fetch it.
 
-This is a *distinct* guard from `still_dangling/1` (the gc-reset model): that one
-re-validates an offset-based finding against the live floor after a reset; this
-one excludes the referenced leading group from offset-based classification in the
-first place. The flat-offset gc-reset model does not exercise it, so it lives
-here.
+This guard is distinct from `still_dangling/1` (the `gc-reset` model): that one re-validates an offset-based finding against the live floor after a reset, this one excludes the referenced leading group from offset-based classification in the first place. The flat-offset `gc-reset` model does not exercise it, so it lives here.
 
 ## What the model captures
 
-- Objects carry a `Kind` (`FRAGMENT` or `GROUP`); S3 holds genuine orphans below
-  the floor, the referenced leading group (also below the floor), and a live
-  fragment at the floor
+- Objects carry a `Kind` (`FRAGMENT` or `GROUP`); S3 holds genuine orphans below the floor, the referenced leading group (also below the floor), and a live fragment at the floor
 - The manifest records the referenced leading group key
 - `guardLeadingGroup` toggles the `classify_group` carve-out
 - `NoDanglingReference` (INV#2): GC never deletes a referenced object
 
-This is a classification-correctness property, not a concurrency race, so there
-is no exploration test.
+This is a classification-correctness property, not a concurrency race, so there is no exploration test.
 
-## Tests and the validation gate
+## Tests
 
 | Test case | Expectation |
 | --- | --- |
-| `tcLeadingGroupGuarded` | **holds** - the carve-out protects the leading group; also asserts the genuine orphans are reclaimed and the leading group preserved (anti-vacuity) |
-| `tcLeadingGroupUnguarded` | **fails** - carve-out removed; `INV#2 violated: GC deleted referenced object (offset=80, uid=2)` |
+| `tcLeadingGroupGuarded` | holds: the carve-out protects the leading group, and the genuine orphans are reclaimed with the leading group preserved (anti-vacuity) |
+| `tcLeadingGroupUnguarded` | fails: carve-out removed; `INV#2 violated: GC deleted referenced object (offset=80, uid=2)` |
 
-`tcLeadingGroupUnguarded` is *expected to fail*; that counterexample is the proof
-the model reproduces the live-group deletion.
+`tcLeadingGroupUnguarded` is expected to fail: that counterexample is the proof the model reproduces the live-group deletion.
 
 ```bash
 p compile