tegwick
5734b280c6
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
75 lines
3.2 KiB
Markdown
75 lines
3.2 KiB
Markdown
---
|
|
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.
|