bvisor/contract/

qualification.rs

//! The QUALIFICATION axis (proof-spine §0/§1) — ORTHOGONAL to the RuntimeGuarantee
//! axis ([`crate::contract::capability::Enforcement`]). Never collapse them.
//!
//! - **RuntimeGuarantee** ([`Enforcement`]): what a backend CLAIMS it can guarantee
//!   for a particular plan + machine profile.
//! - **QualificationStatus** (this module): what the REPOSITORY has INDEPENDENTLY
//!   qualified through the complete path `spec → admission → lowering → execution →
//!   independent observation`, INCLUDING the fail-closed / teardown branches.
//!
//! THE COUPLING LAW: a production profile may advertise [`Enforcement::Enforced`]
//! for a requirement key ONLY when the committed qualification ledger holds
//! [`QualificationStatus::Proven`] for that key — with a profile floor the machine
//! satisfies and a matching mechanism digest. The coupling is enforced as a CI
//! GATE: the backend's ceiling claim is explicit; the ledger is DERIVED from proof
//! receipts; the gate asserts they agree. A backend can never self-stamp `Proven`.
//!
//! This is the structural fix for the over-claim class: the family `support_matrix`
//! may CLAIM `Enforced` as aspiration, but production advertises it only when the
//! claim is `Proven` — so an unproven advertised cell is an `Incomplete`
//! qualification, not a lie.

use crate::contract::capability::Enforcement;
use crate::contract::support::RequirementKind;
use serde::{Deserialize, Serialize};

/// What the repository has INDEPENDENTLY qualified about a capability claim.
/// Distinct from [`Enforcement`] (the runtime claim a backend makes).
///
/// Serialized to/from the committed qualification ledger (kebab-case) so the
/// integrity coupling gate — which cannot depend on this crate — reads it as data.
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
#[serde(rename_all = "kebab-case")]
#[non_exhaustive]
pub enum QualificationStatus {
    /// The complete contract path PLUS its fail-closed / teardown branches were
    /// observed by an INDEPENDENT oracle (host-side kernel-state preferred over
    /// workload self-report; dual-channel). The ONLY status that permits a
    /// production `Enforced` claim, for the matching key + profile-floor + digest.
    Proven,
    /// Explicitly unsupported on this platform/profile; planning REFUSES before
    /// execution. The fail-closed default for any unproven capability. NOT a
    /// waiver — a platform limitation is `FailClosed`, never `Waived`.
    FailClosed,
    /// Some layers exist (a mechanism, a partial path) but the claimed guarantee
    /// is NOT proven end-to-end. May not be advertised `Enforced` in production.
    Incomplete,
    /// Mechanically impossible to witness, OR deliberately excluded — carried as an
    /// owner-signed, EXPIRING waiver (owner + reason + expiry). NEVER describes a
    /// platform capability limitation.
    Waived,
    /// Test-only support that exists to PROVE detection (a red fixture's planted
    /// lie). Never a production claim.
    FaultInjected,
}

impl QualificationStatus {
    /// The coupling-law predicate: whether this qualification permits a production
    /// [`Enforcement::Enforced`] runtime claim. ONLY [`Self::Proven`] does.
    #[must_use]
    pub fn permits_enforced(self) -> bool {
        matches!(self, Self::Proven)
    }
}

/// The coupling-law check at a single (key, profile, claim) point: a runtime
/// [`Enforcement`] claim is admissible against a qualification only when either the
/// claim is not `Enforced`, or the qualification is `Proven`. (The full gate also
/// matches the profile floor and mechanism digest — those live in the ledger + the
/// integrity gate; this is the pointwise core, kept here so it is unit-testable and
/// shared by the runtime if it ever consults a qualification.)
#[must_use]
pub fn enforced_claim_is_qualified(claim: Enforcement, qualification: QualificationStatus) -> bool {
    match claim {
        Enforcement::Enforced => qualification.permits_enforced(),
        // A backend may always claim a weaker guarantee than it has proven.
        Enforcement::Mediated | Enforcement::Unsupported => true,
    }
}

/// A `blake3` digest of a backend's MECHANISM string for a requirement key (§1's
/// `H_M`). The coupling law binds a production `Enforced` claim to a `Proven`
/// ledger row ONLY when the row's digest matches the digest of the mechanism the
/// backend would actually use — so a backend cannot satisfy the gate by swapping
/// in a different (unproven) mechanism under the same key.
///
/// Derived with [`batpak::event::hash::compute_hash`] (the same blake3 the
/// launcher attestation uses), over the UTF-8 bytes of the mechanism string a
/// backend authors in its `mechanism(req, enforcement)` (e.g.
/// `"linux:landlock:Enforced"`).
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
pub struct MechanismDigest(pub [u8; 32]);

impl MechanismDigest {
    /// Derive the digest from a backend's mechanism string (the exact bytes a
    /// backend's `mechanism(req, enforcement)` returns, e.g.
    /// `"linux:landlock:Enforced"`).
    #[must_use]
    pub fn of_mechanism(mechanism: &str) -> Self {
        Self(batpak::event::hash::compute_hash(mechanism.as_bytes()))
    }

    /// The lowercase hex spelling of the 32-byte digest (for the committed ledger
    /// + diagnostics). Deterministic, so a ledger row's digest is one stable line.
    #[must_use]
    pub fn to_hex(self) -> String {
        self.0.iter().map(|b| format!("{b:02x}")).collect()
    }
}

/// The MINIMUM machine facts a qualification covers (§3 PROFILE-CLASS): the floor
/// predicate a production profile must DOMINATE (`p_prod ⊒ floor`) for a `Proven`
/// receipt earned at the floor to transfer to it.
///
/// A qualification is earned on ONE probed CI runner, but production runs
/// elsewhere; an exact-profile digest would never transfer. So the floor states
/// the LEAST the mechanism needs, and the load-bearing argument is that proving AT
/// the floor generalizes UPWARD — a stronger machine still satisfies every minimum.
/// `satisfied_by` is exactly that domination check.
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
pub struct ProfileFloor {
    /// The minimum landlock ABI the mechanism requires (`None` = landlock is not
    /// part of this floor — e.g. a cgroup-only Kill cell does not need landlock).
    pub landlock_abi_min: Option<u8>,
    /// The mechanism requires atomic `cgroup.kill` run-tree teardown.
    pub requires_cgroup_kill: bool,
    /// The mechanism requires the `pids.peak` usage witness (cgroup v2 ≥ 6.1).
    pub requires_pids_peak: bool,
    /// The mechanism requires UNPRIVILEGED user + network namespace creation (the
    /// `NetworkDenyAll` empty-netns floor, S9 / D3): an unprivileged process may create a
    /// new netns ONLY when it is also root in a new userns (the S8 rendezvous). A kernel
    /// that forbids unprivileged userns cannot realize the empty netns, so the cell is
    /// FAIL_CLOSED there — never a silent pass.
    pub requires_unprivileged_userns: bool,
    /// The mechanism requires installing a seccomp BPF FILTER (the
    /// `ChildSpawn::DenyNewTasks` floor, S10): a kernel without `CONFIG_SECCOMP_FILTER`
    /// cannot install the task-creation denylist, so the cell is FAIL_CLOSED there — never
    /// a silent unfiltered run.
    pub requires_seccomp_filter: bool,
}

impl ProfileFloor {
    /// The empty floor: no minimum machine facts (structural mechanisms that hold
    /// on every machine of the platform — e.g. process spawn / pipe capture).
    #[must_use]
    pub const fn structural() -> Self {
        Self {
            landlock_abi_min: None,
            requires_cgroup_kill: false,
            requires_pids_peak: false,
            requires_unprivileged_userns: false,
            requires_seccomp_filter: false,
        }
    }

    /// The empty-netns `NetworkDenyAll` floor (S9 / D3): requires unprivileged
    /// user + network namespace creation, no landlock / cgroup minimum. Structural
    /// otherwise (the empty netns holds on any kernel that permits unprivileged userns).
    #[must_use]
    pub const fn unprivileged_userns_netns() -> Self {
        Self {
            landlock_abi_min: None,
            requires_cgroup_kill: false,
            requires_pids_peak: false,
            requires_unprivileged_userns: true,
            requires_seccomp_filter: false,
        }
    }

    /// The `ChildSpawn::DenyNewTasks` floor (S10): requires seccomp FILTER support. No
    /// landlock / cgroup / userns minimum — the task-creation denylist is structural above
    /// that floor (it holds on any kernel with `CONFIG_SECCOMP_FILTER`), so the proof
    /// transfers upward. Below the floor the cell drops from the ceiling (fail-closed).
    #[must_use]
    pub const fn seccomp_filter() -> Self {
        Self {
            landlock_abi_min: None,
            requires_cgroup_kill: false,
            requires_pids_peak: false,
            requires_unprivileged_userns: false,
            requires_seccomp_filter: true,
        }
    }

    /// The `ChildSpawn::AllowDescendantsWithinBoundary` floor (S10): requires the cgroup
    /// `cgroup.kill` boundary (the S1 Kill mechanism the descendant inherits), no seccomp /
    /// landlock / userns minimum — the descendant is killable + counted + namespace-trapped
    /// by the cgroup. Below the floor (no cgroup) the cell drops from the ceiling.
    #[must_use]
    pub const fn cgroup_descendant_boundary() -> Self {
        Self {
            landlock_abi_min: None,
            requires_cgroup_kill: true,
            requires_pids_peak: false,
            requires_unprivileged_userns: false,
            requires_seccomp_filter: false,
        }
    }

    /// THE §3 DOMINATION CHECK: whether the concrete machine `facts` satisfy every
    /// minimum this floor requires (`facts ⊒ self`). A production profile may
    /// advertise the qualification's key ONLY when this holds — so a receipt earned
    /// at the floor transfers UPWARD to any stronger machine but NEVER downward to a
    /// weaker one.
    #[must_use]
    pub fn satisfied_by(&self, facts: &ProfileFacts) -> bool {
        if let Some(min) = self.landlock_abi_min {
            if facts.landlock_abi < i64::from(min) {
                return false;
            }
        }
        if self.requires_cgroup_kill && !facts.has_cgroup_kill {
            return false;
        }
        if self.requires_pids_peak && !facts.has_pids_peak {
            return false;
        }
        if self.requires_unprivileged_userns && !facts.has_unprivileged_userns {
            return false;
        }
        if self.requires_seccomp_filter && !facts.has_seccomp_filter {
            return false;
        }
        true
    }
}

/// The concrete, TYPED machine facts a [`ProfileFloor`] is checked against — the
/// probe truths a backend derives once at construction (the live landlock ABI, and
/// whether the kernel exposes atomic `cgroup.kill` / the `pids.peak` witness).
///
/// Distinct from [`crate::contract::support::BackendProfile`] (the per-kind
/// enforcement CEILING): the ceiling is the OUTPUT of these facts, while the floor
/// predicate is stated over the facts THEMSELVES (the ABI integer, the cgroup
/// presence) — a ceiling has no ABI integer to compare a floor against.
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct ProfileFacts {
    /// The live landlock ABI integer probed from the kernel (`0` = unavailable).
    pub landlock_abi: i64,
    /// Whether the probed cgroup base exposes atomic `cgroup.kill`.
    pub has_cgroup_kill: bool,
    /// Whether the probed cgroup base exposes the `pids.peak` usage witness.
    pub has_pids_peak: bool,
    /// Whether the host permits UNPRIVILEGED user + network namespace creation (the
    /// `NetworkDenyAll` empty-netns floor, S9 / D3). Probed once at construction
    /// (`unprivileged_userns_available`); `false` ⇒ the empty-netns cell fails closed.
    pub has_unprivileged_userns: bool,
    /// Whether the host supports installing a seccomp BPF FILTER (the
    /// `ChildSpawn::DenyNewTasks` floor, S10). Probed once at construction
    /// (`seccomp_filter_available`); `false` ⇒ the task-creation-deny cell fails closed.
    pub has_seccomp_filter: bool,
}

/// One committed row of the qualification LEDGER (§1 `Qualification(p,k)` joined to
/// its profile-class + mechanism digest + proof receipt). The ledger is the
/// REPOSITORY's independent record; a backend never authors it.
///
/// A row may carry [`QualificationStatus::Proven`] ONLY if every entry in
/// `proof_receipts` cites a REAL, currently-passing oracle test (`path::fn`) — and
/// together they prove the COMPLETE §4 contract path INCLUDING the fail-closed /
/// teardown branch (a cell's guarantee-holds and its setup-failure ⇒ no-effect are
/// usually distinct oracles). The coupling test enforces the §1 law: every
/// production-`Enforced` ceiling cell must have a `Proven` row here whose
/// [`ProfileFloor`] the running profile satisfies AND whose [`MechanismDigest`]
/// matches the backend's mechanism for that key; the proof-receipt RESOLVER
/// (`coupling_proof.rs`) additionally fails CI if any cited receipt is a ghost.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct QualificationRow {
    /// The backend family id this qualification was earned for (e.g. `"linux"`).
    pub backend: &'static str,
    /// The requirement key this row qualifies.
    pub key: RequirementKind,
    /// The minimum machine facts the proof generalizes from (§3).
    pub profile_floor: ProfileFloor,
    /// The exact backend MECHANISM STRING this row proves (e.g.
    /// `"linux:landlock:Enforced"`). Stored as the source string — not a
    /// pre-baked digest — because blake3 is not `const`; the coupling test
    /// re-derives [`MechanismDigest::of_mechanism`] from this AND from the
    /// backend's live `mechanism(req, enforcement)` and asserts they MATCH, so a
    /// backend cannot satisfy the gate under a different (unproven) mechanism.
    pub mechanism: &'static str,
    /// What the repository independently qualified for this cell.
    pub status: QualificationStatus,
    /// The proof receipts: the `path::fn`s of the oracle tests that TOGETHER prove
    /// the cell's complete §4 path (guarantee-holds + fail-closed branch). Empty for
    /// non-`Proven` rows. Every entry is machine-resolved to a real `#[test]` by the
    /// resolver gate — a `Proven` row may NOT cite a ghost.
    pub proof_receipts: &'static [&'static str],
}

impl QualificationRow {
    /// The blake3 [`MechanismDigest`] (§1 `H_M`) of this row's committed mechanism
    /// string — the digest the coupling gate matches the backend's live mechanism
    /// against.
    #[must_use]
    pub fn mechanism_digest(&self) -> MechanismDigest {
        MechanismDigest::of_mechanism(self.mechanism)
    }
}

/// Derive the [`MechanismDigest`] for a Linux mechanism string built the way
/// `backend_impl::mechanism` builds it: `"{id}:{primitive}:{enforcement:?}"`. The
/// ledger is committed `const`, but a digest is a runtime blake3, so the ledger
/// stores the SOURCE mechanism string and the coupling test re-derives the digest;
/// this helper keeps the two spellings (ledger vs. backend) in one place.
#[must_use]
pub fn linux_mechanism(primitive: &str, enforcement: Enforcement) -> String {
    format!("linux:{primitive}:{enforcement:?}")
}

/// Derive the [`MechanismDigest`] source string for a Wasm mechanism.
#[must_use]
pub fn wasm_mechanism(primitive: &str, enforcement: Enforcement) -> String {
    format!("wasm:{primitive}:{enforcement:?}")
}

/// 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`.
pub const LINUX_QUALIFICATION_LEDGER: &[QualificationRow] = &[
    QualificationRow {
        backend: "linux",
        key: RequirementKind::Filesystem,
        // Landlock ABI v1 already enforces path-beneath read/write/execute — the
        // backend's floor. The proof transfers to any higher ABI.
        profile_floor: ProfileFloor {
            landlock_abi_min: Some(1),
            requires_cgroup_kill: false,
            requires_pids_peak: false,
            requires_unprivileged_userns: false,
            requires_seccomp_filter: false,
        },
        mechanism: "linux:landlock:Enforced",
        status: QualificationStatus::Proven,
        // Guarantee-holds: independent on-disk G-grid denial oracle. Fail-closed:
        // below the ABI floor the cell drops from the ceiling (the coupling test
        // `below_floor_profile_drops_filesystem_from_the_ceiling` proves it).
        proof_receipts: &[
            "crates/bvisor/tests/grid_linux_fs.rs::g1_landlock_denies_secret_read_outside_declared_root",
        ],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::LaunchWorkload,
        profile_floor: ProfileFloor::structural(),
        mechanism: "linux:process_spawn:Enforced",
        status: QualificationStatus::Proven,
        // §4 BOTH branches: guarantee-holds (a workload launches + runs to a verdict)
        // AND fail-closed (a setup problem REFUSES before any child — the target
        // never runs).
        proof_receipts: &[
            "crates/bvisor/tests/launcher_capture_linux.rs::launcher_captures_workload_streams_cleanly_and_deterministically",
            "crates/bvisor/tests/launcher_skeleton_linux.rs::missing_primitive_refuses_before_any_child",
        ],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::CaptureStreams,
        profile_floor: ProfileFloor::structural(),
        mechanism: "linux:pipe_capture:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/launcher_capture_linux.rs::launcher_captures_workload_streams_cleanly_and_deterministically",
        ],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::Kill,
        // Kill rides cgroup v2 atomic `cgroup.kill`; no landlock minimum.
        profile_floor: ProfileFloor {
            landlock_abi_min: None,
            requires_cgroup_kill: true,
            requires_pids_peak: false,
            requires_unprivileged_userns: false,
            requires_seccomp_filter: false,
        },
        mechanism: "linux:cgroup_kill:Enforced",
        status: QualificationStatus::Proven,
        // §4: host-state oracle (kernel pids.events) + workload exit (dual channel)
        // AND teardown observed (cgroup.kill drains the tree to empty).
        proof_receipts: &[
            "crates/bvisor/tests/cgroup_enforcement_linux.rs::pids_max_genuinely_denies_forks_past_the_cap_or_explicit_skip",
        ],
    },
    // Non-proven cells, status stated explicitly. These keys are absent from the
    // production ceiling, so the coupling test never demands a Proven row for them;
    // they are listed so the ledger states the qualification status explicitly. The
    // mechanism string for an unimplemented cell mirrors `backend_impl::mechanism`'s
    // `"none/unimplemented-this-chunk"` primitive (Unsupported in the ceiling).
    QualificationRow {
        backend: "linux",
        key: RequirementKind::Environment,
        // Explicit-envp lowering is structural (no kernel-version floor): the launcher
        // serves the admitted env to fexecve on any Linux. The proof transfers to every
        // machine of the platform.
        profile_floor: ProfileFloor::structural(),
        mechanism: "linux:explicit_env:Enforced",
        status: QualificationStatus::Proven,
        // §4 BOTH branches, dual-channel:
        //  - guarantee-holds: the child's env EQUALS the admitted table EXACTLY,
        //    witnessed by the HOST reading /proc/<child_pid>/environ (kernel state,
        //    independent) AND the workload's own reported env; a parent sentinel var is
        //    ABSENT in the child (no ambient leak); a SecretLease resolves IN THE CHILD
        //    while the serialized plan+report carry only the REF, never the value;
        //  - fail-closed: an unresolvable lease ⇒ the target NEVER runs (no child
        //    output), and a contract-invalid policy ⇒ admission refuses before execution.
        proof_receipts: &[
            "crates/bvisor/tests/env_exact_linux.rs::child_env_equals_the_admitted_table_with_no_ambient_leak",
            "crates/bvisor/tests/env_exact_linux.rs::an_unresolvable_lease_fails_closed_and_the_target_never_runs",
            "crates/bvisor/tests/env_exact_linux.rs::a_contract_invalid_policy_is_refused_before_execution",
            // The full execute()/BoundaryRunner contract-path witness (vs the launcher-
            // direct /proc oracle above): the durable plan+report carry only the lease ref.
            "crates/bvisor/tests/env_exact_linux.rs::a_secret_lease_resolves_but_the_durable_plan_and_report_carry_only_the_ref",
        ],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::InheritedFdsNone,
        // The fd-scrub is structural (no kernel-version floor): the launcher reads
        // /proc/self/fd + raw SYS_close on any Linux. The proof transfers to every
        // machine of the platform.
        profile_floor: ProfileFloor::structural(),
        mechanism: "linux:fd_scrub:Enforced",
        status: QualificationStatus::Proven,
        // §4 BOTH branches, dual-channel:
        //  - guarantee-holds: the child's open fds (read HOST-SIDE from
        //    /proc/<child_pid>/fd — kernel state, independent) contain ONLY the declared
        //    allowlist (stdio); a parent-opened non-CLOEXEC SENTINEL fd is ABSENT from the
        //    child (scrubbed), witnessed both host-side AND by the workload's own attempt
        //    to write to it failing (no leak across the boundary);
        //  - fail-closed: an undeclared inherited fd is scrubbed BEFORE the workload (the
        //    launcher mechanism proof), AND a contract-level setup failure ⇒ the target
        //    NEVER runs (the full execute()/BoundaryRunner path refuses an unrealized fd
        //    policy). The execute()-path witness proves the lowering rides the production
        //    contract, not only a run_launcher-direct plan.
        proof_receipts: &[
            "crates/bvisor/tests/inherited_fds_none_linux.rs::child_inherits_only_the_declared_fds_no_sentinel_leak",
            "crates/bvisor/tests/launcher_inherited_fds_linux.rs::undeclared_inherited_fd_is_scrubbed_before_the_workload",
            "crates/bvisor/tests/inherited_fds_none_linux.rs::an_unrealized_fd_policy_fails_closed_and_the_target_never_runs",
            // The full execute()/BoundaryRunner contract-path witness (vs the launcher-
            // direct /proc oracle above): a None-policy spec runs to a clean verdict.
            "crates/bvisor/tests/inherited_fds_none_linux.rs::a_none_policy_spec_runs_through_the_execute_path",
        ],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::InheritedFdsOnly,
        profile_floor: ProfileFloor::structural(),
        mechanism: "linux:none/unimplemented-this-chunk:Unsupported",
        status: QualificationStatus::Incomplete,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::NetworkDenyAll,
        // The empty-netns floor (S9 / D3): requires UNPRIVILEGED user + network namespace
        // creation (the S8 rendezvous makes the child root-in-userns; CLONE_NEWNET then
        // births it into an empty netns). No landlock/cgroup minimum — the empty netns is
        // structural above that floor, so the proof transfers to any kernel that permits
        // unprivileged userns. Below the floor the cell drops from the ceiling (fail-closed).
        profile_floor: ProfileFloor::unprivileged_userns_netns(),
        mechanism: "linux:empty_netns:Enforced",
        status: QualificationStatus::Proven,
        // §4 BOTH branches, DUAL channel (host-side kernel-state strongest, per §4):
        //  - guarantee-holds (A) HOST-SIDE: the host reads the CHILD's netns interface list
        //    from /proc/<child_pid>/net/dev and asserts it contains ONLY `lo` — NO external
        //    interface (the independent "zero external interfaces" witness, kernel state the
        //    launcher cannot forge); (B) WORKLOAD self-report: the workload enumerates its
        //    own interfaces + routing table and OBSERVES it has ZERO routes (only `lo`, which
        //    has no address ⇒ no reachable destination). NO-LEAK: no inherited routable socket
        //    survives (the S5 scrub).
        //    HOSTCONTROL: the launcher's own control channel still works through the netns
        //    (the workload runs to a verdict);
        //  - fail-closed: a kernel without unprivileged userns+netns ⇒ the cell SKIPs LOUD
        //    (never a silent pass), and a contract-level setup failure ⇒ the target never runs
        //    (the empty netns engages on the full execute()/BoundaryRunner path).
        proof_receipts: &[
            "crates/bvisor/tests/network_deny_all_linux.rs::host_sees_only_loopback_in_the_child_netns_no_external_interface_or_skip",
            "crates/bvisor/tests/network_deny_all_linux.rs::workload_cannot_reach_the_network_from_the_empty_netns_or_skip",
            "crates/bvisor/tests/network_deny_all_linux.rs::a_deny_all_spec_runs_through_the_execute_path_or_skip",
            "crates/bvisor/tests/network_deny_all_linux.rs::network_allow_list_fails_closed_at_admission_the_target_never_runs",
        ],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::NetworkAllowList,
        profile_floor: ProfileFloor::structural(),
        mechanism: "linux:none/unimplemented-this-chunk:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    // The three FROZEN child-task semantics (proof-spine S6). S6 froze the taxonomy +
    // the clone3-pointer/classic-BPF enforcement CONSTRAINT (see `SpawnPolicy`); S10
    // realizes two of the three and keeps the unenforceable one FailClosed:
    //
    // - DenyNewTasks → PROVEN via a seccomp DENYLIST (deny clone/clone3/fork/vfork at the
    //   syscall-NUMBER level — no clone3 arg-deref). Floor = seccomp filter support.
    // - AllowDescendants → PROVEN via the CGROUP boundary (the descendant inherits the run
    //   cgroup ⇒ killable via cgroup.kill, counted by pids.max, namespace-trapped — NOT
    //   seccomp). Floor = cgroup.kill.
    // - AllowThreads → STAYS FailClosed: the clone3-pointer/classic-BPF problem (S6) means
    //   seccomp cannot permit-threads-but-deny-processes precisely, and denying clone3
    //   outright breaks glibc threads. The OPEN enforcement problem — NOT faked, absent
    //   from the ceiling (Unsupported), so the coupling gate never demands a Proven row.
    QualificationRow {
        backend: "linux",
        key: RequirementKind::ChildSpawnDenyNewTasks,
        // The seccomp-filter floor (S10): requires CONFIG_SECCOMP_FILTER. No landlock /
        // cgroup / userns minimum — the task-creation denylist is structural above that
        // floor (it holds on any kernel with seccomp filter mode), so the proof transfers
        // upward. Below the floor the cell drops from the ceiling (fail-closed).
        profile_floor: ProfileFloor::seccomp_filter(),
        mechanism: "linux:seccomp_deny_tasks:Enforced",
        status: QualificationStatus::Proven,
        // §4 BOTH branches, DUAL channel (host-side kernel-state strongest, per §4):
        //  - guarantee-holds (A) HOST-SIDE: the host reads the CHILD's /proc/<pid>/status
        //    and observes `Seccomp: 2` (filter mode installed — the kernel-state witness the
        //    launcher cannot forge); (B) WORKLOAD self-report: the workload attempts to spawn
        //    a child and OBSERVES the fork/spawn is REFUSED (EPERM). NO-LEAK: the filter is
        //    installed LAST, after landlock, before fexecve;
        //  - fail-closed: a kernel without seccomp filter support ⇒ the cell SKIPs LOUD
        //    (never a silent pass), and a contract-level setup failure ⇒ the target never
        //    runs (the seccomp denylist engages on the full execute()/BoundaryRunner path).
        proof_receipts: &[
            "crates/bvisor/tests/child_spawn_linux.rs::deny_new_tasks_fork_is_refused_and_host_sees_seccomp_filter_or_skip",
            "crates/bvisor/tests/child_spawn_linux.rs::a_deny_new_tasks_spec_runs_through_the_execute_path_or_skip",
            "crates/bvisor/tests/child_spawn_linux.rs::allow_threads_fails_closed_at_admission_the_target_never_runs",
        ],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::ChildSpawnAllowThreads,
        // STAYS FailClosed: the open clone3-pointer/classic-BPF problem (S6). NOT faked.
        profile_floor: ProfileFloor::structural(),
        mechanism: "linux:none/unimplemented-this-chunk:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "linux",
        key: RequirementKind::ChildSpawnAllowDescendants,
        // The cgroup-boundary floor (S10): requires cgroup.kill (the descendant inherits the
        // run cgroup ⇒ killable + counted + namespace-trapped — NOT seccomp). Below the
        // floor (no cgroup) the cell drops from the ceiling (fail-closed).
        profile_floor: ProfileFloor::cgroup_descendant_boundary(),
        mechanism: "linux:cgroup_descendant_boundary:Enforced",
        status: QualificationStatus::Proven,
        // §4 BOTH branches:
        //  - guarantee-holds: the workload (placed in the run cgroup via CLONE_INTO_CGROUP — the
        //    SAME placement the S1 Kill cell proves) spawns a DESCENDANT that OUTLIVES it; the
        //    descendant is in the leaf by the kernel fork-membership guarantee (it cannot leave
        //    its cgroup without a privileged cgroup.procs write it lacks), and cgroup.kill reaps
        //    the WHOLE leaf to empty (the S1 drain-to-empty witness — the OBSERVED branch). A
        //    direct per-descendant cgroup.procs membership read is a tracked §4-quality
        //    strengthening; today the descendant claim rests on the fork-inheritance guarantee +
        //    the whole-tree drain, not a direct membership observation.
        //  - fail-closed: no cgroup base ⇒ the cell SKIPs LOUD (absent from the ceiling), and
        //    a contract-level setup failure ⇒ the target never runs.
        proof_receipts: &[
            "crates/bvisor/tests/child_spawn_linux.rs::allow_descendants_is_cgroup_confined_and_cgroup_kill_drains_the_tree_or_skip",
            "crates/bvisor/tests/child_spawn_linux.rs::an_allow_descendants_spec_runs_through_the_execute_path_or_skip",
        ],
    },
];

/// Look up the committed Linux ledger row for a requirement key (the lookup the
/// coupling gate uses). `None` ⇒ the key is not in the ledger at all (which, for an
/// `Enforced` production cell, is itself a coupling violation).
#[must_use]
pub fn linux_ledger_row(key: RequirementKind) -> Option<&'static QualificationRow> {
    LINUX_QUALIFICATION_LEDGER.iter().find(|r| r.key == key)
}

/// The committed Wasm qualification ledger. Every production `Enforced` Wasm
/// ceiling cell has a `Proven` row backed by the live grid oracle; structurally
/// unsupported native cells are stated explicitly and stay absent from the ceiling.
pub const WASM_QUALIFICATION_LEDGER: &[QualificationRow] = &[
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::Filesystem,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:wasi_preopen:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::g1_wasi_preopen_denies_secret_read_outside_declared_root",
            "crates/bvisor/tests/grid_wasm.rs::g3_wasi_preopen_denies_write_outside_quarantine",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::LaunchWorkload,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:wasi_instantiate:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::wasm_profile_admits_declared_roots_spec",
            "crates/bvisor/tests/grid_wasm.rs::g7_wasi_preopen_commit_allows_in_root_output",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::CaptureStreams,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:wasi_stdio:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::wasi_capture_streams_records_guest_output",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::Environment,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:wasi_env:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::wasi_env_exact_is_delivered_to_guest",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::TempRoot,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:wasi_preopen_tmp:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::wasi_temp_root_is_private_and_writable",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::CommitArtifact,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:preopen_commit:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::g7_wasi_preopen_commit_allows_in_root_output",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::DiscardArtifact,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:preopen_commit:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::wasi_temp_root_is_private_and_writable",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::ListOutputs,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:preopen_readdir:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::g7_wasi_preopen_commit_allows_in_root_output",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::NetworkDenyAll,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:no_socket_cap:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::wasi_socket_capability_is_absent",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::InheritedFdsNone,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:wasi_stdio:Enforced",
        status: QualificationStatus::Proven,
        proof_receipts: &[
            "crates/bvisor/tests/grid_wasm.rs::wasi_no_inherited_fds_contract_runs_without_raw_fd_authority",
        ],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::InheritedFdsOnly,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:none/structurally-unsupported:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::ChildSpawnDenyNewTasks,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:none/structurally-unsupported:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::ChildSpawnAllowThreads,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:none/structurally-unsupported:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::ChildSpawnAllowDescendants,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:none/structurally-unsupported:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::Kill,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:none/structurally-unsupported:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::ExposePath,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:none/structurally-unsupported:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
    QualificationRow {
        backend: "wasm",
        key: RequirementKind::NetworkAllowList,
        profile_floor: ProfileFloor::structural(),
        mechanism: "wasm:none/structurally-unsupported:Unsupported",
        status: QualificationStatus::FailClosed,
        proof_receipts: &[],
    },
];

/// Look up the committed Wasm ledger row for a requirement key.
#[must_use]
pub fn wasm_ledger_row(key: RequirementKind) -> Option<&'static QualificationRow> {
    WASM_QUALIFICATION_LEDGER.iter().find(|r| r.key == key)
}

#[cfg(test)]
#[path = "qualification_tests.rs"]
mod tests;