diff --git a/docs/TestDriverGeneralisationReview.md b/docs/TestDriverGeneralisationReview.md index 7ae9bf5..0bceb73 100644 --- a/docs/TestDriverGeneralisationReview.md +++ b/docs/TestDriverGeneralisationReview.md @@ -244,3 +244,30 @@ Validation for this follow-up: initial reproduction had 20 failures and two passing controls; full suite **327 passed**. The final dynamic-dependency and strict-postcondition additions passed **32 boundary checks**, including four new cases. These counts overlap; they are not separate independent samples. + +## Isolation and repeated-action replay follow-up (2026-09-28) + +Recorded actor isolation violations now stop the runner before further actions +or judgments. Unreached scheduled assertions become INCONCLUSIVE; prior observed +product failures remain FAIL. The framework finding remains separate S3 evidence, +so it does not add or rewrite product claims. Isolation is examined at entry and +after each action. Classification requires all these checks to be present, S3, +and free of violations; crystallization inherits that gate. Older packs with +only an entry check need rerunning before automatic acceptance. Canary checks +remain a diagnostic at those boundaries, not proof against arbitrary memory +access or transient leaks inside a driver. + +Runner dispatch now passes step identity to drivers that expose `realize_step`. +Composite drivers forward it while ordinary action-only drivers keep their +existing interface. Frozen replay selects by step and verifies the action name; +repeated names no longer overwrite different targets. Unknown/mismatched steps, +duplicate frozen step ids and ambiguous action-only calls cannot send a request. +Unambiguous action-only calls remain supported. Replay has no advancing cursor, +so the same driver can run the schedule repeatedly. + +Regression coverage includes entry/mid-run/final-action leaks, otherwise passing +packs with invalid isolation evidence, distinct targets for repeated actions +through direct and composite dispatch, driver reuse and invalid frozen lookup. +Decision: `e8fabf6e-3e5e-424e-9a60-152bf3dec641`. + +Validation: the complete suite passed **343 tests** (153.67 seconds). diff --git a/research/decisions/README.md b/research/decisions/README.md index 68d7199..c6d9050 100644 --- a/research/decisions/README.md +++ b/research/decisions/README.md @@ -10,3 +10,4 @@ file is a pointer table, not a second source of truth. | TD-WP-0003 T04/T05/T08 | Python claims, concept removal and not-ready assessment | `d80734d1-01b8-4a98-8e72-c86f1806d572` | `docs/TestDriverGeneralisationReview.md` | | TD-WP-0003 T08 safety follow-up | Run-input manifests and incomplete-run handling | `afb38ade-893b-48a2-b1b3-c55e49cc40ee` | `docs/TestDriverGeneralisationReview.md` | | TD-WP-0003 T08 admission follow-up | Qualified crystallization, passing baselines and intent revisions | `88e51e10-cd32-44d2-a2d6-055675b5ce04` | `docs/TestDriverGeneralisationReview.md` | +| TD-WP-0003 T08 isolation/replay follow-up | Isolation acceptance gate and step-bound frozen replay | `e8fabf6e-3e5e-424e-9a60-152bf3dec641` | `docs/TestDriverGeneralisationReview.md` | diff --git a/src/testdriver/classification.py b/src/testdriver/classification.py index ab395e3..0dbb080 100644 --- a/src/testdriver/classification.py +++ b/src/testdriver/classification.py @@ -179,6 +179,14 @@ def _has_complete_evidence(pack: Mapping[str, Any]) -> bool: or not isinstance(o["data"], Mapping) or not o["data"] for o in records)): return False + isolation = [o for o in observations if o["kind"] == "actor_isolation"] + isolation_steps = [o["step_id"] for o in isolation] + if (len(isolation_steps) != len(steps) + 1 + or set(isolation_steps) != {None, *steps} + or any(o["stratum"] != "S3" or not isinstance(o["data"], Mapping) + or o["data"].get("violations") != [] + for o in isolation)): + return False if any(o["kind"] == "surface_violation" for o in observations): return False revisions = pack["intent_revisions"] diff --git a/src/testdriver/crystallization.py b/src/testdriver/crystallization.py index 9e69689..6750407 100644 --- a/src/testdriver/crystallization.py +++ b/src/testdriver/crystallization.py @@ -137,16 +137,28 @@ class CrystallizedDriver: def __init__(self, trajectories: Sequence[Trajectory], session_factory) -> None: self._by_step = {t.step_id: t for t in trajectories} - self._by_action = {t.action_name: t for t in trajectories} + if len(self._by_step) != len(trajectories): + raise ValueError("duplicate frozen step ids") + self._by_action: dict[str, list[Trajectory]] = {} + for trajectory in trajectories: + self._by_action.setdefault(trajectory.action_name, []).append(trajectory) self._session_factory = session_factory self.surface = None # set per action; a frozen path may span surfaces def realize(self, actor: Actor, action: SemanticAction) -> Realization: - trajectory = self._by_action.get(action.name) - if trajectory is None: + matches = self._by_action.get(action.name, []) + if len(matches) != 1: + return Realization("crystallized", {"action": action.name}, + raised="NotCrystallized: action needs an unambiguous step id") + return self.realize_step(actor, matches[0].step_id, action) + + def realize_step(self, actor: Actor, step_id: str, + action: SemanticAction) -> Realization: + trajectory = self._by_step.get(step_id) + if trajectory is None or trajectory.action_name != action.name: return Realization( "crystallized", {"action": action.name}, - raised="NotCrystallized: no frozen path for this action", + raised="NotCrystallized: no matching frozen path for this step and action", ) action.check_surface(trajectory.surface_id) args = dict(action.args) diff --git a/src/testdriver/drivers.py b/src/testdriver/drivers.py index eb869c0..f98d731 100644 --- a/src/testdriver/drivers.py +++ b/src/testdriver/drivers.py @@ -29,6 +29,18 @@ class Driver(Protocol): def realize(self, actor: Actor, action: SemanticAction) -> Realization: ... +def realize_step(driver: Driver, actor: Actor, step_id: str, + action: SemanticAction) -> Realization: + """Pass schedule identity to drivers that bind mechanics to a specific step. + + Ordinary drivers retain their action-only interface. + """ + method = getattr(driver, "realize_step", None) + if method is not None: + return method(actor, step_id, action) + return driver.realize(actor, action) + + class UnsupportedAction(Exception): """The driver has no mechanical implementation for this semantic action.""" @@ -95,11 +107,16 @@ class CompositeDriver: self.surface = drivers[default].surface def realize(self, actor: Actor, action: SemanticAction) -> Realization: + return self.realize_step(actor, None, action) + + def realize_step(self, actor: Actor, step_id: str | None, + action: SemanticAction) -> Realization: permitted = action.permitted_surfaces or {self._default} for surface_id in sorted(permitted): driver = self._drivers.get(surface_id) if driver is not None: - return driver.realize(actor, action) + return (realize_step(driver, actor, step_id, action) if step_id is not None + else driver.realize(actor, action)) raise UnsupportedAction( f"no driver for any permitted surface of {action.name!r}: " f"{sorted(permitted)}" diff --git a/src/testdriver/runner.py b/src/testdriver/runner.py index 189ff8f..28a1f1b 100644 --- a/src/testdriver/runner.py +++ b/src/testdriver/runner.py @@ -14,7 +14,7 @@ from datetime import datetime, timezone from typing import Any from .actions import SurfaceNotPermitted -from .drivers import Driver +from .drivers import Driver, realize_step from .evidence import EvidencePack, Observation, Stratum from .observers import StateObserver from .oracles import Judgment, Oracle, Verdict, overall @@ -149,12 +149,25 @@ class Runner: for claim in scenario.use_case.claims: claims_by_step.setdefault(claim.after_step, []).append(claim) + def skip_remaining(index: int, reason: str) -> None: + for skipped in scenario.steps[index:]: + for assertion in (*scenario.use_case.invariants, + *claims_by_step.get(skipped.id, ())): + judgments.append(Judgment( + assertion.id, assertion.text, Verdict.INCONCLUSIVE, + skipped.id, {"reason": reason}, + )) + for step_index, step in enumerate(scenario.steps): + if isolation: + aborted = True + skip_remaining(step_index, "framework actor isolation violated") + break actor = self._world.cast[step.actor_id] # --- S1: how it was done ------------------------------------- try: - realization = self._driver.realize(actor, step.action) + realization = realize_step(self._driver, actor, step.id, step.action) except SurfaceNotPermitted as exc: # D-05: routing around a control is a finding, not a recovery. self._record( @@ -191,6 +204,17 @@ class Runner: step.id, ) + isolation = self._isolation_violations() + self._record( + pack, Stratum.JUDGMENT, self._observer.name, "actor_isolation", + {"violations": isolation, "actors": sorted(self._world.cast.actors)}, + step.id, + ) + if isolation: + aborted = True + skip_remaining(step_index, "framework actor isolation violated") + break + # --- S3: what is now true ------------------------------------ snapshot = self._observer.snapshot() self._record( diff --git a/tests/selfverification/checks.py b/tests/selfverification/checks.py index 2329882..23084c9 100644 --- a/tests/selfverification/checks.py +++ b/tests/selfverification/checks.py @@ -103,12 +103,12 @@ def check_isolation_was_examined(pack: Mapping[str, Any]) -> list[str]: 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"] + records = [o for o in _observations(pack) if o["kind"] == "actor_isolation"] + if not records: + return ["this run did not examine actor isolation at all"] + return [f"actor isolation violated: {v}" for o in records + for v in o["data"].get("violations", [])] + # --- td://self/oracle-independence --------------------------------------- diff --git a/tests/test_isolation_and_replay.py b/tests/test_isolation_and_replay.py new file mode 100644 index 0000000..c137ca9 --- /dev/null +++ b/tests/test_isolation_and_replay.py @@ -0,0 +1,110 @@ +"""Framework isolation and frozen schedule identity are acceptance boundaries.""" +from copy import deepcopy +from dataclasses import replace +import json + +import pytest + +from scenarios.alice_bob_carol import build +from testdriver import Runner, Verdict +from testdriver.actions import SemanticAction +from testdriver.classification import classify +from testdriver.crystallization import CrystallizedDriver, Trajectory, assess_stability +from testdriver.drivers import CompositeDriver +from testdriver.scenario import Step + + +@pytest.mark.parametrize('leak_at', [None, 0, 1, 2]) +def test_isolation_breach_stops_run_and_cannot_be_accepted_or_frozen(leak_at): + world, driver, observer, asset, oracle = build() + calls = [] + + def leak(): + world.cast['bob'].remember('overheard', world.cast['alice'].canary) + + class LeakingDriver: + def realize(self, actor, action): + result = driver.realize(actor, action) + calls.append(action.name) + if len(calls) - 1 == leak_at: + leak() + return result + + if leak_at is None: + leak() + result = Runner(world, LeakingDriver(), observer, oracle).run(asset) + assert result.verdict is Verdict.INCONCLUSIVE + assert len(calls) == (0 if leak_at is None else leak_at + 1) + assert any(j.verdict is Verdict.INCONCLUSIVE for j in result.judgments) + pack = json.loads(result.evidence.to_json()) + assert any(o['data']['violations'] for o in pack['observations'] + if o['kind'] == 'actor_isolation') + assert not classify(pack, pack).safe_to_accept + assert not assess_stability([pack, deepcopy(pack), deepcopy(pack)]).stable + + +@pytest.mark.parametrize('damage', ['violation', 'missing', 'stratum', 'duplicate', 'malformed']) +def test_passing_product_verdicts_cannot_hide_invalid_isolation_evidence(damage): + packs = [] + for _ in range(3): + world, driver, observer, asset, oracle = build() + pack = json.loads(Runner(world, driver, observer, oracle).run(asset).evidence.to_json()) + guard = [o for o in pack['observations'] if o['kind'] == 'actor_isolation'][-1] + if damage == 'violation': + guard['data']['violations'] = ['actor leaked'] + elif damage == 'missing': + pack['observations'].remove(guard) + elif damage == 'stratum': + guard['stratum'] = 'S1' + elif damage == 'duplicate': + pack['observations'].append(deepcopy(guard)) + else: + guard['data'].pop('violations') + assert all(v['verdict'] == 'PASS' for v in pack['verdicts']) + assert not classify(pack, pack).safe_to_accept + packs.append(pack) + assert not assess_stability(packs).stable + + +def trajectories(): + return [Trajectory('a', 'grant_access', 'browser', '/resources/A/grant', ('subject_id',)), + Trajectory('b', 'grant_access', 'browser', '/resources/B/grant', ('subject_id',))] + + +@pytest.mark.parametrize('composite', [False, True]) +def test_runner_replays_repeated_actions_by_step_and_can_reuse_driver(composite): + world, _, observer, asset, oracle = build() + calls = [] + + class Session: + def post_form(self, path, fields): + calls.append((path, fields)) + return 200, '' + + driver = CrystallizedDriver(trajectories(), lambda actor: Session()) + if composite: + driver = CompositeDriver({'browser': driver}, 'browser') + asset.scenario = replace(asset.scenario, steps=tuple( + Step(step_id, 'alice', SemanticAction('grant_access', {'subject_id': subject}, + frozenset({'browser'}))) + for step_id, subject in [('a', 'bob'), ('b', 'carol')] + )) + for _ in range(2): + Runner(world, driver, observer, oracle).run(asset) + assert calls == [('/resources/A/grant', {'subject_id': 'bob'}), + ('/resources/B/grant', {'subject_id': 'carol'})] * 2 + + +def test_ambiguous_unknown_and_mismatched_frozen_actions_do_not_send_requests(): + world, _, _, _, _ = build() + + def unexpected_session(actor): + pytest.fail('invalid frozen dispatch must not open a session') + + driver = CrystallizedDriver(trajectories(), unexpected_session) + action = SemanticAction('grant_access', {}, frozenset({'browser'})) + assert driver.realize(world.cast['alice'], action).raised + assert driver.realize_step(world.cast['alice'], 'unknown', action).raised + assert driver.realize_step(world.cast['alice'], 'a', replace(action, name='revoke_access')).raised + with pytest.raises(ValueError, match='duplicate'): + CrystallizedDriver([trajectories()[0]] * 2, unexpected_session) diff --git a/tests/test_reference_scenario.py b/tests/test_reference_scenario.py index 70554d5..70496ec 100644 --- a/tests/test_reference_scenario.py +++ b/tests/test_reference_scenario.py @@ -80,5 +80,5 @@ def test_every_run_records_a_verdict_on_isolation(): examined = [ obs for obs in result.evidence.observations if obs.kind == "actor_isolation" ] - assert len(examined) == 1 + assert len(examined) == 4 assert examined[0].data["violations"] == [] diff --git a/workplans/TD-WP-0003-generalise-and-settle.md b/workplans/TD-WP-0003-generalise-and-settle.md index 436b3b3..6c576a1 100644 --- a/workplans/TD-WP-0003-generalise-and-settle.md +++ b/workplans/TD-WP-0003-generalise-and-settle.md @@ -337,3 +337,19 @@ postcondition guards passed **32 boundary tests** (including four new cases). The earlier classification/crystallization subset passed 69 tests. Process/path stability and captured-value redaction are covered; `git diff --check` is clean. No new task or workplan; T01/T06/T07 remain waiting and this workplan stays blocked. + + +**2026-09-28 isolation/replay follow-up — done.** Isolation breaches at entry +or after an action now abort further execution and leave unreached judgments +INCONCLUSIVE, preserving prior observed failures. Classification and +crystallization require complete, clean S3 isolation checks. Frozen replay binds +mechanics to scheduled step identity, including composite routing, and rejects +ambiguous action-only calls, mismatched steps and duplicate frozen step ids. +Ordinary drivers retain their action-only interface. + +Validation: **343 tests passed** in the full suite; the focused subset passed +81 tests. New regressions cover leaks at each action boundary, invalid isolation +evidence despite passing product verdicts, repeated action names with distinct +targets, reusable frozen drivers and invalid dispatch. `git diff --check` is +clean. Decision: `e8fabf6e-3e5e-424e-9a60-152bf3dec641`. No new task or workplan; +T01/T06/T07 remain waiting and this workplan remains blocked.