integrations/fleet-proof/REASON-COVERAGE.md

Proof reason coverage

Linux adds unsupported_pid_namespace to the fixed terminal and native reason vocabularies. A real private-PID-namespace container emits this refusal before process or socket observation. The manual host-only Linux fixture exercises real TCP cookies, shared descriptors (including private per-thread tables), unreadable same-user processes, pinned births, ancestry exits and serial transport. The portable vocabulary check compares the protocol with both production helper sources. Linux evidence and its initial-PID-namespace limits are recorded in VUH-2118 verification.

fleet-health-metrics-native.integration.test.ts runs the real macOS helper, live loopback TCP sockets, an isolated Herdr daemon and a service-owned private registry. It asserts fourteen existing terminal refusal cases independently of native retry diagnostics: eighteen attempts, sixteen refusals and two admissions. It also checks a real provider method refusal and an actual reply corrupted by an owned Unix relay. No kernel observations or successful provider responses are fabricated.

Terminal reason	Exercised boundary
`unsupported_platform`	Host platform configuration refuses a live socket.
`invalid_pane`	An invalid caller pane claim on a live socket.
`closed_socket`	The owned TCP peer is closed; project coverage also closes it after a real native observation.
`missing_binding`	The service supplies no current Herdr binding.
`native_initial_unavailable`	The compiled helper is unavailable at the initial checkpoint.
`native_final_unavailable`	The real initial observation succeeds, then the final helper is unavailable.
`pane_unavailable`	Real Herdr returns `pane_not_found` on the initial pane read.
`pane_moved`	The claimed ID belongs to a pane moved to another workspace; real Herdr answers for it under its new ID.
`not_member`	Neither the actual ancestry nor the service registry grants membership.
`snapshot_changed`	The TCP owner's actual parent exits between observations.
`pane_changed`	The owned pane is removed between the initial and final Herdr reads.
`private_seat_expired`	The service revokes its actual private registry entry between checks.
`binding_changed`	The service changes its Herdr binding between checks.
`observation_failed`	The real Herdr control socket is unavailable, rejects an unknown method, or returns a reply corrupted in transit.

Only Herdr's fixed pane_not_found code is preserved by the native control transport. Other provider errors, invalid JSON, incorrect reply IDs and transport failures remain generic failures. An initial missing pane maps to pane_unavailable; a missing final pane maps to pane_changed. Both refuse admission. A project socket that closes during asynchronous observation maps to closed_socket, separately from changes in binding or native observations.

native-ancestry-exit.integration.test.ts adds real scheduled claimant and intermediate exits: caller_exited is terminal and never replayed; ancestor_exited permits one re-walk only with the same live claimant. A second intermediate exit is terminal. The fixture controls owned exit timing while returning only real libproc/sysctl/socket observations. It also checks stale PID/birth/socket pins and HTTP non-member refusal after real reparenting. PID/birth facts remain private; public metrics retain the fixed reasons.

Native diagnostic evidence

The manual native churn test asserts real multiple_owners, owner_mismatch, socket_mismatch, invalid_arguments and owner_not_found counters. It uses a second real PID sharing the connected FD, an invalid server-owned lifetime/socket pin, and a previously owned TCP pair after both endpoints close.

The project HTTP integration uses real execv with a 4097-byte argv[0]. The kernel permits the exec, but the helper's bounded argument observation emits argv_invalid; the project request refuses with HTTP 403 and no forwarded effect. Project process diagnostics are passed through the same schema and collector as socket diagnostics; diagnostic hooks do not affect admission.

The redacted fixture exhausted-diagnostics.json retains actual budget_exhausted and attempts_exhausted events from independent FD-churn runs on unchanged commit 8fcf47a54b578629386bdbc306db3ae2205d57f4. Both original requests returned HTTP 403 with zero forwarded effects. Their source run names, checkpoint, attempt and fixed event fields are retained; variable PIDs, ports, paths and other request data are omitted. Those same runs also observed socket_unavailable, process_unavailable and process_census_changed. The captures prove these OS branches occurred; a golden replay does not claim to force their occurrence on every machine.

fleet-health-metrics.integration.test.ts derives the complete fixed native vocabulary from the helper's diagnostic declarations, compares it to the protocol enum, and checks every token through the collector and authenticated HTTP schema. It also counts the captured exhaustion events and rejects an unknown diagnostic reason. These vocabulary samples are contract inputs, not claims that the OS produced every possible failure. Native diagnostics never add terminal proof attempts or inflate the refusal denominator.

Additional defensive OS evidence

The four-producer evidence and the seven-producer evidence (manual fleet-additional-os-native.integration.test.ts) establish eleven of the sixteen formerly unmet reasons. Those owned workloads cover ancestry_bounds, process_census_unavailable, fd_list_unavailable, argv_unavailable, executable_unavailable, fd_list_bounds, executable_changed, argv_changed, process_changed, ancestry_unavailable and ancestry_changed. These direct helper observations are distinct from full HTTP admission proofs and do not claim a deployed check. Since VUH-2070 that oversized owner's table is read whole: the same manual test now proves the non-refusing fd_list_large diagnostic, and the opt-in native-proof-churn.integration.test.ts proves an unrelated oversized table neither refuses a caller nor hides a second holder of its socket.

fleet-final-os-native.integration.test.ts adds a real clock_unavailable producer. The unchanged helper runs under a policy denying only its libc retry wait syscalls, on actual owned TCP sockets with bounded process churn. A native baseline verifies that the monotonic clock remains available while the wait is denied. The helper refuses after its real retry wait fails. Its actual fixed reason reaches the production schema, aggregate counter and five/sixty-minute windows without adding terminal proof attempts. See the actual capture and limitations. The same file proves ancestry_cycle from an owned child debugger tracing its parent, with actual reciprocal kernel PPIDs. A stable untraced supervisor reaps the original target after detach/continue; ordinary high-level exit waits during reparenting do not prove exit. Only owned debug-signed fixture processes are addressed. The production helper and its kernel observations are not replaced. Pure final-check budget expiration still reports budget_exhausted without inventing a socket mismatch.

Explicit OS coverage limits

fleet-allocation-native.integration.test.ts now proves allocation_failed with the original stock Intel allocator and production proof implementation on a real owned TCP pair. An unconstrained baseline admits; bounded, untouched PROT_NONE address-space reservations make the FD buffer allocation return ENOMEM. Its actual diagnostic reaches the schema, collector and both windows. This manual-only case requires an executable x86_64 macOS slice (Rosetta on Apple Silicon); it does not claim an ARM reproduction. See the producer evidence. The lead's revised acceptance classifies fd_record_invalid and socket_identity_invalid as defensive, not producible through supported APIs on the reviewed ABI. The same manual test compiles the production guard and diagnostic implementations directly, checks negative/valid FD records and each missing/complete Unix/TCP identity field, then checks the production schema, collector and both windows. These explicitly supplied direct guard inputs are not records claimed to come from the OS. The kernel/ABI review and direct tests satisfy the revised guard acceptance; vocabulary/schema inputs alone do not. Actual failed candidate probes and the pinned Apple API review are distinguished from successful native diagnostics.

Supported FD operations have not supplied negative descriptor records, and no supported per-process operation was found that zeros a matched socket's opaque identity. These fail-closed guards stay intact. Published debugger attach paths can alter process parentage, so a blanket assertion that kernel observations cannot be cyclic is not sufficient evidence. The successful owned debugger workload above proves cyclic parentage on this host; its earlier denied attach did not. Allocation-limit setup failures and loader exits before the helper's allocation are likewise not allocation_failed events. No existing fleet process, host-wide policy or proof response is changed to manufacture a diagnostic.

Worker receipt failures

fleet-report-reasons.integration.test.ts exercises the production installed sender against real loopback HTTP, the durable conversation store and inbound receipt fence, and real local files. Every fixed failure reason reaches the collector, authenticated HTTP schema and CLI five/sixty-minute windows:

Reason	Actual failure boundary
`binding_timeout`	The owned binding endpoint holds its response past the request deadline.
`binding_unavailable`	The binding endpoint returns HTTP 503.
`binding_rejected`	The binding endpoint denies the request with HTTP 403.
`receipt_timeout`	The original POST response exceeds its deadline; the local claim remains.
`receipt_invalid`	The service stores the original, then its reply fingerprint is corrupted. Exact GET reconciliation later settles it.
`receipt_unresolved`	The POST returns HTTP 503; the real listener is then closed before refreshed-bridge GET reconciliation.
`connection_refused`	The real listener closes after binding and before POST dispatch.
`local_receipt_unavailable`	A real file occupies the required claim-directory path.

The stored control verifies durable receipt evidence and removes only its exact claim. Retained originals are reconciled by GET without another POST. Repeated polls of the same health observation do not add attempts. Snapshots contain only fixed counters, never report bodies, binding fingerprints, paths or process data. This proves receipt transport and counter boundaries, not native OS diagnostics.

The proof-alert integration in fleet-lead-round.integration.test.ts uses real TCP refusals and durable native outbox receipts with a captured census boundary. It proves threshold → notifyFleetHealthAlert → exact head acknowledgment, and that unavailable delivery does not consume the accepted-alert cooldown. Native owner TUI acceptance remains a separate live proof; this fixture does not claim that an original operator TUI received the alert.

Focused checks

pnpm fleet-proof:build
FLEET_PROOF_NATIVE_TEST=1 PROJECT_NATIVE_PROOF_TEST=1 pnpm exec vitest run --config vitest.config.ts \
  apps/clankie/test/fleet-health-metrics-native.integration.test.ts \
  apps/clankie/test/native-proof-churn.integration.test.ts \
  apps/clankie/test/project-native-proof.integration.test.ts \
  apps/clankie/test/fleet-health-metrics.integration.test.ts

Native cases are manual opt-ins. They add no build, subprocess churn or Herdr daemon to per-push CI. The vocabulary/HTTP contract uses no native build and remains a fast portable integration check.

Run the additional manual cases under the fleet's heavy wrapper with FLEET_ADDITIONAL_OS_TEST=1; build the production helper first. The owning fixtures' lifetime and reproduction notes describe their bounded processes and cleanup.