88 lines
4.7 KiB
Markdown
88 lines
4.7 KiB
Markdown
---
|
|
description: Break the implementation plan into ordered tasks
|
|
allowed-tools: [Read, Write, Edit, Glob, Grep]
|
|
---
|
|
|
|
# FormSpec Tasks
|
|
|
|
You are breaking the implementation plan into concrete, dependency-ordered tasks that can be executed one at a time.
|
|
|
|
## Steps
|
|
|
|
### 1. Read artifacts
|
|
|
|
Read:
|
|
- `spec/plan.md` (must exist — if not, direct user to `/formspec.plan.4`)
|
|
- `spec/formal/traceability.md`
|
|
- All feature design docs: Glob for `spec/features/*/design.md`
|
|
|
|
### 2. Generate spec/tasks.md
|
|
|
|
Write `spec/tasks.md` with two sections: implementation tasks and verification milestones.
|
|
|
|
Implementation tasks are fine-grained and component-oriented — they track what code to write. Verification milestones are coarser and property-oriented — they define when a TLA+ property can actually be validated end-to-end. This separation exists because the implementation architecture is more fine-grained than the specification: a single formal property (e.g., crash safety) typically spans multiple implementation components (persistence layer + coordinator + integration tests), so no single task is a meaningful checkpoint for validating it.
|
|
|
|
#### Task format
|
|
|
|
```markdown
|
|
# Implementation Tasks
|
|
|
|
## Task T-01: [Title]
|
|
**Depends on**: (none | T-XX, T-YY)
|
|
**Implements**: US-3, SC-1 (from 2026-02-10-user-auth)
|
|
**Description**: [What to implement — specific enough that the implementer knows exactly what code to write]
|
|
**Acceptance**: [Unit-level criteria — how to verify this component works in isolation. Must be objectively verifiable. These are TDD checkpoints, not TLA+ property verification.]
|
|
```
|
|
|
|
Tasks do NOT have a "Verifies" field for TLA+ properties. Individual tasks verify their own component contracts through unit tests; TLA+ properties are verified at the milestone level.
|
|
|
|
#### Milestone format
|
|
|
|
After the tasks, add a milestones section:
|
|
|
|
```markdown
|
|
# Verification Milestones
|
|
|
|
## Milestone M-01: [TLA+ Property or property group]
|
|
**Tasks**: T-02, T-04, T-05, T-08
|
|
**Verifies**: PersistBeforeGrant, EventualRecovery (from System.tla)
|
|
**Verification method**: `go test -race -run Recovery ./coordinator/...`
|
|
**Description**: [What this milestone validates and why it requires all the listed tasks to be complete first]
|
|
```
|
|
|
|
A milestone gates on a set of tasks. Only after all of its tasks are complete can the verification method be run and the result recorded in the verification matrix. A single task may appear in multiple milestones. A single milestone may verify multiple related properties.
|
|
|
|
### 3. Coverage requirements
|
|
|
|
**Tasks** must collectively cover:
|
|
- **All user stories** from all feature design docs (every US-N must appear in at least one task's "Implements" field)
|
|
- **All implementation components** from the plan's architecture
|
|
- **F* proof modules** if included in the plan
|
|
- **Infrastructure setup** tasks (project scaffolding, CI configuration, test harness) where needed
|
|
|
|
**Milestones** must collectively cover:
|
|
- **Every TLA+ property** from traceability.md that has a runtime or integration-level verification method
|
|
- **Every verification method** from the plan's Verification Strategy table
|
|
- Properties verified by structural or compile-time guarantees do not need milestones — they are validated by the data model or type system, not by test execution
|
|
|
|
### 4. Dependency ordering rules
|
|
|
|
- Foundational types, interfaces, and data models before business logic
|
|
- Verification infrastructure (test harness, F* module structure) before verification tasks
|
|
- Core functionality before features that depend on it
|
|
- No circular dependencies
|
|
- Tasks should be small enough to implement in a single session but large enough to be meaningful (not "create a file" granularity)
|
|
- Each task should be independently testable with unit tests after its dependencies are met — if a task can only be tested as part of a larger integration, it should be merged with the tasks it depends on or the milestone structure should be reconsidered
|
|
|
|
### 5. Validation
|
|
|
|
Before finishing, check:
|
|
- Every US-N from every feature design doc is covered by at least one task
|
|
- Every TLA+ property from traceability.md with a runtime verification method is covered by at least one milestone
|
|
- Every milestone's task list references valid task IDs
|
|
- Every task's dependencies reference valid task IDs
|
|
- No circular dependency chains exist in the task graph
|
|
- The dependency graph has a valid topological ordering
|
|
- Every milestone's tasks collectively provide the components needed to execute its verification method (e.g., a milestone that verifies crash recovery must include tasks for persistence, the coordinator, and the recovery integration test)
|
|
|
|
Report any gaps found during validation. Suggest proceeding with `/formspec.implement.6` to start implementing tasks.
|