docs(827): Gate0 Probe-3 Class-B §3-review v3 PASS @ace60667
Independent Opus §3-conformance review (Gate-16 author≠reviewer).
Reviewed object = ace6066762
harness sha256 = 2f11c9391c0eef203f26b1206bee8bc4cd106e8c1192399c5e7b71f41a3f6b75
Verdict PASS: (a) live-path gated launcher, (b) fail-closed precondition,
(c) fixture-socket isolation, (d) lease_anchor_registered assertion intact.
Byte review only; ran nothing. FIRE remains separately gated on Mos GO.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -0,0 +1,65 @@
|
|||||||
|
# Gate0 Probe-3 (D4) Class-B — §3-Conformance Review v3
|
||||||
|
|
||||||
|
**Verdict: ✅ PASS**
|
||||||
|
|
||||||
|
## Pin (G1 — reviewed object, mandatory)
|
||||||
|
|
||||||
|
- **Reviewed object = `ace6066762c088f4b9729860da71b4c84451a7c3`** (harness commit, branch `feat/827-gate0-probe`, `mosaicstack/stack` @ git.mosaicstack.dev).
|
||||||
|
- **Reviewed file:** `docs/compaction-refresh/probes/p3_d4_focused_run.py`
|
||||||
|
- **Harness sha256 (pushed provider bytes, fetched `-o FILE`, FULL-40 ref, verified before trust):**
|
||||||
|
`2f11c9391c0eef203f26b1206bee8bc4cd106e8c1192399c5e7b71f41a3f6b75` (17162 bytes; no not-found sentinel).
|
||||||
|
- **§3 amendment authority read at pin:** `GATE0-PROBE3-EXEC-AMENDMENT.md` @ ref `571f239154c6793fb1a5eac0d1cd4182f286a3ac`,
|
||||||
|
sha256 `9ac9ff873fad41a6e15763cc89cb94d0bc4a6b0cf9b6770561d1781b03f63276` (7699 bytes). MUST-HAVE/MUST-BE-ABSENT
|
||||||
|
confirmed against the actual fetched §3 text, not a paraphrase.
|
||||||
|
|
||||||
|
## Independence (G2)
|
||||||
|
|
||||||
|
Distinct Opus §3-conformance reviewer (Gate-16 author≠reviewer). I did **not** build this harness (author =
|
||||||
|
ms-rev-826); I am not Mos. This verdict is my own; the author did not author or edit it. Byte review only — **ran
|
||||||
|
nothing** (no harness, no broker, no sockets/state). Reviewed across v1 (FAIL, live-broker launch path) → v2 (PASS,
|
||||||
|
later found runtime-dead producer) → this v3 (closes the live-path review-gap).
|
||||||
|
|
||||||
|
## Why v3 (the review-gap closed)
|
||||||
|
|
||||||
|
v2 PASS @`839d156f` credited the static presence of `lease_anchor_registered` as isolation proof. At FIRE the
|
||||||
|
producing path was **dead**: the harness drove the *released* `mosaic` binary, which launched Pi **ungated**, so
|
||||||
|
`register_anchor` never ran. Static presence of an assertion ≠ its producing path executing. v3 requires the
|
||||||
|
producing path to be **live at runtime**.
|
||||||
|
|
||||||
|
## Surface-by-surface
|
||||||
|
|
||||||
|
| Surface | Result | Evidence (file:line) |
|
||||||
|
|---|---|---|
|
||||||
|
| Pushed bytes fetched + sha-verified | ✅ | sha256==`2f11c939…`, 17162B, no sentinel |
|
||||||
|
| (a) LIVE-PATH — drives the **gated** launcher, producer in the exec chain, NOT released `mosaic`/plain `execRuntime` | ✅ | launch = `python3 <GATED_LAUNCHER> --runtime pi -- pi …` :357-364; `GATED_LAUNCHER=…/launch-runtime.py` :32, pinned `GATED_WI_HEAD=abd2791f…` :31; `mosaic yolo`/`execRuntime` = 0 hits. `launch-runtime.py` unconditionally `register_anchor`s before `execvpe`, so the producer is in the invoked chain |
|
||||||
|
| (b) Fail-closed precondition present + correct (gated + fixture-socket, refuses otherwise), invoked before all launches | ✅ | `gated_launcher_precondition` :229-251, called :342 **before** broker Popen :343 and Pi launch :357. Verifies (ii) `MOSAIC_LEASE_BROKER_SOCKET==fixture` :232 + fixture in tempdir :234; (i) launcher HEAD==`abd2791f` :243 + source has `register_anchor` **before** `execute(command[0]…)` and reads `MOSAIC_LEASE_BROKER_SOCKET` :246-250. Raises `RuntimeError` (no run) on any miss :233/:235/:242/:244/:250 |
|
||||||
|
| (c) Fixture-socket isolation (no live/default broker reachable, single p3 fixture, non-destructive) | ✅ | `pop("MOSAIC_LEASE_BROKER_SOCKET")` :330 + set to fixture socket :334; harness invokes `launch-runtime.py` directly so it reads `MOSAIC_LEASE_BROKER_SOCKET`=fixture with **no** `defaultLeaseBrokerSocket`/XDG/`/run/user` fallback in the path; `register_anchor` served by the single p3 fixture; `p3_generation_broker.py` **zero diff** vs `839d156f` (in-memory volatile hex-256 session `secrets.token_hex(32)`, nothing durable outside tempdir) |
|
||||||
|
| (d) Assertion INTACT (`lease_anchor_registered` + `session_id_shape=="hex-256"`, not softened/optional/repointed) | ✅ | :256-258 (event), :298 (`hex-256`), folded into single-PID/starttime identity set :286. Not Case C |
|
||||||
|
| spawns ONLY p3_generation_broker.py | ✅ | broker Popen = `HERE/p3_generation_broker.py` :343-346; the pinned launcher is a register-before-exec launch wrapper, not a 2nd broker |
|
||||||
|
| promotion = fixture-only (not P2-banked) | ✅ | `d4_fixture_promote` "not a P2 evidence-gathering authorization"; `promote-probe` in-memory; precondition target only; no P2 import |
|
||||||
|
| D4 assertions complete | ✅ | same-PID+starttime persist (incl. launcher registration) :284-288; gen strictly increases :290-293; reload revokes genuinely-VERIFIED prior :299-300; new→`MUTATOR_UNVERIFIED` :301; prior→`STALE_GENERATION` :302; lifecycle boundaries :294-297 |
|
||||||
|
| P5 / P6 / P2-bank / retry-launder / live-effect / mechanism-change / scope-widen ABSENT | ✅ | 0 hits: `source-invalid`/`run_open`/`atomic`/`p2_provider`/`p5`/`p6`/`pi_gate0_run`/`retry`; no real-broker path; the only mechanism change is the required launch-routing fix (release→pinned gated launcher), which narrows scope, not widens |
|
||||||
|
| non-destructive | ✅ | per-run `tempfile.mkdtemp` fixtures; p3 in-memory + tempdir socket/log only; reads `/proc/<pid>/stat` (read-only) |
|
||||||
|
| deterministic | ✅ | isolated tempdir per run; deterministic assertions; session-id randomness is **shape**-asserted only (`hex-256`), `setdefault` idempotent |
|
||||||
|
| hidden exec-at-import | ✅ absent | only `if __name__ == "__main__": main()`; docstring: not executed until FIRE |
|
||||||
|
|
||||||
|
## Verdict
|
||||||
|
|
||||||
|
**PASS @ `ace60667`** — (a) LIVE-PATH, (b) fail-closed precondition, (c) fixture-socket isolation, and
|
||||||
|
(d) intact assertion all hold, with zero out-of-scope surface. The v2 review-gap (runtime-dead producer via the
|
||||||
|
released ungated `mosaic`) is structurally closed: the harness no longer invokes `mosaic` at all — it invokes the
|
||||||
|
pinned `abd2791f` `launch-runtime.py` directly (register-before-exec), and refuses to launch unless the launcher is
|
||||||
|
that pinned gated register-before-exec binary bound to this run's fixture socket.
|
||||||
|
|
||||||
|
**Findings: none.**
|
||||||
|
|
||||||
|
## Scope reminder (not a finding)
|
||||||
|
|
||||||
|
Per §3/§5 of the amendment, producing this evidence **executes** the Gate0 mechanism (launches processes, creates
|
||||||
|
socket/state artifacts, exercises revocation). This review clears the **bytes**; **FIRE remains separately gated on
|
||||||
|
Mos's explicit post-clear GO** and is not authorized by this review.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
**Reviewer:** independent Opus §3-conformance reviewer (Gate-16 author≠reviewer). Byte review only; ran nothing.
|
||||||
|
**Reviewed object (pin):** `ace6066762c088f4b9729860da71b4c84451a7c3` · harness sha256 `2f11c9391c0eef203f26b1206bee8bc4cd106e8c1192399c5e7b71f41a3f6b75`.
|
||||||
Reference in New Issue
Block a user