tegwick
cf682281d7
Assistant: codex Assistant-Model: gpt-6-astra Assistant-Session: 01a0e76f-be98-7ae3-965d-e0b31290a4c4
70 lines
3.2 KiB
Python
70 lines
3.2 KiB
Python
"""Same-name resources, explicit foreign access and delete/recreate isolation."""
|
|
from testdriver import (
|
|
Actor, Cast, Claim, Invariant, Oracle, Provenance, Scenario, SemanticAction,
|
|
Step, UseCase, VerificationAsset, World,
|
|
)
|
|
from lab.workflows import TenantLab, TenantObserver, WorkflowDriver
|
|
|
|
SOURCE = "usecases/generalisation-spec.md#tenant-lifecycle"
|
|
PROVENANCE = Provenance.AGENT_FROM_SPEC
|
|
|
|
|
|
def isolated_reads(obs):
|
|
for actor, own, foreign in (("admin-a", "A", "B"), ("admin-b", "B", "A")):
|
|
if obs["reads"][f"{actor}:{foreign}"] != {"allowed": False, "content": None}:
|
|
return False
|
|
record = obs["records"][own]
|
|
if obs["reads"][f"{actor}:{own}"] != {"allowed": record is not None, "content": record}:
|
|
return False
|
|
return True
|
|
|
|
|
|
def foreign_delete_refused(obs):
|
|
return (obs["receipts"][-1]["allowed"] is False
|
|
and obs["records"] == {"A": "alpha", "B": "beta"})
|
|
|
|
|
|
USE_CASE = UseCase(
|
|
"uc-tenant-lifecycle", "Tenant-scoped deletion and recreation",
|
|
"Two administrators use R independently; deleting and recreating A never affects B.",
|
|
PROVENANCE, source_ref=SOURCE,
|
|
claims=(
|
|
Claim("tenant-create-a", "A holds alpha", PROVENANCE,
|
|
lambda o: o["records"] == {"A": "alpha", "B": None}, "create-a", SOURCE),
|
|
Claim("tenant-create-b", "Same local name preserves both records", PROVENANCE,
|
|
lambda o: o["records"] == {"A": "alpha", "B": "beta"}, "create-b", SOURCE),
|
|
Claim("tenant-deny-a", "A cannot delete B", PROVENANCE,
|
|
foreign_delete_refused, "foreign-a", SOURCE),
|
|
Claim("tenant-deny-b", "B cannot delete A", PROVENANCE,
|
|
foreign_delete_refused, "foreign-b", SOURCE),
|
|
Claim("tenant-delete", "Deleting A preserves B", PROVENANCE,
|
|
lambda o: o["records"] == {"A": None, "B": "beta"}, "delete-a", SOURCE),
|
|
Claim("tenant-recreate", "Recreate does not resurrect or overwrite", PROVENANCE,
|
|
lambda o: o["records"] == {"A": "new-alpha", "B": "beta"}, "recreate-a", SOURCE),
|
|
),
|
|
invariants=(Invariant("tenant-reads", "Read enforcement matches tenant records",
|
|
PROVENANCE, isolated_reads, SOURCE),),
|
|
)
|
|
|
|
|
|
def build(defect=None):
|
|
lab = TenantLab(defect)
|
|
cast = Cast()
|
|
for actor, token in lab.tokens.items():
|
|
cast.add(Actor(actor, actor.title(), credentials={"token": token}))
|
|
schedule = (
|
|
("create-a", "admin-a", "create", "A", "alpha"),
|
|
("create-b", "admin-b", "create", "B", "beta"),
|
|
("foreign-a", "admin-a", "delete", "B", None),
|
|
("foreign-b", "admin-b", "delete", "A", None),
|
|
("delete-a", "admin-a", "delete", "A", None),
|
|
("recreate-a", "admin-a", "create", "A", "new-alpha"),
|
|
)
|
|
scenario = Scenario("sc-tenant-lifecycle", USE_CASE, tuple(
|
|
Step(id, actor, SemanticAction(operation, {"tenant": tenant, "content": content},
|
|
frozenset({"workflow"})))
|
|
for id, actor, operation, tenant, content in schedule
|
|
), variant=defect or "baseline")
|
|
return (World("w-tenant", lab, f"tenant-1/{defect or 'baseline'}", cast),
|
|
WorkflowDriver(lab), TenantObserver(lab),
|
|
VerificationAsset("va-tenant", scenario), Oracle())
|