(tasks) add tasks for harness
This commit is contained in:
@@ -0,0 +1,113 @@
|
||||
# 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)
|
||||
Reference in New Issue
Block a user