You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Facts that were expensive to find and that nobody re-derives on the way to implementing. Each is verified against code.
acquireLease cannot hold the check: it returns early on a nil lease (the default in both
binaries), again on a sticky leaseDisabled any storage backend can set, and again on heldLeases, which is session-scoped for the session's life by design. The check would fire on
the first run-entry only.
The live-run verbs touch no store, so no store decorator sees them: ApproveRun's lock-free fast
path, Cancel, CancelChild, SetMode, ApprovePlan, Persist.
engine/agent reads the shared store from model-facing tools, gated by an id-prefix family
check rather than ownership, over ids that are derived rather than secret.
StreamSessionEvents returns the log for any id the caller names, and deliberately relays EvUserPrompt and EvApproval in full.
The driver protocol is out of the enforcement path by declaration, not by accident.grpcdriver
wraps the raw ports, exposing session save/load/list/delete and all six memory methods over the
network with no service involvement. The decision is that it is declared trusted infrastructure for
now, which means the declaration itself is a deliverable here (see the criteria). Without it, anyone
who can dial the driver reaches every session and all memory regardless of what this epic ships, and
the guarantee is silently void at that endpoint.
childgc and both memory consolidators run on goroutines with no caller. They break silently the
day a check lands unless they get an explicit system principal.
Acceptance criteria
One decision function governs every owned kind — sessions, schedules, teams, memory — with a
per-kind interpretation table rather than a second mechanism per subsystem.
It is enforced where the object is touched, so a caller reaching an object through a port
directly, or through the model's own tools, is governed by the same code as one arriving at the
API.
The check runs per request. Not once per session, not once per process, and never conditional on
an optional backend being configured.
A refusal is indistinguishable from the object not existing.
Listing returns the caller's own objects and no others — both halves tested, so "return nothing"
cannot pass.
Adding a method that touches an owned object fails the build or the test suite until it is
classified as governed or explicitly exempt.
Actors with no caller run under an explicit system principal, never under an absent one.
It stays orthogonal to the model-facing posture ladder, so no posture setting can disable it.
The driver endpoint's trust status is written down as an explicit deployment requirement: it
speaks only to mecatl pods and is never tenant-reachable, enforced by a NetworkPolicy, mTLS pinning
or a unix socket. "Declared trusted" only counts once that sentence exists; silence is not an answer.
If a principal ever crosses the driver protocol, it carries a principal claim only, never
authority or scopes. A driver that receives what the caller may do has to become a policy engine,
which rebuilds the enforcement option by accident.
The decision function is shaped so a later driver-side check can call the same function rather
than growing a second one. One decision function, two enforcement points, no drift.
Proof
The same properties, adversarially, with an actor and an ordering. A property-level criterion can go green while being false; these are what stop that.
Bob lists sessions and sees only his. Alice still sees hers.
Bob prompts Alice's session twice; both are refused.
Bob asks for Alice's events by id and cannot tell refusal from not-found.
Bob approves a tool call on Alice's live run, cancels it, and flips her mode: all three refused.
All three succeed today.
A prompt-injected agent handed another tenant's subagent id gets a refusal, not the transcript.
A developer widens a store port, forgets to classify the method, and the build fails.
Slices
Decomposition is the implementer's job; these are the natural seams, not a mandate.
The one shared check, called from the store boundary.
Bob is refused on Alice's sessions, events, memory and live runs.
mecatl. After #367.
Hazards
Facts that were expensive to find and that nobody re-derives on the way to implementing. Each is verified against code.
acquireLeasecannot hold the check: it returns early on a nil lease (the default in bothbinaries), again on a sticky
leaseDisabledany storage backend can set, and again onheldLeases, which is session-scoped for the session's life by design. The check would fire onthe first run-entry only.
ApproveRun's lock-free fastpath,
Cancel,CancelChild,SetMode,ApprovePlan,Persist.engine/agentreads the shared store from model-facing tools, gated by an id-prefix familycheck rather than ownership, over ids that are derived rather than secret.
StreamSessionEventsreturns the log for any id the caller names, and deliberately relaysEvUserPromptandEvApprovalin full.grpcdriverwraps the raw ports, exposing session save/load/list/delete and all six memory methods over the
network with no service involvement. The decision is that it is declared trusted infrastructure for
now, which means the declaration itself is a deliverable here (see the criteria). Without it, anyone
who can dial the driver reaches every session and all memory regardless of what this epic ships, and
the guarantee is silently void at that endpoint.
childgcand both memory consolidators run on goroutines with no caller. They break silently theday a check lands unless they get an explicit system principal.
Acceptance criteria
per-kind interpretation table rather than a second mechanism per subsystem.
directly, or through the model's own tools, is governed by the same code as one arriving at the
API.
an optional backend being configured.
cannot pass.
classified as governed or explicitly exempt.
speaks only to mecatl pods and is never tenant-reachable, enforced by a NetworkPolicy, mTLS pinning
or a unix socket. "Declared trusted" only counts once that sentence exists; silence is not an answer.
authority or scopes. A driver that receives what the caller may do has to become a policy engine,
which rebuilds the enforcement option by accident.
than growing a second one. One decision function, two enforcement points, no drift.
Proof
The same properties, adversarially, with an actor and an ordering. A property-level criterion can go green while being false; these are what stop that.
All three succeed today.
Slices
Decomposition is the implementer's job; these are the natural seams, not a mandate.
Reasoning
The design this comes from, both on
main:Every hazard above is stated in full here rather than linked, so this issue stands on its own.