test-driver/tests/selfverification/checks.py

"""Out-of-band verification of test-driver's own foundational guarantees.

These checks are deliberately **not** written using test-driver. Using the
framework to establish that the framework's oracles are independent is a system
certifying itself: any flaw serious enough to matter would likely be shared by
both the thing under test and the thing testing it.

So: plain functions over an Evidence Pack, plain pytest assertions, no `Oracle`,
no `Runner`, no `Verdict` aggregation. They read the same artefact an auditor
would read six months later, and nothing else.

Each check returns a list of violation strings — empty means satisfied. Returning
data rather than asserting keeps the checks usable both as tests and, later, as
the `td://self/...` verification assets themselves.

Registry of self-verification identifiers:

    td://self/actor-isolation
    td://self/oracle-independence
    td://self/evidence-reproducibility
    td://self/intent-independence

A check that cannot fail is worth nothing, so every check here has a
corresponding case in `test_checks_can_fail.py` that feeds it a deliberately
broken artefact and asserts it complains.
"""

from __future__ import annotations

import json
from typing import Any, Iterable, Mapping

SELF_CHECKS = (
    "td://self/actor-isolation",
    "td://self/oracle-independence",
    "td://self/evidence-reproducibility",
    "td://self/intent-independence",
)

# Provenance values that may back an assertion capable of producing FAIL.
ADMISSIBLE_PROVENANCE = frozenset({"human", "spec", "agent-from-spec"})


def _observations(pack: Mapping[str, Any]) -> list[dict]:
    return list(pack.get("observations", ()))


def _snapshots_by_step(pack: Mapping[str, Any]) -> dict[str, dict]:
    return {
        obs["step_id"]: obs["data"]
        for obs in _observations(pack)
        if obs["kind"] == "state_snapshot"
    }


# --- td://self/actor-isolation -------------------------------------------


def check_actor_isolation(
    pack: Mapping[str, Any],
    secrets_by_actor: Mapping[str, str],
    memories_by_actor: Mapping[str, Mapping[str, Any]],
) -> list[str]:
    """No actor may hold or emit anything private to another actor.

    Checked two ways, because either alone is weak:

    * **memory** — actor A's private store must not contain actor B's secret;
    * **evidence** — an observation attributed to actor A must not carry B's
      secret, which would mean the leak escaped into the record even if A's
      memory looked clean.
    """
    violations: list[str] = []

    for actor, memory in memories_by_actor.items():
        rendered = json.dumps(memory, default=str)
        for other, secret in secrets_by_actor.items():
            if other != actor and secret in rendered:
                violations.append(
                    f"actor {actor!r} holds {other!r}'s private value in memory"
                )

    for obs in _observations(pack):
        collector = obs.get("collector")
        if collector not in secrets_by_actor:
            continue
        rendered = json.dumps(obs.get("data"), default=str)
        for other, secret in secrets_by_actor.items():
            if other != collector and secret in rendered:
                violations.append(
                    f"observation {obs['id']} collected by {collector!r} "
                    f"carries {other!r}'s private value"
                )
    return violations


def check_isolation_was_examined(pack: Mapping[str, Any]) -> list[str]:
    """Every run must carry a verdict on actor isolation — F-0003, resolved.

    Before this existed, isolation was only observable in scenarios written to
    expose it: a run in which every actor shared one memory store produced
    evidence indistinguishable from a correct one. Actors now carry an automatic
    private marker and the runner examines them on every scenario, so the absence
    of this observation is itself a failure.
    """
    for obs in _observations(pack):
        if obs["kind"] != "actor_isolation":
            continue
        violations = obs["data"].get("violations") or []
        return [f"actor isolation violated: {v}" for v in violations]
    return ["this run did not examine actor isolation at all"]


# --- td://self/oracle-independence ---------------------------------------


def check_no_actor_collected_judgment(
    pack: Mapping[str, Any], actor_ids: Iterable[str]
) -> list[str]:
    """S2 and S3 evidence must never be attributed to an actor."""
    actors = set(actor_ids)
    return [
        f"{obs['stratum']} observation {obs['id']} was collected by actor "
        f"{obs['collector']!r}"
        for obs in _observations(pack)
        if obs["stratum"] in ("S2", "S3") and obs["collector"] in actors
    ]


def check_verdicts_follow_from_judgment_evidence(
    pack: Mapping[str, Any], assertions: Iterable[Any]
) -> list[str]:
    """Every recorded verdict must be reproducible from S3 evidence alone.

    This is the substantive independence check. Re-evaluating each assertion
    against the stored snapshots — with no actor, no driver and no live system in
    reach — must reproduce exactly what the run reported. If it does not, then
    something outside the judgment stratum influenced the verdict, whatever the
    architecture diagram claims.
    """
    violations: list[str] = []
    snapshots = _snapshots_by_step(pack)
    recorded = {(v["assertion_id"], v["step_id"]): v["verdict"] for v in pack["verdicts"]}

    for assertion in assertions:
        for (assertion_id, step_id), verdict in recorded.items():
            if assertion_id != assertion.id:
                continue
            snapshot = snapshots.get(step_id)
            if snapshot is None:
                violations.append(
                    f"verdict {assertion_id}@{step_id} has no S3 snapshot to rest on"
                )
                continue
            try:
                expected = "PASS" if assertion.predicate(snapshot) else "FAIL"
            except KeyError:
                expected = "INCONCLUSIVE"
            if expected != verdict:
                violations.append(
                    f"verdict {assertion_id}@{step_id} recorded {verdict}, but the "
                    f"retained judgment evidence yields {expected}"
                )
    return violations


# --- td://self/evidence-reproducibility -----------------------------------


def check_evidence_supports_every_verdict(pack: Mapping[str, Any]) -> list[str]:
    """A verdict with no evidence behind it is an EVIDENCE_FAILURE, not a result."""
    violations: list[str] = []
    snapshots = _snapshots_by_step(pack)
    steps_with_surface = {
        obs["step_id"] for obs in _observations(pack) if obs["kind"] == "realization"
    }

    for verdict in pack["verdicts"]:
        step_id = verdict["step_id"]
        if step_id not in snapshots:
            violations.append(
                f"verdict {verdict['assertion_id']}@{step_id} has no state snapshot"
            )
        if step_id not in steps_with_surface:
            violations.append(
                f"verdict {verdict['assertion_id']}@{step_id} has no record of how "
                "the step was performed"
            )
    if not pack.get("sut_version"):
        violations.append("evidence does not identify the version under test")
    if not pack.get("finished_at"):
        violations.append("evidence does not record when the run ended")
    return violations


def check_runs_agree(first: Mapping[str, Any], second: Mapping[str, Any]) -> list[str]:
    """Two runs from the same seed must reach the same judgments."""
    def key(pack):
        return sorted(
            (v["assertion_id"], v["step_id"], v["verdict"]) for v in pack["verdicts"]
        )

    if key(first) != key(second):
        return ["two runs from the same initial state disagreed"]
    if first["sut_version"] != second["sut_version"]:
        return ["runs were taken against different versions"]
    return []


# --- td://self/intent-independence ----------------------------------------


def check_intent_independence(pack: Mapping[str, Any]) -> list[str]:
    """No verdict may rest on intent derived from the implementation.

    Independence of *components* does not give independence of *belief*. A
    verdict is only worth something if the claim behind it came from somewhere
    the implementation could not reach.
    """
    violations: list[str] = []
    index = pack.get("provenance_index", {})

    for verdict in pack["verdicts"]:
        assertion_id = verdict["assertion_id"]
        provenance = index.get(assertion_id)
        if provenance is None:
            violations.append(
                f"assertion {assertion_id!r} produced a verdict with no recorded "
                "provenance — its independence cannot be audited"
            )
        elif provenance not in ADMISSIBLE_PROVENANCE:
            violations.append(
                f"assertion {assertion_id!r} has provenance {provenance!r}, which is "
                "derived from the implementation it constrains"
            )
    return violations