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)
|