docs: record F11-1 closed — boundedness needs a resolved Client

Design v3.7 §6.1.1 gains the round-13 box (the rule, the ordering that is
load-bearing in both directions, and why bridging deliberately still uses the
full union); the phase-5 results file records the close with the measurement
the deferral was waiting for; the impl plan's phase-6 gate note drops F11-1.

pixelpass c78eb2d is the implementation.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
2026-07-26 04:46:25 -04:00
co-authored by Claude Opus 5
parent bf908adbf0
commit 692ad677d2
3 changed files with 62 additions and 20 deletions
@@ -472,9 +472,10 @@ observable in Phase 5 before they gate anything real.
> **The eligible half of row 1 is the only thing that exposed it** — the verdict was > **The eligible half of row 1 is the only thing that exposed it** — the verdict was
> fail-closed and silent. > fail-closed and silent.
> >
> ⚠️ **Phase 6 is NOT unblocked by this file alone.** F11-1 is a separate open gate (see §4's > ⚠️ **Phase 6 is NOT unblocked by this file alone.** F11-1 was the other gate and is now
> owner-union note and `owner_is_bounded`'s doc), as are phases 0b/0c/0d and the "Stereo Mix" > **closed** (2026-07-26, pixelpass `c78eb2d`: key 4 bounds an owner only when the node's
> design call. > Client resolves; measured cost on the live graph, zero — see the results file). Phases
> 0b/0c/0d and the "Stereo Mix" design call still precede phase 6.
> >
> Two things to keep when re-running: **every partition row must run with `AEC=off`** (a > Two things to keep when re-running: **every partition row must run with `AEC=off`** (a
> configured-but-unvalidated AEC shuts the fan-out gate and empties the eligible half of every > configured-but-unvalidated AEC shuts the fan-out gate and empties the eligible half of every
@@ -4,8 +4,8 @@
eligible half of every row is non-empty. O5 re-measured on the fixed graph and eligible half of every row is non-empty. O5 re-measured on the fixed graph and
stays closed.** One new defect was found and fixed during the run (F13-1); three stays closed.** One new defect was found and fixed during the run (F13-1); three
findings are recorded as non-blocking, and three rows carry recorded findings are recorded as non-blocking, and three rows carry recorded
substitutions. Phase 6 is unblocked **by this file**, but see "What still blocks substitutions. Phase 6 is unblocked **by this file**, and F11-1 — the other gate —
phase 6" — F11-1 is a separate gate and is still open. was closed with this data on 2026-07-26 (see "What still blocks phase 6").
- **Run date:** 2026-07-26 (run 1: 2026-07-25, gate FAILED — see history below) - **Run date:** 2026-07-26 (run 1: 2026-07-25, gate FAILED — see history below)
- **Host:** `cazen` — PipeWire 1.6.8, WirePlumber 0.5.15, CachyOS - **Host:** `cazen` — PipeWire 1.6.8, WirePlumber 0.5.15, CachyOS
@@ -332,24 +332,41 @@ lesson: the row could not have been asserted from any previous build's output.
## What still blocks phase 6 ## What still blocks phase 6
This file passing removes **one** of the two gates. Still outstanding: This file passing removes **one** of the two gates. F11-1, the other, is now
closed. Still outstanding:
1. **🔴 F11-1 — the owner-key union can *reduce* taint.** Unchanged and still 1. **Hardware playback-to-capture paths ("Stereo Mix")** defeat `session_device`
open; it was to be decided *with* this matrix data. The data now exists: the
suppression path is live and correct (F13-1 fixed), and rows 2/9 show key 4
doing real work, which means the interaction F11-1 describes is reachable in
principle. The rule to implement is written in `owner_is_bounded`'s doc in
pixelpass `src/host/taint/owner.rs`, sharpened by Codex round 12: "resolved"
must mean **an unambiguous Client yielding `Some(pipewire.sec.pid)` before
pipewire-pulse suppression**. A five-case Client matrix (absent · ambiguous ·
unique-but-pid-less · resolved-native · resolved-to-pipewire-pulse) is owed.
2. **Hardware playback-to-capture paths ("Stereo Mix")** defeat `session_device`
and are a real echo path — needs ALSA control inspection; user design call owed. and are a real echo path — needs ALSA control inspection; user design call owed.
3. **Phases 0b / 0c / 0d** are untouched and all precede phase 6. 2. **Phases 0b / 0c / 0d** are untouched and all precede phase 6.
4. **The readiness budget calibration argument** (above). 3. **The readiness budget calibration argument** (above).
5. **Owed samples:** a real third-party forwarder (row 1b), EasyEffects (row 8), 4. **Owed samples:** a real third-party forwarder (row 1b), EasyEffects (row 8),
a real `Audio/Duplex` device (row 13). a real `Audio/Duplex` device (row 13).
### ✅ F11-1 — closed 2026-07-26, with this matrix's data
The rule now implemented (pixelpass `c78eb2d`, §6.1.2's round-13 box): **key 4 bounds an
owner only when the node's Client resolves** — an unambiguous Client yielding
`Some(pipewire.sec.pid)`, read *before* pipewire-pulse suppression — so a node can no
longer bound itself, and escape `propagate_unresolved_owner`'s sweep, with an
`application.process.id` it invented. Bridging still uses the full union.
Codex's round-12 sharpening was the decisive part: "resolved" must mean a `sec_pid`, not
"a unique Client object exists", and the **unique-but-pid-less** row is the only one that
tells the two apart. All five Client cases are unit tests (absent · ambiguous ·
unique-but-pid-less · resolved-native · resolved-to-pipewire-pulse), plus the recorded
three-step leak path end to end. Mutation-verified: dropping the provenance test fails
four of the six rows and leaves the two no-over-exclusion rows green.
**The cost question the deferral was waiting on, measured on this host:** the before- and
after-binaries audited the *same* live graph simultaneously (both are read-only observers)
— tagged producer into the default sink, `parec` on its monitor as a live tainted reader
so the sweep was genuinely armed, Firefox + `aplay` + `pacat` as bystanders. **181 records
each, the same 14 distinct decision states, none exclusive to either side, no
`unresolved-owner` on either, eligible half non-empty throughout.** O5 unmoved (identical
p50 15 µs and busy fraction 0.0012). Every real app here is native or Pulse-emulated and
**both resolve**; sweeping all 18 live nodes, the only unresolved-Client ones were
`Dummy-Driver` and `Freewheel-Driver`, which carry no pid key to lose.
--- ---
## Reproducing this run ## Reproducing this run
+25 -1
View File
@@ -581,6 +581,30 @@ Where an owner has a tainted input leg and an output leg with **no** resolvable
(§6.1.2), fail closed and exclude the output leg. This only ever engages for owners (§6.1.2), fail closed and exclude the output leg. This only ever engages for owners
actually reading a tainted monitor, so the blast radius is small. actually reading a tainted monitor, so the blast radius is small.
> **⚠️ Round 13 (F11-1) — "bounded" is not "has a key". A self-claimed pid is not
> provenance.** Which legs this backstop sweeps depends on whether the tainted reader and
> the candidate outputs are *bounded* — i.e. whether we could enumerate their sibling legs
> and be right. Key 4 is a union of the node's `application.process.id` (client-controlled,
> optional) and its Client's `pipewire.sec.pid` (protected), so a node could bound itself
> with a value it invented and escape the sweep while its real sibling was unfindable.
>
> **Rule:** a strong key (`node.link-group`, `pulse.module.id`) bounds an owner on its own;
> key 4 bounds an owner **only when the node's Client resolves** — an unambiguous Client
> yielding `Some(pipewire.sec.pid)`, read *before* pipewire-pulse suppression. The
> ordering is load-bearing in both directions: read after suppression and every
> Pulse-emulated app on the box goes unbounded (§6.1.1 catastrophe, new door); accept "a
> unique Client object exists" instead of a `sec_pid` and a pid-less Client leaves the hole
> open.
>
> **Bridging is unchanged** — it still uses the full union, because a self-claimed pid is
> perfectly good *evidence that two legs are related*, which is the taint-increasing
> direction. Only the permission to declare a differently-keyed output "provably someone
> else" now demands a `pipewire.*` answer to "who is this".
>
> Measured cost on this host: **zero** — before/after binaries audited the same live graph
> simultaneously, same 14 decision states, no `unresolved-owner` on either side, eligible
> half non-empty. Implemented in pixelpass `c78eb2d`; five-case Client matrix in the tests.
### 6.1.3 ⚠️ Taint must be STICKY — current topology is not enough ### 6.1.3 ⚠️ Taint must be STICKY — current topology is not enough
**Conceded to Codex in round 6; my "conditional bridge" was correct about topology and **Conceded to Codex in round 6; my "conditional bridge" was correct about topology and
@@ -1198,7 +1222,7 @@ requirement to assert what must remain **eligible**: §6.1.2's pulse-PID derivat
| §5.1 matrix | **PASSED** — 13/13, incl. the full sticky lifecycle (row 10) and provable identifier recycling (row 11) | | §5.1 matrix | **PASSED** — 13/13, incl. the full sticky lifecycle (row 10) and provable identifier recycling (row 11) |
| O5 | **closed on the real graph** — worst recompute 67 µs, churn mean 10 µs, busy fraction 0.0006 | | O5 | **closed on the real graph** — worst recompute 67 µs, churn mean 10 µs, busy fraction 0.0006 |
| Phase 5 | **machinery unchanged and correct** — three real defects caught on first contact with the live graph, none of them in the engine | | Phase 5 | **machinery unchanged and correct** — three real defects caught on first contact with the live graph, none of them in the engine |
| Phase 6 | **still blocked** — by F11-1, phases 0b/0c/0d, and the "Stereo Mix" design call, *not* by this matrix | | Phase 6 | **still blocked** — by F11-1, phases 0b/0c/0d, and the "Stereo Mix" design call, *not* by this matrix. (F11-1 was **closed later the same day** with this matrix's data — §6.1.2's round-13 box; the rest stand.) |
Three rows passed with recorded substitutions (8 EasyEffects, 9 Firefox's own mic/monitor Three rows passed with recorded substitutions (8 EasyEffects, 9 Firefox's own mic/monitor
paths, 13 a real `Audio/Duplex` device) and the third-party samples stay owed. paths, 13 a real `Audio/Duplex` device) and the third-party samples stay owed.