feat(#830): revoke leases across compaction lifecycle

docs/scratchpads/830-compaction-revoke.md

@@ -47,3 +47,37 @@ Working estimate: **35K tokens**. No explicit hard cap was supplied; reduce refa
 - Preserve revoke-first/promote-last and WI-1/WI-2 reviewed state machine.
 - ≥85% attributable executable coverage with real tests.
 - No author self-review, no merge, no `--no-verify`.
+
+## Local implementation complete (push held)
+
+Implemented on the WI-3 base `abd2791f59b3f06f46dd08e55298ced72f6aa7c2` without changing the reviewed broker state machine:
+
+- Added `revoke-lease.py`, which authenticates through the existing broker session/generation and invokes `revoke_lease`. A fired observer that cannot confirm broker revocation advances the private generation as a local fence before returning non-zero.
+- Added `lease_generation.py`: owner/type/mode/size validation, no-follow opens, exclusive bump lock, monotonic `int64` generation, write-all + `fsync`, and fail-closed exhaustion/corruption handling.
+- `launch-runtime.py` creates `generation-<broker-session>.state` mode `0600` beside the socket before `exec`; `mutator-gate.py` resolves that current file value on every tool check.
+- Claude settings and isolated Claudex settings now preserve/install `PreCompact`, `SessionStart(compact)`, and resume/clear rollover hooks in addition to the global all-tools gate.
+- Pi now registers tested `session_before_compact`, `session_compact`→first `context`, and `session_start(reload|new|resume|fork)` handlers. Failed pre-compact revocation cancels compaction; failed post-compact/rollover revocation latches local all-tool denial.
+- Added PRD requirements, architecture/security/protocol/operations updates, sitemap entry, and the ignored-by-default documentation checklist (force-add required at commit).
+
+### Acceptance and coverage evidence
+
+- Focused acceptance: `19/19`; T12b/T30 prints within-TTL **ALLOWED** and after-TTL **DENIED**.
+- Pi lifecycle: `8/8`, with **100% statements/branches/functions/lines** attributable coverage.
+- New Python generation/revoker: `24/24`, **99% branch-aware aggregate coverage** (`lease_generation.py` 98%, `revoke-lease.py` 100%).
+- Mosaic package: `1399/1399`; framework shell Python `24/24`, launch guard `12/12`, permanent launch inventory `14 gated/14 total`.
+- Existing lease-broker real-socket acceptance: `37/37` within the package run.
+- Full repository: `43/43` Turbo tasks green; gateway `628 passed / 12 skipped`; Mosaic `1399/1399`.
+- Root typecheck: `42/42`; lint: `23/23`; format and `git diff --check` green.
+- Initial direct package test without first building the package reproduced the known missing-`dist/cli.js` harness condition; the canonical root Turbo test (which schedules `@mosaicstack/mosaic#build`) and explicit package build+test are green. No test was weakened.
+
+### Review evidence
+
+- Codex uncommitted code review: **APPROVE**, confidence `0.88`, zero findings. Its read-only sandbox could not rerun Vitest, but the author-side focused and full suites above were green.
+- Codex uncommitted security review: risk **none**, confidence `0.91`, zero findings.
+- Coordinator-mandated fresh exact-head terra CODE and Opus SECREV remain pending after rebase/push clearance; these local reviews do not replace that final gate.
+
+### Hold and residuals
+
+- **DO NOT PUSH OR OPEN A PR YET.** Coordinator requires flake-fix #838 to land, then WI-3 must rebase onto deterministic-green `main` before push.
+- Merge remains gated on #838, #827 Probe 3, and combined GO.
+- Named residual retained verbatim: when both observers are entirely missed, within-TTL consequential actions remain allowed; only lease expiry denies after the bounded stale window. No within-window mutator-action bound is claimed.