114 lines
4.3 KiB
Markdown
114 lines
4.3 KiB
Markdown
|
# T0.2 — Kernel `AttemptState`
|
|||
|
|
|
|||
|
|
| Field | Value |
|
|||
|
|
|---|---|
|
|||
|
|
| Phase | P0 — Foundations |
|
|||
|
|
| Size | S — under 1 day |
|
|||
|
|
| Status | ✅ Done |
|
|||
|
|
| Flags | — |
|
|||
|
|
| Spec | inlined below |
|
|||
|
|
| Blocks | — |
|
|||
|
|
|
|||
|
|
## Goal
|
|||
|
|
|
|||
|
|
The closed kernel attempt enum and its transition function, matching the
|
|||
|
|
normative transition table arm for arm.
|
|||
|
|
|
|||
|
|
## Facts (inlined — no spec read needed)
|
|||
|
|
|
|||
|
|
```rust
|
|||
|
|
/// Kernel. Closed. Users never extend this.
|
|||
|
|
#[derive(Clone, Copy, PartialEq, Eq)]
|
|||
|
|
pub enum AttemptState {
|
|||
|
|
Pending,
|
|||
|
|
Running,
|
|||
|
|
Succeeded,
|
|||
|
|
Failed,
|
|||
|
|
/// Crashed mid-side-effect; recovery could not determine what happened.
|
|||
|
|
Indeterminate,
|
|||
|
|
/// Stopped by decision, no dispatched intent outstanding.
|
|||
|
|
Cancelled,
|
|||
|
|
TimedOut,
|
|||
|
|
}
|
|||
|
|
```
|
|||
|
|
|
|||
|
|
Normative legal set — the match has exactly these arms and no others:
|
|||
|
|
|
|||
|
|
| From | To | When |
|
|||
|
|
|---|---|---|
|
|||
|
|
| `Pending` | `Running` | admitted |
|
|||
|
|
| `Pending` | `Cancelled` | run cancelled before the attempt started |
|
|||
|
|
| `Pending` | `TimedOut` | queue deadline passed before admission |
|
|||
|
|
| `Running` | `Succeeded` | completed |
|
|||
|
|
| `Running` | `Failed` | completed with an error |
|
|||
|
|
| `Running` | `TimedOut` | step deadline passed |
|
|||
|
|
| `Running` | `Cancelled` | run cancelled, **no intent was `Dispatched`** |
|
|||
|
|
| `Running` | `Indeterminate` | an intent was `Dispatched` and did not resolve |
|
|||
|
|
| terminal | — | nothing leaves a terminal state |
|
|||
|
|
|
|||
|
|
- `Cancelled` and `Indeterminate` are **separate states**. Cancellation is a
|
|||
|
|
decision; indeterminacy is an unknown. The deciding fact is the intent record
|
|||
|
|
(T2.1): no `Dispatched` intent means nothing external happened, so the attempt
|
|||
|
|
is cleanly `Cancelled`.
|
|||
|
|
- Why it matters beyond taxonomy: operations alerts on `Indeterminate` count and
|
|||
|
|
expects near zero. Route ordinary cancellations there and the alert acquires a
|
|||
|
|
noisy floor, which is the same as not having the alert.
|
|||
|
|
- Domain states are the opposite — open, declared by the workflow as data
|
|||
|
|
(`pub struct StepState(SmolStr)`), validated at load. Not this task.
|
|||
|
|
|
|||
|
|
## Steps
|
|||
|
|
|
|||
|
|
1. Declare `AttemptState` exactly as above.
|
|||
|
|
2. Write `fn transition(from: AttemptState, cause: TransitionCause) -> Result<AttemptState, IllegalTransition>`
|
|||
|
|
as an **exhaustive match** — no `_ =>` catch-all, so adding a state becomes a
|
|||
|
|
compile error at this function.
|
|||
|
|
3. Model the `Running → {Cancelled, Indeterminate}` split on an explicit input:
|
|||
|
|
`TransitionCause::Cancel { intent_dispatched: bool }`. Never infer it from the
|
|||
|
|
drop site.
|
|||
|
|
4. Make every terminal state reject all outgoing transitions with
|
|||
|
|
`IllegalTransition`.
|
|||
|
|
5. Property test with `proptest`: enumerate all `(from, to)` pairs, assert the
|
|||
|
|
accepted set equals the table above exactly — reject-set included.
|
|||
|
|
|
|||
|
|
## Acceptance
|
|||
|
|
|
|||
|
|
- Property test over all state pairs: legal set matches the table exactly.
|
|||
|
|
- Targeted test: cancelling an attempt with **no** `Dispatched` intent yields
|
|||
|
|
`Cancelled`; cancelling one **with** a `Dispatched` intent yields
|
|||
|
|
`Indeterminate`.
|
|||
|
|
|
|||
|
|
## Verify
|
|||
|
|
|
|||
|
|
**Harness:** `proptest`, plus a recorded log fixture once P1 exists.
|
|||
|
|
|
|||
|
|
**Integration test** — `tests/it_transition_table.rs`:
|
|||
|
|
1. Build the **cartesian product** of all 7 states × all 7 states, written out by
|
|||
|
|
hand from the table in this file — not generated by the code under test.
|
|||
|
|
2. For each pair, assert accept/reject matches the table.
|
|||
|
|
3. Replay a real recorded run's log (P1 fixture) and feed every observed state
|
|||
|
|
change through `transition`; assert none is rejected. This proves the executor
|
|||
|
|
and the table agree.
|
|||
|
|
4. Two targeted cases: cancel with `intent_dispatched: false` → `Cancelled`;
|
|||
|
|
cancel with `true` → `Indeterminate`.
|
|||
|
|
|
|||
|
|
**Command:** `cargo test -p kernel transition`
|
|||
|
|
|
|||
|
|
**False pass:**
|
|||
|
|
- A property test whose generator produces states **by calling `transition`**.
|
|||
|
|
It then agrees with itself and cannot see a missing arm. The pair list must be
|
|||
|
|
written independently.
|
|||
|
|
- Asserting only the accepted set. The rejected set is half the table, and a
|
|||
|
|
permissive `_ => Ok(to)` passes every accept-only test.
|
|||
|
|
|
|||
|
|
## Traps
|
|||
|
|
|
|||
|
|
- Collapsing `Cancelled` into `Indeterminate` "because the tool might have been
|
|||
|
|
mid-something". That "might" is exactly what the intent record answers.
|
|||
|
|
- A `_ =>` arm. It compiles forever and silently absorbs a new state.
|
|||
|
|
|
|||
|
|
---
|
|||
|
|
|
|||
|
|
Background (not required to do this task):
|
|||
|
|
[rust-agentic-sys.md](../../../rust-agentic-sys.md) §2, §5.1, §15 ·
|
|||
|
|
[rust-agentic-task.md](../../../rust-agentic-task.md)
|