test-driver/tests/test_kernel_guarantees.py

"""The kernel must enforce the properties the T02 design claims for it.

These are unit-level checks on the kernel's construction. The behavioural
self-verification suite (actor isolation, oracle independence, evidence
reproducibility, intent independence) is TD-WP-0002-T06 and lives separately.
"""

from __future__ import annotations

import dataclasses

import pytest

from testdriver import (
    Claim, InadmissibleProvenance, Invariant, Oracle, Provenance, Runner,
    SemanticAction, StateObserver, SurfaceNotPermitted, Stratum, Verdict,
)
from lab.app import Denied, LabApp, ObservationChannel, build_baseline
from scenarios.alice_bob_carol import build


def test_implementation_derived_claims_are_rejected(): 
    """D-06: a claim derived from watching the system cannot constrain it."""
    with pytest.raises(InadmissibleProvenance) as exc:
        Claim(
            "c-observed", "whatever the system currently does",
            Provenance.AGENT_FROM_IMPLEMENTATION,
            lambda obs: True, after_step="s1",
        )
    assert "derived from the implementation" in str(exc.value)


def test_spec_and_human_provenance_are_admissible():
    for provenance in (Provenance.HUMAN, Provenance.SPEC, Provenance.AGENT_FROM_SPEC):
        Invariant("i-ok", "fine", provenance, lambda obs: True)


def test_claims_are_frozen():
    """D-02: claims are run inputs. No adaptation path may rewrite them."""
    claim = Claim("c", "text", Provenance.HUMAN, lambda obs: True, after_step="s1")
    with pytest.raises(dataclasses.FrozenInstanceError):
        claim.text = "something the implementation would prefer"


def test_surface_substitution_is_refused():
    """D-05: achieving an action through an unpermitted surface is not recovery."""
    action = SemanticAction(
        "grant_access", {"resource_id": "R"}, permitted_surfaces=frozenset({"browser"})
    )
    with pytest.raises(SurfaceNotPermitted):
        action.check_surface("api")


def test_missing_evidence_yields_inconclusive_not_pass():
    """An unjudgeable assertion must never default either way."""
    claim = Claim(
        "c-needs-missing", "depends on evidence nobody collected",
        Provenance.HUMAN, lambda obs: obs["probe_read:dave:R"], after_step="s1",
    )
    judgment = Oracle().judge(claim, {"probe_read:bob:R": True}, "s1")
    assert judgment.verdict is Verdict.INCONCLUSIVE
    assert "missing from snapshot" in judgment.detail["reason"]


def test_inconclusive_outranks_pass_in_the_run_verdict():
    from testdriver.oracles import Judgment, overall

    assert overall([
        Judgment("a", "", Verdict.PASS, None),
        Judgment("b", "", Verdict.INCONCLUSIVE, None),
    ]) is Verdict.INCONCLUSIVE


def test_actors_cannot_be_recorded_as_judgment_collectors():
    """Wiring an actor in as an observer must fail loudly, not silently pass."""
    world, driver, observer, asset, oracle = build()
    observer.name = "alice"  # an actor pretending to be the observer
    with pytest.raises(Exception) as exc:
        Runner(world, driver, observer, oracle).run(asset)
    assert "do not judge their own outcomes" in str(exc.value)


# --- preview of the M05 authorization defect (built properly in T05) --------


class RevokeIsCosmetic(LabApp):
    """Revocation updates the record and the audit trail but not enforcement.

    This is the shape of a real authorization defect: everything an operator
    would look at says access was removed, and access was not removed.
    """

    def _may_read(self, user_id: str, resource_id: str) -> bool:
        resource = self.resources.get(resource_id)
        if resource is None:
            return False
        if resource["owner"] == user_id:
            return True
        return any(
            r.event == "grant" and r.subject_id == user_id and r.resource_id == resource_id
            for r in self.audit
        )

    # NOTE: this predates the mutation catalogue, where the same defect is M15.
    # Kept as a direct subclass so the kernel test does not depend on the lab
    # catalogue's wiring being correct.


def test_seeded_authorization_defect_fails_the_run():
    """The kernel must report FAIL, not adapt, when revocation does not revoke."""
    from testdriver import Actor, Cast, DirectDriver, World
    from scenarios.alice_bob_carol import USE_CASE
    from scenarios import alice_bob_carol as ref

    lab = RevokeIsCosmetic(version="lab-0.1.0-M05-auth-defect")
    tokens = {u: lab.add_user(u) for u in ("alice", "bob", "carol")}
    cast = Cast()
    for name in tokens:
        cast.add(Actor(name, name.title(), credentials={"token": tokens[name]}))

    _, _, _, baseline_asset, _ = ref.build()
    world = World("w-defect", lab, lab.version, cast=cast)
    driver = DirectDriver(lab, tokens)
    observer = StateObserver(ObservationChannel(lab), baseline_asset.scenario.watches)

    result = Runner(world, driver, observer, Oracle()).run(baseline_asset)

    assert result.verdict is Verdict.FAIL
    assert result.judgment("c-bob-revoked").verdict is Verdict.FAIL
    # The claim set is untouched by the failure — there is no path to adapt it.
    by_id = {c.id: c for c in USE_CASE.claims}
    assert by_id["c-bob-revoked"].text == "Bob cannot read R after revocation"


def test_defect_run_emits_an_energy_event():
    """Energy events are captured; no score is computed (H-005 is dormant)."""
    import testdriver.energy as energy

    assert not hasattr(energy, "score")