115 lines
5.2 KiB
Markdown
115 lines
5.2 KiB
Markdown
# T8.3 — Keyed capability
|
||||
|
|
|
|||
|
|
| Field | Value |
|
|||
|
|
|---|---|
|
|||
|
|
| Phase | P8 — Operability |
|
|||
|
|
| Size | L — over 3 days |
|
|||
|
|
| Status | Not started |
|
|||
|
|
| Flags | — |
|
|||
|
|
| Spec | inlined below |
|
|||
|
|
| Blocks | — |
|
|||
|
|
|
|||
|
|
## Goal
|
|||
|
|
|
|||
|
|
Make an `Idempotent` declaration enforceable: the kernel derives and supplies the
|
|||
|
|
idempotency key on every call, and a write issued without it is denied.
|
|||
|
|
|
|||
|
|
## Facts (inlined — no spec read needed)
|
|||
|
|
|
|||
|
|
- **A framework cannot trust a user-supplied `EffectClass`.** A tool declared
|
|||
|
|
`Idempotent` that is not will be retried after an indeterminate crash, and the
|
|||
|
|
damage is the user's data.
|
|||
|
|
- Three layers, in order of strength:
|
|||
|
|
1. **Declaration** — required, recorded, auditable (T2.2).
|
|||
|
|
2. **Keyed capability** — this task.
|
|||
|
|
3. **Sandbox** — shadow and replay deny `Unsafe` outright (T6.5).
|
|||
|
|
- **Layer 2 is the one that makes layer 1 more than paperwork.**
|
|||
|
|
- **`Idempotent` is a claim about *retry*, not about abstaining from writes.**
|
|||
|
|
Denying an `Idempotent` tool network and filesystem writes would deny the
|
|||
|
|
recovery path itself, which retries the write under an idempotency key.
|
|||
|
|
- So the restriction is on the **shape** of the write, not its existence: the
|
|||
|
|
tool declares how its key derives from its arguments, the kernel derives and
|
|||
|
|
supplies that key on every call, and **a write issued without it is denied**.
|
|||
|
|
- **A tool that cannot derive a stable key cannot be `Idempotent`** — the same
|
|||
|
|
claim as before, now refused at registration rather than discovered after a
|
|||
|
|
double-charge.
|
|||
|
|
|
|||
|
|
```rust
|
|||
|
|
pub enum EffectClass {
|
|||
|
|
Idempotent { key: KeyDerivation },
|
|||
|
|
Queryable { lookup: RequestIdLookup },
|
|||
|
|
Unsafe,
|
|||
|
|
}
|
|||
|
|
```
|
|||
|
|
|
|||
|
|
## Steps
|
|||
|
|
|
|||
|
|
1. Make `KeyDerivation` a required payload on `Idempotent` — a registration
|
|||
|
|
without one must **fail to compile**, not fail at runtime.
|
|||
|
|
2. At call time, derive the key from the recorded arguments and pass it through
|
|||
|
|
the capability handle the tool must use to write. The tool cannot mint its own.
|
|||
|
|
3. Deny any write issued through a handle without the kernel-supplied key.
|
|||
|
|
Denial is at call time, not a post-hoc audit.
|
|||
|
|
4. Record every denial against the tool id, so a misbehaving tool is auditable
|
|||
|
|
rather than merely blocked.
|
|||
|
|
5. Ensure the recovery path (T2.2) re-derives the **same** key from the **same**
|
|||
|
|
recorded arguments — that is what makes the retry safe.
|
|||
|
|
6. Test the duplicate-call case explicitly: two calls with the same derived key
|
|||
|
|
produce one effect.
|
|||
|
|
|
|||
|
|
## Acceptance
|
|||
|
|
|
|||
|
|
- A tool declaring `Idempotent` with a key completes its write and **survives a
|
|||
|
|
duplicate call with no duplicate effect**.
|
|||
|
|
- The same tool writing outside the kernel-supplied key is **denied at call
|
|||
|
|
time**, with the denial **recorded against the tool id** for audit.
|
|||
|
|
- A registration declaring `Idempotent` **without a derivation does not compile**.
|
|||
|
|
|
|||
|
|
## Verify
|
|||
|
|
|
|||
|
|
**Harness:** a test tool writing to the external side-effect ledger, keyed by
|
|||
|
|
whatever key it is given. Plus `trybuild`.
|
|||
|
|
|
|||
|
|
**Integration test** — `tests/it_keyed_capability.rs`:
|
|||
|
|
1. **Compile-fail:** an `Idempotent` registration with no `KeyDerivation`. Assert
|
|||
|
|
the stderr names the missing field.
|
|||
|
|
2. Happy path: the tool completes its write. Assert the ledger holds one entry
|
|||
|
|
under the **kernel-supplied** key.
|
|||
|
|
3. **Duplicate call:** invoke again with the same arguments. Assert the derived
|
|||
|
|
key is identical and the ledger still holds **exactly one** entry.
|
|||
|
|
4. **Out-of-band write:** the same tool attempts a write **not** using the
|
|||
|
|
supplied key. Assert it is **denied at call time**, and that the denial is
|
|||
|
|
**recorded against the tool id** — read the audit record back.
|
|||
|
|
5. **Recovery is a write:** crash mid-call, restart, let T2.2's idempotent
|
|||
|
|
recovery retry. Assert the retry **succeeds** — a blanket write denial would
|
|||
|
|
break exactly this path, and it is the most likely wrong implementation.
|
|||
|
|
6. Determinism: derive the key 100 times from the same recorded arguments; assert
|
|||
|
|
all identical. Derive from arguments containing a timestamp field; assert the
|
|||
|
|
derivation ignores it or the registration is rejected.
|
|||
|
|
7. Assert `Queryable` and `Unsafe` tools are unaffected by this mechanism.
|
|||
|
|
|
|||
|
|
**Command:** `cargo test -p operability keyed_capability && cargo test -p operability --test compile_fail`
|
|||
|
|
|
|||
|
|
**False pass:**
|
|||
|
|
- Implementing this as a blanket write denial for `Idempotent` tools. Steps 1–4
|
|||
|
|
all pass; step 5 is the one that fails, and it is the whole reason the
|
|||
|
|
restriction is on the **shape** of the write rather than its existence.
|
|||
|
|
- Step 3 passing because the ledger deduplicates on content rather than key. Make
|
|||
|
|
the ledger key-only, or the key derivation is never actually exercised.
|
|||
|
|
- Step 4 asserting the denial without asserting the audit record. A denial nobody
|
|||
|
|
can attribute to a tool is not actionable.
|
|||
|
|
|
|||
|
|
## Traps
|
|||
|
|
|
|||
|
|
- Blanket-denying writes to `Idempotent` tools. That denies the recovery path,
|
|||
|
|
which is itself a write.
|
|||
|
|
- A key derived from anything non-deterministic — a timestamp, a counter, a
|
|||
|
|
random id. The retry then writes twice under two keys.
|
|||
|
|
- Logging denials without the tool id, which leaves nothing to act on.
|
|||
|
|
|
|||
|
|
---
|
|||
|
|
|
|||
|
|
Background (not required to do this task):
|
|||
|
|
[rust-agentic-sys.md](../../../rust-agentic-sys.md) §8.4, §13.1, §13.2 ·
|
|||
|
|
[rust-agentic-task.md](../../../rust-agentic-task.md)
|