fsl-design · diff
git:20261017.bf06ebf to git:20261107.deab533
240 added, 133 removed. Audit A to A.
---
name: fsl-design
- description: Write and verify FSL design-layer specs for engineers from an agreed requirements contract. Use for internal state/action design, decomposition, queues/outboxes, compose, refinement mappings to requirements, typestate checks, scenarios-to-testgen handoff, and implementation-conformance planning. Do not use for PM requirements authoring or business process discovery.
+ description: Write and verify FSL design-layer specs for engineers from an agreed requirements contract. Use for internal state/action design, decomposition, queues/outboxes, compose, refinement mappings to requirements (including requirements written with entities, events, rules, decision tables and a glossary), typestate checks, scenarios-to-testgen handoff, and implementation-conformance planning. Do not use for PM requirements authoring or business process discovery.
---
# FSL Design Layer
+ A headerless document is FSL 4; to migrate it, see the migration guide in `docs/manual/LANGUAGE.md` ("FSL 4 to FSL 5 migration").
+
Use this skill after a requirements contract exists or the user explicitly asks
- for engineering design. The design layer is an ordinary kernel `spec` plus an
- optional refinement mapping back to the requirements layer. That mapping is the
- **refinement seam, not a plain baton pass**: the design must refine the (frozen)
- requirements contract, and `fslc refine` verifies the seam. When a seam breaks,
- repair the design or the mapping — not the upper contract, unless a human revises it.
+ for engineering design. The design layer is an ordinary kernel `spec` headed
+ `fsl 5`, plus a refinement mapping back to the requirements layer. That mapping
+ is the **refinement seam, not a plain baton pass**: the design must refine the
+ (frozen) requirements contract, and `fslc refine` verifies the seam. When a
+ seam breaks, repair the design or the mapping — not the upper contract, unless
+ a human revises it.
- Before writing syntax, read `../fsl/SKILL.md`, then use its reference index to
- load only the needed language and verifier detail. The main pattern: a kernel
- `spec` that declares `entity`/`number` domains (sizes in `verify`), tags each
- action and invariant with `@requirement(...)`, and adds internal detail the
- requirements do not have (review substages, payment submit/confirm, an outbox);
- plus a `refinement` file that maps it back — `map claim_stage[c: Claim] = if
- design[c].st == DesignAutoReview then Submitted else ...` collapses internal
- stages onto the requirements stage, `action pay_submit(c) -> pay(c)` names the
- visible step, and `action pay_confirm(c) -> stutter` hides an internal one.
- Refinement syntax is in `../fsl/references/syntax.md`; the seam rules are in
- `../fsl/references/layers.md`. Use
- `fsl-design-review` instead when the user asks for a design review, SOLID
- judgment, substitutability, or variant comparison.
+ Kernel syntax (state, init, actions, properties, `struct`, `Map`, `Seq`,
+ `compose`) is in `../fsl/references/syntax.md`; the refinement file and the
+ seam rules are in `../fsl/references/syntax.md` and
+ `../fsl/references/layers.md`. Use `fsl-design-review` instead when the user
+ asks for a design review, SOLID judgment, substitutability, or variant
+ comparison.
+ ## What the `fsl 5` header changes here
+
+ - The kernel language is the same. The stricter rules of the edition are
+ errors: `check` answers `result: "error"`, `kind: "unsupported_in_edition"`
+ with `findings[]` (for example `legacy_string_metadata` for an action
+ string `"REQ-1: text"`: write `@requirement("REQ-1", "text")` on the line
+ before the declaration). `fslc migrate --edition 5 file.fsl` plans the
+ edits and the header; `--write` applies them.
+ - A requirements spec of this edition is written in entities, events, rules
+ and decision tables, but **the design refines its lowered kernel**, not its
+ surface. The mapping names the lowered state and actions.
+ - The glossary is not read in a design spec or a refinement file. Write both
+ in canonical (ASCII) names; a requirements spec written in Japanese has the
+ same lowered names as its English spelling, and the same mapping refines
+ either.
+
+ ## Reading the upper contract
+
+ Run `fslc explain --readable requirements.fsl` (with a glossary, add
+ `--names canonical`). Its "State" and "Actions" sections are what you map:
+
+ | Requirements surface | Lowered name the mapping uses |
+ |---|---|
+ | `entity Return { amount: … }` | `return_amount: Map<Return, Amount>` |
+ | its `lifecycle` lines | `return_stage: Map<Return, ReturnStage>`; the enum's members are the stages, in order of first appearance |
+ | `event request = Customer requests Return with amount Draft -> Requested` | action `request(r: Return, amount: Amount)`: the instance first, then the inputs |
+ | `Order belongs to User as buyer via place` | `order_buyer: Map<Order, Option<User>>`; `place` gets the `User` instance as its second parameter |
+ | `P only after Q` | a history field `order_did_<events of Q>` |
+ | `resource stock: Qty` | `stock` |
+ | `allow` / `never` / a decision row | an extra `requires` on the event's action |
+ | `always` / `enters` / `assuming` | an invariant or transition property |
+
+ With an origin-aware `fslc`, `fslc explain --readable` also prints after each
+ `requires` where it came from (`← move Draft -> Requested`, `← decide REQ-… row
+ 1: …`, `← rule REQ-… allow …`), and `fslc explain --lowering` gives the same as
+ JSON. Read them to see which rule or decision row a refinement failure on that
+ action is about (`../fsl-verify/SKILL.md`, the origin self-check).
+
+ ## Example
+
+ The design below refines the requirements example of
+ `../fsl-requirements/SKILL.md`: requests split by amount into two review
+ queues, and the refund is a two-step exchange with a payment provider.
+
+ ```fsl check
+ fsl 5
+ spec ReturnDesign {
+ entity Return
+ number Amount
+ const AUTO_LIMIT = 1
+
+ enum Phase { Drafting, AutoReview, ManagerReview, Cleared, Declined, RefundSent, RefundDone }
+ struct Case { phase: Phase, amount: Amount }
+
+ state {
+ cases: Map<Return, Case>
+ }
+ init {
+ forall r: Return { cases[r] = Case { phase: Drafting, amount: 0 } }
+ }
+
+ @requirement("REQ-RET-003", "a small return goes to automatic review")
+ fair action request_small(r: Return, a: Amount) {
+ requires cases[r].phase == Drafting
+ requires a > 0
+ requires a <= AUTO_LIMIT
+ cases[r] = Case { phase: AutoReview, amount: a }
+ }
+
+ @requirement("REQ-RET-004", "a large return goes to manager review")
+ fair action request_large(r: Return, a: Amount) {
+ requires cases[r].phase == Drafting
+ requires a > AUTO_LIMIT
+ cases[r] = Case { phase: ManagerReview, amount: a }
+ }
+
+ @requirement("REQ-RET-003", "the system approves a return in automatic review")
+ fair action auto_approve(r: Return) {
+ requires cases[r].phase == AutoReview
+ cases[r].phase = Cleared
+ }
+
+ @requirement("REQ-RET-004", "a manager approves a return in manager review")
+ fair action mgr_approve(r: Return) {
+ requires cases[r].phase == ManagerReview
+ cases[r].phase = Cleared
+ }
+
+ @requirement("REQ-RET-004", "a manager rejects a return in manager review")
+ fair action mgr_reject(r: Return) {
+ requires cases[r].phase == ManagerReview
+ cases[r].phase = Declined
+ }
+
+ @requirement("MODEL-RET-001", "the refund is sent to the payment provider")
+ fair action refund_send(r: Return) {
+ requires cases[r].phase == Cleared
+ cases[r].phase = RefundSent
+ }
+
+ @requirement("MODEL-RET-002", "the payment provider confirms the refund")
+ fair action refund_confirm(r: Return) {
+ requires cases[r].phase == RefundSent
+ cases[r].phase = RefundDone
+ }
+
+ @requirement("REQ-RET-002", "only a small return is in automatic review")
+ invariant AutoReviewIsSmall {
+ forall r: Return { cases[r].phase == AutoReview => cases[r].amount <= AUTO_LIMIT }
+ }
+
+ @requirement("REQ-RET-005", "a requested return keeps a positive amount")
+ invariant AmountPositive {
+ forall r: Return { cases[r].phase != Drafting => cases[r].amount > 0 }
+ }
+
+ terminal { forall r: Return { cases[r].phase == RefundDone or cases[r].phase == Declined } }
+ }
+
+ verify {
+ instances Return = 2
+ values Amount = 0..3
+ }
+ ```
+
+ The mapping (a refinement file of its own, so shown as a fragment):
+
+ ```fsl-fragment
+ fsl 5
+ refinement ReturnDesignRefinesRequirements {
+ impl ReturnDesign
+ abs ReturnRequirements
+
+ map return_stage[r: Return] =
+ if cases[r].phase == Drafting then Draft
+ else if cases[r].phase == AutoReview then Requested
+ else if cases[r].phase == ManagerReview then Requested
+ else if cases[r].phase == Cleared then Approved
+ else if cases[r].phase == Declined then Rejected
+ else Refunded
+ map return_amount[r: Return] = cases[r].amount
+
+ action request_small(r, a) -> request(r, a)
+ action request_large(r, a) -> request(r, a)
+ action auto_approve(r) -> auto_approve(r)
+ action mgr_approve(r) -> mgr_approve(r)
+ action mgr_reject(r) -> reject(r)
+ action refund_send(r) -> refund(r)
+ action refund_confirm(r) -> stutter
+ }
+ ```
+
+ `fslc refine design.fsl requirements.fsl mapping.fsl` returns `refines`
+ (depth 8), against the English requirements spec and against its Japanese
+ spelling alike. Removing `requires a <= AUTO_LIMIT` from `request_small` (and
+ the invariant that notices it) makes it `refinement_failed`,
+ `abs_requires_failed` on `auto_approve`: the design would approve a large
+ return automatically, which the upper decision table forbids.
+
+ - Name the design's own enum members apart from the upper stage names
+ (`Drafting`, not `Draft`): a mapping that sees a member in two enums is an
+ error (`ambiguous enum member`).
+ - `refine` carries safety. An upper `policy` / `leadsTo` is checked through the
+ mapping only with `preserve progress { respond … by … }`; otherwise verify
+ progress in the design itself.
+ - Tag each design declaration with the requirement it realizes:
+ `@requirement("REQ-RET-003", "…")` with the upper spec's rule, decision
+ table or row ID; `MODEL-` / `ASSUME-` for a design choice the requirements
+ do not state.
+
## Boundary
Produce design-layer artifacts only:
- A kernel `spec` for internal design state and actions
- - A refinement mapping from design to requirements when a stable requirement spec
- exists
+ - A refinement mapping from design to requirements when a stable requirement
+ spec exists
- Verification/refinement commands and result interpretation
- Optional `testgen`, `replay`, or `typestate` handoff plan
- Do not rewrite business policies or PM requirements to make the design pass. If
- the upper contract is too strict or ambiguous, report the counterexample and ask
- for a contract decision.
+ Do not rewrite business policies or PM requirements to make the design pass.
+ If the upper contract is too strict or ambiguous, report the counterexample and
+ ask for a contract decision.
## Workflow
- 1. Confirm the upper contract:
- - the requirements/business file that must remain stable
- - externally observable state and actions
- - which internal actions correspond to upper actions and which are true stutters
- - open/closed boundaries and human-owned design judgments
- 2. Write the design spec as kernel FSL. It may include internal states, queues,
- outboxes, two-phase operations, retries, and decomposition that are absent from
- requirements, as long as they map back to the upper contract.
- Write the design so that the errors you want caught break something the
- verifier checks. `fslc verify` and `fslc refine` report a design error
- when it breaks something they evaluate, within the depth and domain sizes
- of the run. For `fslc verify` that includes declared properties
- (`invariant`, `trans`, `leadsTo`, `ensures`, `reachable`) and automatic
- checks (type bounds, partial operations, deadlock detection); `fslc refine`
- adds the correspondence to the upper contract. `acceptance` and `forbidden`
- scenarios belong to the requirements layer — a kernel `spec` that declares
- them is a parse error. They run when the requirements spec is checked; the
- design reaches that contract through `refine`, which carries safety only and
- does not replay an acceptance trace on the design. This list is
- illustrative, not complete:
- `../fsl/references/commands.md` is the reference for what each command
- checks and returns. An error that breaks nothing they evaluate is not
- reported, so an intent that no declaration states is checked only where
- an automatic check happens to cover it. A run that reports no violation
- has not thereby passed: `unknown_cti` and `unknown_budget` mean the check
- did not decide. So list the failures this design must exclude — for
- example: processed twice, lost, out of order, inconsistent after a crash,
- wrong on retry, interleaved in the middle of a multi-step procedure, a
- quantity not conserved — and for each one declare the property it would
- break, using the construct that fits that property (see
- `../fsl/references/nl-to-syntax.md`). The fit depends on what is meant:
- "not lost" can be a safety property (the item is always held somewhere) or
- a progress property (the item is eventually delivered), and the two are
- written differently. If neither the source nor the upper contract states
- the property, ask; do not invent it. Where the design has the following
- mechanisms, model them as state and actions rather than folding them into
- one step or leaving them in a comment (the order is not a ranking):
- - **Transaction boundaries**: one `action` per step the implementation
- performs atomically, with what must hold between those steps declared as
- properties.
- - **Queues and outboxes**: the queue held in `state`, with what the
- contract requires of it declared as properties (for example: nothing is
- lost, nothing is duplicated, only the head is processed).
- - **Retries and idempotency**: for example an unknown outcome, the
- idempotency key, and a release that is separate from its acknowledgement.
- 3. Link every design declaration back to the requirement it serves with the
- canonical typed annotation, on the line before the declaration:
- `@requirement("REQ-CHECKOUT-001", "one-sentence intent")` before
- `invariant PaidLedger { ... }` / `action submit(...) { ... }`. The
- requirements spec owns the ID (`requirement REQ-CHECKOUT-001`); the design
- spec only links to it. Use a `MODEL-`/`ASSUME-`prefixed id for a design
- choice the requirements do not state. **Never use the `"REQ-1: text"` string
- slot** — it is non-canonical migration input and `fslc lint` reports it as
- `legacy_string_metadata`.
- 4. Verify the design itself with `fslc check`, `fslc lint <file>`, `fslc verify`,
- and usually `fslc verify --engine induction`. `fslc lint` is the tagging
- gate: it exits 1 on any non-canonical ID form, which `--strict-tags` accepts
- silently; the design is not done until it reports no findings. For
- traceability, add `fslc check <file> --strict-tags --requirements ids.txt`
- (a file with one requirement ID per line, not a comma list).
- A bounded `verified` says nothing past the depth and the domain sizes it
- ran at, and a design with many interleavings can hold its first violation
- beyond the default depth. For properties about interactions between
- entities, see "Domain sizing" in `../fsl/references/practices.md`: a result
- at a smaller size, even a closed `proved`, does not cover a larger one.
- What to do with `unknown_cti` / `unknown_budget`, how to repair, and the
- completion report format are in `../fsl-verify/SKILL.md`.
- 5. Write the mapping file:
- - `map abs_var = expr` or `map abs_var[x: T] = expr`
- - `action impl_action(...) -> abs_action(...)` for visible effects
- - `action impl_action(...) -> stutter` only when the action is confirmed not to
- change abstract observable state
- - `preserve progress { respond AbsLeadsTo by impl_action, ... }` when an
- upper `leadsTo` must be checked through the mapping at refine time
- 6. Run `fslc refine design.fsl requirements.fsl mapping.fsl`. Repair by deciding
- whether the design is wrong, the mapping is wrong, or the upper contract needs
- human revision.
+ 1. Confirm the upper contract: the requirements/business file that must remain
+ stable, its lowered state and actions (above), which design actions
+ correspond to which upper actions and which are true stutters, and the
+ human-owned design judgments.
+ 2. Write the design spec as kernel FSL headed `fsl 5`. It may include internal
+ states, queues, outboxes, two-phase operations, retries, and decomposition
+ absent from the requirements, as long as they map back. List the failures
+ the design must exclude (processed twice, lost, out of order, inconsistent
+ after a crash, wrong on retry, interleaved in the middle of a multi-step
+ procedure, a quantity not conserved) and declare for each the property it
+ would break (`../fsl/references/nl-to-syntax.md`); if neither the source nor
+ the upper contract states the property, ask. Model transaction boundaries,
+ queues/outboxes, and retries/idempotency as state and actions, not as one
+ step or a comment. `acceptance` / `forbidden` belong to the requirements
+ layer; a kernel `spec` that declares them is a parse error.
+ 3. Tag every action and invariant with `@requirement("ID", "intent")`.
+ 4. Verify the design itself: `fslc check`, `fslc lint <file>` (no findings),
+ `fslc verify --depth 8`, `fslc verify --engine induction`; for
+ traceability `fslc check <file> --strict-tags --requirements ids.txt`.
+ A bounded `verified` says nothing past its depth and domain sizes.
+ 5. Write the mapping file: `map abs_var[x: T] = expr` for every lowered state
+ variable of the upper spec, `action impl(...) -> abs(...)` for visible
+ effects, `action impl(...) -> stutter` only when the action changes no
+ mapped state, and `preserve progress { respond AbsLeadsTo by impl_action }`
+ when an upper progress property must hold through the mapping.
+ 6. Run `fslc refine design.fsl requirements.fsl mapping.fsl`. Repair by
+ deciding whether the design is wrong, the mapping is wrong, or the upper
+ contract needs human revision.
7. If implementation anchoring is required, run `fslc testgen` and wire the
- Adapter, or use `fslc replay` against execution logs.
- Generated tests and conformance vectors are sequences of design actions
- and do not enumerate interleaving or crash points inside one; where the
- design declares a procedure atomic, plan implementation tests that
- interleave or crash inside it (see `../fsl/references/impl.md` §9).
+ Adapter, or use `fslc replay` against execution logs. Generated tests do not
+ enumerate interleavings or crash points inside one action; plan
+ implementation tests for those (`../fsl/references/impl.md` §9).
## Guardrails
- - Treat `abs_requires_failed` as a design bypass of an upper guard until proven
- otherwise.
+ - Treat `abs_requires_failed` as a design bypass of an upper guard — an
+ `allow` / `never` rule or a decision row — until proven otherwise; the
+ origin of that `requires` names which.
- Treat `stutter_changed_abs` as a false claim of internal-only behavior.
- - Treat `progress_lost` as a lower-layer liveness failure: inspect the lasso/stall
- trace, then add/restore `fair` on the lower progress action or write a
- lower-layer ranked `leadsTo`.
- - Do not model variants by editing the abstract spec each time; keep variant detail
- in the design layer and fold it through the mapping.
- - When you change an existing design spec, re-run `fslc verify` on the changed
- design and `fslc refine` against the unchanged requirements, and, when the
- old and new design share state and action names, also run
- `fslc diff old_design.fsl new_design.fsl --forbid behavior_removed,unknown`
- (add the other kinds your change policy rejects; see `../fsl-verify/SKILL.md`).
- `refine` passes a change that only makes the design refuse more (a
- strengthened guard); `diff` reports it as `behavior_removed`. Decide whether
- that refusal is intended before accepting or reverting the change (see
- `../fsl-design-review/SKILL.md`, Step 3). These checks are bounded by their
- depth: a violation that first appears beyond the checked depth is not
- reported. An `unknown` finding or an `unknown_budget` result from `diff` is
- undecided; do not read it as "no behavior removed".
+ - Treat `progress_lost` as a lower-layer liveness failure: inspect the
+ lasso/stall trace, then add/restore `fair` on the lower progress action or
+ write a lower-layer ranked `leadsTo`.
+ - Do not model variants by editing the abstract spec each time; keep variant
+ detail in the design layer and fold it through the mapping.
+ - When you change an existing design spec, re-run `fslc verify` on it and
+ `fslc refine` against the unchanged requirements, and, when old and new
+ share state and action names, `fslc diff old.fsl new.fsl --forbid
+ behavior_removed,unknown` (plus the kinds your change policy rejects;
+ `../fsl-verify/SKILL.md`). `refine` passes a change that only makes the
+ design refuse more; `diff` reports it as `behavior_removed`.
- Report proof categories separately: design invariants proved, refinement to
- requirements proved, implementation conformance not yet proved unless `testgen`
- or `replay` has been anchored to real code/logs.
- - Author the design spec as documentation: declare domains with `entity`/`number`
- (sizes in the `verify` block, not in `type X = 0..N`), tag every action/invariant
- with `@requirement("ID", "intent")` as in step 3 (prefix verification-only
- invariants `MODEL-`/`ASSUME-`), and
- prefer `forall x in coll { … }` over index quantifiers in invariant bodies. See
- `../fsl/references/layers.md` → "Authoring specs as readable documentation".
+ requirements proved, implementation conformance not yet proved unless
+ `testgen` or `replay` has been anchored to real code/logs.
+ - Author the design spec as documentation: declare domains with `entity` /
+ `number` (sizes in `verify`), tag every action/invariant, and prefer
+ `forall x in coll { … }` over index quantifiers in invariant bodies.