"""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