Constant LINUX_QUALIFICATION_LEDGER 

pub const LINUX_QUALIFICATION_LEDGER: &[QualificationRow];

The COMMITTED Linux qualification ledger (S1): the CURRENTLY-PROVEN cells, each citing its real passing oracle(s), plus the explicitly-stated non-proven cells.

PROVEN rows cite a real, currently-passing oracle that proves the complete contract path (verified to exist in crates/bvisor/tests/):

• Filesystem — landlock denial proven on-disk by the independent G-grid oracle (above the ABI floor; below it the cell is fail-closed, never advertised).
• Kill — atomic cgroup.kill teardown DRAINS the tree to empty (observed via the bounded wait_until_empty poll), paired with the pids cap proof.
• LaunchWorkload / CaptureStreams — the launcher spawns + the host captures the workload’s own stdout/stderr cleanly (no launcher contamination).
• process_count budget — the cgroup pids.max cap GENUINELY denies forks past the cap (kernel pids.events max counter), witnessed from pids.peak. (process_count is a budget dimension, not a RequirementKind; it rides the Kill cell’s cgroup floor, so it is documented here, not a separate row.)

Environment (explicit envp) — the admitted Environment::Exact policy is lowered to the launcher’s explicit env (literals plus parent-resolved secret leases); the child env EQUALS the admitted table EXACTLY, witnessed by the host reading the child’s proc environ AND the workload’s own self-report (dual channel, no ambient leak), with the fail-closed branches (an unresolvable lease means the target never runs; an invalid policy means admission refuses) proven by the same oracle.

InheritedFdsNone (fd-scrub) — the admitted FdPolicy::None drives the launcher’s child-side fd-scrub; the child’s open fds (read HOST-SIDE from /proc/<pid>/fd) contain ONLY the declared allowlist, a parent-opened non-CLOEXEC sentinel fd is ABSENT (scrubbed), with the fail-closed branches (an undeclared fd is scrubbed before the workload; an unrealized fd policy ⇒ the target never runs) proven by the oracle.

NetworkDenyAll (empty netns, S9 / D3) — the admitted NetPolicy::DenyAll engages a NEW, EMPTY network namespace (CLONE_NEWNET, alongside the S8 userns rendezvous it requires); the netns has NO external interface, witnessed HOST-SIDE (the host reads the CHILD’s /proc/<pid>/net/dev and sees ONLY lo) AND by the workload’s own self-report (it cannot reach the network), with the launcher’s own control channel still working through the netns (HostControl carve-out — fd-passed sockets are unaffected). Fail-closed branches: a kernel without unprivileged userns+netns ⇒ the cell SKIPs LOUD (floor not met), and an unrealized AllowList ⇒ the target never runs. NetworkAllowList STAYS FailClosed (no broker in v1).

NON-PROVEN cells are stated explicitly (the coupling test asserts they are NOT advertised Enforced in production): InheritedFdsOnly is Incomplete (the scrub realizes only None; the selective-keep allowlist has no lowering + no oracle); every other capability — including NetworkAllowList (no broker in v1) and all THREE ChildSpawn child-task keys (proof-spine §2 split + the S6 3-variant freeze) — is FailClosed.