T06: out-of-band self-verification
Checks written as plain functions over a serialized Evidence Pack, outside the framework - no Oracle, no Runner, no Verdict aggregation. 12 tests that they hold, 12 that they can fail. All four td://self identifiers covered. The substantive check is verdict reproducibility from S3 evidence alone, asserted on failing runs as well as passing ones. F-0003 (open): actor isolation leaves no trace in ordinary evidence - the self-test catches a shared memory store only because the harness plants per-actor canaries. Isolation is currently a property of a scenario written to expose it, not of runs in general. The mirror-image case is noted too: a guarantee enforced by construction cannot be verified by observing real runs, so four green self-tests are not four equivalent proofs. Carried to T10. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Assistant: claude-code Assistant-Model: opus Assistant-Process: 1629012@bnt-lap001 Assistant-Session: 78d4fb13-8a1e-474b-87a3-9b9261c49a39
This commit is contained in:
parent
de25673c5d
commit
5734b280c6
12 changed files with 619 additions and 6 deletions
|
|
@ -17,7 +17,7 @@
|
|||
| task | TD-WP-0002-T02 | done | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
| task | TD-WP-0002-T03 | done | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
| task | TD-WP-0002-T04 | done | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
| task | TD-WP-0002-T05 | todo | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
| task | TD-WP-0002-T05 | done | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
| task | TD-WP-0002-T06 | todo | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
| task | TD-WP-0002-T07 | todo | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
| task | TD-WP-0002-T08 | todo | — | workplans/TD-WP-0002-vertical-spike-crystallization.md |
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# Concept ↔ Implementation Fitness Map
|
||||
|
||||
**Updated:** 2026-08-22 (TD-WP-0002-T05)
|
||||
**Updated:** 2026-08-22 (TD-WP-0002-T06)
|
||||
|
||||
Traces each important concept to the implementation, experiment and evidence that
|
||||
support it. **Unsupported entries are the point of this map** — a concept with no
|
||||
|
|
@ -25,15 +25,15 @@ were aspirational, not evidenced.
|
|||
| Concept | Level | Implementation | Experiment | Evidence | Open question |
|
||||
|---|---|---|---|---|---|
|
||||
| `C-use-case` | C1 | `intent.py` | — | — | Is a use case expressible without leaking mechanics? |
|
||||
| `C-actor-isolation` | C1 | `world.py` | E-001 | — | Isolation is asserted by construction; unverified. |
|
||||
| `C-actor-isolation` | C1 | `world.py` | E-001 | `td://self/actor-isolation` | **F-0003** — only observable when the scenario plants canaries. |
|
||||
| `C-semantic-action` | C1 | `actions.py` | E-001 | — | Does identity survive restructuring better than a recorded sequence? (H-001) |
|
||||
| `C-oracle-independence` | C1 | `runner.py`, `oracles.py` | E-001, E-003 | — | Independence of components ≠ independence of belief. (H-004) |
|
||||
| `C-evidence-pack` | C1 | `evidence.py` | — | — | What is the minimum sufficient for replay? |
|
||||
| `C-evidence-pack` | C1 | `evidence.py` | — | `td://self/evidence-reproducibility` | Verdicts are reproducible from S3 alone, on passing and failing runs. |
|
||||
| `C-observation-channel` | C1 | `lab/app.py` | — | — | **D-07** — required of every system under test. Adoption cost unknown. |
|
||||
| `C-adaptation` | C1 | — (T08) | E-001 | — | (H-002) |
|
||||
| `C-classification` | C1 | — (T08) | E-001, E-003 | — | Decision table is total on paper; unexercised. |
|
||||
| `C-crystallization` | C1 | — (T09) | E-002 | — | (H-003) |
|
||||
| `C-intent-provenance` | C1 | `provenance.py` | E-003 | — | Constrains provenance, not quality. Accepted residual. |
|
||||
| `C-intent-provenance` | C1 | `provenance.py` | E-003 | `td://self/intent-independence` | Constrains provenance, not quality. Accepted residual. |
|
||||
| `C-lineage` | C0 | — | — | — | Parent pointer only in the spike. |
|
||||
| `C-energy` | C0 | `energy.py`, capture only | — | — | Dormant by decision. (H-005) |
|
||||
| `C-temperature` | C0 | — | — | — | Deferred. No implementation planned in TD-WP-0002. |
|
||||
|
|
|
|||
75
research/findings/F-0003-isolation-needs-canaries.md
Normal file
75
research/findings/F-0003-isolation-needs-canaries.md
Normal file
|
|
@ -0,0 +1,75 @@
|
|||
---
|
||||
id: F-0003
|
||||
type: framework-finding
|
||||
class: FRAMEWORK_LIMITATION
|
||||
status: open
|
||||
discovered: "2026-08-22"
|
||||
discovered_by: TD-WP-0002-T06
|
||||
workplan: TD-WP-0002
|
||||
task: TD-WP-0002-T06
|
||||
carried_to: TD-WP-0002-T10
|
||||
---
|
||||
|
||||
# F-0003 — Actor isolation is only observable if the scenario plants canaries
|
||||
|
||||
## Observation
|
||||
|
||||
Writing `td://self/actor-isolation` out-of-band exposed something the concept
|
||||
model does not acknowledge: **an isolation violation leaves no trace in ordinary
|
||||
evidence.**
|
||||
|
||||
The self-test only detects a shared memory store because the test harness first
|
||||
gives each actor a distinguishable private secret and then looks for it in the
|
||||
wrong places. Remove that instrumentation and a run in which Alice, Bob and Carol
|
||||
share one memory dict produces an Evidence Pack indistinguishable from a correct
|
||||
one — same observations, same verdicts, same everything.
|
||||
|
||||
So the guarantee holds in the reference scenario *because it was instrumented to
|
||||
be checkable*, not because runs generally reveal it.
|
||||
|
||||
## Why it matters
|
||||
|
||||
`INTENT.md` and the Concept Model treat actor isolation as a property of the
|
||||
framework. As implemented it is a property of a *scenario that was written to
|
||||
expose it*. Every ordinary scenario — the ones users will actually write —
|
||||
carries no canaries, and for those the framework's central multi-user claim is
|
||||
asserted rather than verified.
|
||||
|
||||
This matters more once actors are agentic (T07). A shared session, a cached HTTP
|
||||
client, or a module-level default is exactly how isolation breaks in practice,
|
||||
and none of those announce themselves.
|
||||
|
||||
## A second, related limitation
|
||||
|
||||
`td://self/oracle-independence` has a mirror-image problem. The framework
|
||||
*prevents* an actor from collecting S2/S3 evidence — `Runner` raises
|
||||
`CollectorIndependenceError` — so no real run can produce the violating artefact.
|
||||
The check is therefore exercised against a hand-built pack.
|
||||
|
||||
That is the right architecture and a weak self-test at once: **a guarantee
|
||||
enforced by construction cannot be verified by observing real runs.** The suite
|
||||
now asserts both halves — that the door is locked, and that we would notice
|
||||
someone coming through the window — but the second half tests the check, not the
|
||||
system.
|
||||
|
||||
Worth stating plainly rather than counting four green self-tests as four
|
||||
equivalent proofs. They are not equivalent.
|
||||
|
||||
## Candidate resolutions
|
||||
|
||||
Not resolved now; deciding cheaply here would be guessing.
|
||||
|
||||
1. **Automatic canaries** — the runtime seeds each actor with a unique private
|
||||
marker at construction and the isolation check runs on every Evidence Pack,
|
||||
making isolation continuously observable rather than specially tested.
|
||||
Cheap, and the obvious first move.
|
||||
2. **Accept and document** — isolation is enforced by construction, and the
|
||||
self-test covers the construction rather than each run. Honest, but leaves the
|
||||
multi-user claim resting on code review.
|
||||
3. **Both** — canaries for observability, plus an explicit statement that some
|
||||
guarantees are structural and are verified once rather than per run.
|
||||
|
||||
Carried to `TD-WP-0002-T10`, where it should be answered together with the wider
|
||||
question of which guarantees are structural and which are observed. Reassess
|
||||
after T07, when agentic actors make the failure mode concrete rather than
|
||||
theoretical.
|
||||
0
tests/selfverification/__init__.py
Normal file
0
tests/selfverification/__init__.py
Normal file
BIN
tests/selfverification/__pycache__/__init__.cpython-312.pyc
Normal file
BIN
tests/selfverification/__pycache__/__init__.cpython-312.pyc
Normal file
Binary file not shown.
BIN
tests/selfverification/__pycache__/checks.cpython-312.pyc
Normal file
BIN
tests/selfverification/__pycache__/checks.cpython-312.pyc
Normal file
Binary file not shown.
Binary file not shown.
Binary file not shown.
219
tests/selfverification/checks.py
Normal file
219
tests/selfverification/checks.py
Normal file
|
|
@ -0,0 +1,219 @@
|
|||
"""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
|
||||
|
||||
|
||||
# --- 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
|
||||
188
tests/selfverification/test_checks_can_fail.py
Normal file
188
tests/selfverification/test_checks_can_fail.py
Normal file
|
|
@ -0,0 +1,188 @@
|
|||
"""A self-test that cannot fail is worth nothing.
|
||||
|
||||
Every check in `checks.py` is fed a deliberately broken artefact here, and must
|
||||
complain. Without this file, the self-verification suite would be a row of green
|
||||
ticks with no evidence that any of them is load-bearing.
|
||||
|
||||
Two kinds of break appear below, and the difference is worth noticing:
|
||||
|
||||
* **structural breaks** — the guarantee is actually violated in a running
|
||||
system (actors sharing memory). The check must catch it from the evidence.
|
||||
* **artefact breaks** — the guarantee cannot be violated through the framework
|
||||
because the architecture forbids it, so the check is exercised against a
|
||||
hand-built pack instead. Where that applies it is stated explicitly, together
|
||||
with the separate assertion that the framework does refuse.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import copy
|
||||
import json
|
||||
|
||||
import pytest
|
||||
|
||||
from testdriver import Actor, Cast, Oracle, Runner, World
|
||||
from testdriver.runner import CollectorIndependenceError
|
||||
from lab.mutations import ObservationChannel, build_lab
|
||||
from testdriver import DirectDriver, StateObserver
|
||||
from scenarios.alice_bob_carol import USE_CASE, build
|
||||
from tests.selfverification.checks import (
|
||||
check_actor_isolation,
|
||||
check_evidence_supports_every_verdict,
|
||||
check_intent_independence,
|
||||
check_no_actor_collected_judgment,
|
||||
check_runs_agree,
|
||||
check_verdicts_follow_from_judgment_evidence,
|
||||
)
|
||||
from tests.selfverification.test_self_verification import SECRETS, run_and_serialize
|
||||
|
||||
|
||||
# --- td://self/actor-isolation -------------------------------------------
|
||||
|
||||
|
||||
def test_shared_actor_memory_is_caught():
|
||||
"""A structural break: two actors handed the same private store.
|
||||
|
||||
This is what an isolation bug actually looks like when the same agent
|
||||
technology executes several actors in one process — nobody writes
|
||||
`bob.memory = alice.memory`, but a shared default or a cached client
|
||||
achieves it by accident.
|
||||
"""
|
||||
lab, tokens = build_lab()
|
||||
shared: dict = {}
|
||||
cast = Cast()
|
||||
for name in ("alice", "bob", "carol"):
|
||||
actor = Actor(name, name.title(), credentials={"token": tokens[name]})
|
||||
object.__setattr__(actor, "_memory", shared) # the leak
|
||||
cast.add(actor)
|
||||
|
||||
_, _, _, asset, _ = build()
|
||||
world = World("w-leaky", lab, lab.version, cast=cast)
|
||||
driver = DirectDriver(lab, tokens)
|
||||
observer = StateObserver(ObservationChannel(lab), asset.scenario.watches)
|
||||
|
||||
for actor_id, secret in SECRETS.items():
|
||||
world.cast[actor_id].remember(f"private-{actor_id}", secret)
|
||||
|
||||
result = Runner(world, driver, observer, Oracle()).run(asset)
|
||||
pack = json.loads(result.evidence.to_json())
|
||||
memories = {a.id: {k: a.recall(k) for k in a.known_keys()} for a in world.cast}
|
||||
|
||||
violations = check_actor_isolation(pack, SECRETS, memories)
|
||||
assert violations, "shared actor memory went undetected"
|
||||
assert any("holds" in v for v in violations)
|
||||
|
||||
|
||||
def test_a_secret_leaking_into_the_record_is_caught():
|
||||
"""An artefact break: the leak escapes into evidence even if memory is clean."""
|
||||
pack, memories, _ = run_and_serialize()
|
||||
tampered = copy.deepcopy(pack)
|
||||
for obs in tampered["observations"]:
|
||||
if obs["collector"] == "alice":
|
||||
obs["data"]["stolen"] = SECRETS["bob"]
|
||||
break
|
||||
assert check_actor_isolation(tampered, SECRETS, memories)
|
||||
|
||||
|
||||
# --- td://self/oracle-independence ---------------------------------------
|
||||
|
||||
|
||||
def test_the_framework_refuses_to_let_an_actor_collect_judgment_evidence():
|
||||
"""The architecture prevents this, so it cannot be produced by a real run."""
|
||||
world, driver, observer, asset, oracle = build()
|
||||
observer.name = "bob"
|
||||
with pytest.raises(CollectorIndependenceError):
|
||||
Runner(world, driver, observer, oracle).run(asset)
|
||||
|
||||
|
||||
def test_actor_collected_judgment_evidence_is_caught_in_the_record():
|
||||
"""...and if it ever did appear in a pack, the out-of-band check sees it.
|
||||
|
||||
Both halves are needed. The first says the door is locked; this one says we
|
||||
would notice if someone came through the window.
|
||||
"""
|
||||
pack, _, actors = run_and_serialize()
|
||||
tampered = copy.deepcopy(pack)
|
||||
for obs in tampered["observations"]:
|
||||
if obs["stratum"] == "S3":
|
||||
obs["collector"] = "bob"
|
||||
break
|
||||
assert check_no_actor_collected_judgment(tampered, actors)
|
||||
|
||||
|
||||
def test_a_verdict_that_contradicts_its_evidence_is_caught():
|
||||
"""The strongest of the checks: verdicts must follow from S3 alone."""
|
||||
pack, _, _ = run_and_serialize()
|
||||
tampered = copy.deepcopy(pack)
|
||||
tampered["verdicts"][0]["verdict"] = "FAIL" # a verdict nothing supports
|
||||
assertions = list(USE_CASE.claims) + list(USE_CASE.invariants)
|
||||
violations = check_verdicts_follow_from_judgment_evidence(tampered, assertions)
|
||||
assert violations
|
||||
assert "retained judgment evidence yields" in violations[0]
|
||||
|
||||
|
||||
def test_a_pass_silently_replacing_a_fail_is_caught():
|
||||
"""The specific corruption the project most needs to notice."""
|
||||
pack, _, _ = run_and_serialize("M15")
|
||||
tampered = copy.deepcopy(pack)
|
||||
for verdict in tampered["verdicts"]:
|
||||
if verdict["verdict"] == "FAIL":
|
||||
verdict["verdict"] = "PASS"
|
||||
assertions = list(USE_CASE.claims) + list(USE_CASE.invariants)
|
||||
assert check_verdicts_follow_from_judgment_evidence(tampered, assertions)
|
||||
|
||||
|
||||
# --- td://self/evidence-reproducibility -----------------------------------
|
||||
|
||||
|
||||
def test_a_verdict_without_a_snapshot_is_caught():
|
||||
pack, _, _ = run_and_serialize()
|
||||
tampered = copy.deepcopy(pack)
|
||||
tampered["observations"] = [
|
||||
o for o in tampered["observations"] if o["kind"] != "state_snapshot"
|
||||
]
|
||||
assert check_evidence_supports_every_verdict(tampered)
|
||||
|
||||
|
||||
def test_a_verdict_without_a_record_of_how_the_step_ran_is_caught():
|
||||
pack, _, _ = run_and_serialize()
|
||||
tampered = copy.deepcopy(pack)
|
||||
tampered["observations"] = [
|
||||
o for o in tampered["observations"] if o["kind"] != "realization"
|
||||
]
|
||||
violations = check_evidence_supports_every_verdict(tampered)
|
||||
assert any("how" in v for v in violations)
|
||||
|
||||
|
||||
def test_evidence_that_does_not_name_the_version_is_caught():
|
||||
pack, _, _ = run_and_serialize()
|
||||
tampered = copy.deepcopy(pack)
|
||||
tampered["sut_version"] = ""
|
||||
assert check_evidence_supports_every_verdict(tampered)
|
||||
|
||||
|
||||
def test_disagreeing_runs_are_caught():
|
||||
first, _, _ = run_and_serialize()
|
||||
second, _, _ = run_and_serialize("M15")
|
||||
assert check_runs_agree(first, second)
|
||||
|
||||
|
||||
# --- td://self/intent-independence ----------------------------------------
|
||||
|
||||
|
||||
def test_implementation_derived_intent_is_caught():
|
||||
pack, _, _ = run_and_serialize("M15")
|
||||
tampered = copy.deepcopy(pack)
|
||||
tampered["provenance_index"]["c-bob-revoked"] = "agent-from-implementation"
|
||||
violations = check_intent_independence(tampered)
|
||||
assert violations
|
||||
assert "derived from the implementation" in violations[0]
|
||||
|
||||
|
||||
def test_unrecorded_provenance_is_caught():
|
||||
"""Absent provenance is not a benign omission — it makes the verdict
|
||||
unauditable, which for this framework is the same as unusable."""
|
||||
pack, _, _ = run_and_serialize()
|
||||
tampered = copy.deepcopy(pack)
|
||||
tampered["provenance_index"] = {}
|
||||
assert check_intent_independence(tampered)
|
||||
110
tests/selfverification/test_self_verification.py
Normal file
110
tests/selfverification/test_self_verification.py
Normal file
|
|
@ -0,0 +1,110 @@
|
|||
"""The framework's foundational guarantees, verified from outside the framework.
|
||||
|
||||
These read an Evidence Pack the way an auditor would — as JSON, with no live
|
||||
objects — and use plain pytest. No Oracle, no Runner, no Verdict aggregation.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import json
|
||||
|
||||
import pytest
|
||||
|
||||
from testdriver import Runner
|
||||
from scenarios.alice_bob_carol import USE_CASE, build
|
||||
from tests.selfverification.checks import (
|
||||
SELF_CHECKS,
|
||||
check_actor_isolation,
|
||||
check_evidence_supports_every_verdict,
|
||||
check_intent_independence,
|
||||
check_no_actor_collected_judgment,
|
||||
check_runs_agree,
|
||||
check_verdicts_follow_from_judgment_evidence,
|
||||
)
|
||||
|
||||
SECRETS = {
|
||||
"alice": "alice-only-9f3c",
|
||||
"bob": "bob-only-2a71",
|
||||
"carol": "carol-only-55e0",
|
||||
}
|
||||
|
||||
|
||||
def run_and_serialize(*mutations: str):
|
||||
"""Run, then throw away everything except the serialized evidence.
|
||||
|
||||
Deliberate: the checks must work from the artefact alone, exactly as they
|
||||
would months later, with no access to the objects that produced it.
|
||||
"""
|
||||
world, driver, observer, asset, oracle = build(*mutations)
|
||||
for actor_id, secret in SECRETS.items():
|
||||
world.cast[actor_id].remember("private", secret)
|
||||
result = Runner(world, driver, observer, oracle).run(asset)
|
||||
pack = json.loads(result.evidence.to_json())
|
||||
memories = {a.id: {k: a.recall(k) for k in a.known_keys()} for a in world.cast}
|
||||
return pack, memories, list(world.cast.actors)
|
||||
|
||||
|
||||
def test_the_registry_is_complete():
|
||||
assert len(SELF_CHECKS) == 4
|
||||
|
||||
|
||||
# --- td://self/actor-isolation -------------------------------------------
|
||||
|
||||
|
||||
def test_actor_isolation():
|
||||
pack, memories, _ = run_and_serialize()
|
||||
assert check_actor_isolation(pack, SECRETS, memories) == []
|
||||
|
||||
|
||||
# --- td://self/oracle-independence ---------------------------------------
|
||||
|
||||
|
||||
def test_no_actor_collected_judgment_evidence():
|
||||
pack, _, actors = run_and_serialize()
|
||||
assert check_no_actor_collected_judgment(pack, actors) == []
|
||||
|
||||
|
||||
@pytest.mark.parametrize("mutations", [(), ("M15",), ("M11",), ("M01", "M15")])
|
||||
def test_verdicts_are_reproducible_from_judgment_evidence_alone(mutations):
|
||||
"""Holds on passing and failing runs alike — a check that only works when
|
||||
everything is green is not verifying independence, it is verifying luck."""
|
||||
pack, _, _ = run_and_serialize(*mutations)
|
||||
assertions = list(USE_CASE.claims) + list(USE_CASE.invariants)
|
||||
assert check_verdicts_follow_from_judgment_evidence(pack, assertions) == []
|
||||
|
||||
|
||||
# --- td://self/evidence-reproducibility -----------------------------------
|
||||
|
||||
|
||||
def test_every_verdict_is_supported_by_retained_evidence():
|
||||
pack, _, _ = run_and_serialize()
|
||||
assert check_evidence_supports_every_verdict(pack) == []
|
||||
|
||||
|
||||
def test_two_runs_from_the_same_seed_agree():
|
||||
first, _, _ = run_and_serialize()
|
||||
second, _, _ = run_and_serialize()
|
||||
assert check_runs_agree(first, second) == []
|
||||
assert first["run_id"] != second["run_id"]
|
||||
|
||||
|
||||
def test_reproducibility_holds_on_a_failing_run():
|
||||
first, _, _ = run_and_serialize("M15")
|
||||
second, _, _ = run_and_serialize("M15")
|
||||
assert check_runs_agree(first, second) == []
|
||||
assert any(v["verdict"] == "FAIL" for v in first["verdicts"])
|
||||
|
||||
|
||||
# --- td://self/intent-independence ----------------------------------------
|
||||
|
||||
|
||||
def test_intent_independence():
|
||||
pack, _, _ = run_and_serialize()
|
||||
assert check_intent_independence(pack) == []
|
||||
|
||||
|
||||
def test_intent_independence_holds_when_a_claim_fails():
|
||||
"""The moment that matters: a FAIL is an accusation, and an accusation
|
||||
resting on implementation-derived intent is worthless."""
|
||||
pack, _, _ = run_and_serialize("M15")
|
||||
assert check_intent_independence(pack) == []
|
||||
|
|
@ -269,7 +269,7 @@ Three results worth carrying:
|
|||
|
||||
```task
|
||||
id: TD-WP-0002-T06
|
||||
status: todo
|
||||
status: done
|
||||
priority: medium
|
||||
state_hub_task_id: "4fb31485-8650-556c-bee4-b4e067a89d04"
|
||||
```
|
||||
|
|
@ -282,6 +282,27 @@ Exit: deliberately breaking actor isolation fails the out-of-band check;
|
|||
allowing an actor to determine its own verdict fails oracle-independence;
|
||||
each failure produces a Framework Finding.
|
||||
|
||||
**Done 2026-08-22.** `tests/selfverification/` — checks as plain functions over a
|
||||
serialized Evidence Pack, plus 12 tests that they hold and 12 that they *can
|
||||
fail*. All four `td://self/...` identifiers are covered. 72 tests pass overall.
|
||||
|
||||
- The strongest check turned out to be **verdict reproducibility from S3 alone**:
|
||||
re-evaluating each assertion against the stored snapshots, with no actor,
|
||||
driver or live system in reach, must reproduce exactly what the run reported.
|
||||
It is asserted on failing runs too — a check that only works when everything is
|
||||
green verifies luck, not independence.
|
||||
- **F-0003 (open)** — actor isolation leaves no trace in ordinary evidence. The
|
||||
self-test catches a shared memory store only because the harness plants
|
||||
per-actor canaries first; without them, a run where all three actors share one
|
||||
memory dict produces an Evidence Pack identical to a correct one. Isolation is
|
||||
currently a property of a scenario written to expose it, not of runs in
|
||||
general. Carried to T10, reassess after T07.
|
||||
- The same finding notes the mirror-image problem: oracle independence is
|
||||
enforced by construction, so no real run can produce the violating artefact and
|
||||
the check must be exercised against a hand-built pack. **A guarantee enforced
|
||||
by construction cannot be verified by observing real runs.** Four green
|
||||
self-tests are not four equivalent proofs, and the suite now says so.
|
||||
|
||||
## Agentic realisation of one semantic action, fully instrumented
|
||||
|
||||
```task
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue