Repository navigation
feat(typestate): check explicit resource state transitions and consumed-state reuse #200
Description
Audited on master at 5630d74ec9cd912d4e2f325349f1943cbc15bcc6. This is a scoped implementation item under #147, based on the typed control/dataflow/effect audit. Proposed syntax below is illustrative unless explicitly marked as a current reproducer.
Gap and evidence
Current state_name values are labels, and fsm_transitions() reconstructs edges from variable dependencies in nlsc/schema.py:181–217. This cannot establish that shipping requires a charged order.
The core document also specifies structural record types. Simply adding a decorative Order<Charged> string or trusting a field named state would not establish a meaningful protocol guarantee.
Minimum deliverable
An opt-in checked protocol for one resource, with explicit state contracts such as:
validate: Order<Pending> -> Order<Validated>,
charge: Order<Validated> -> Order<Charged>,
ship: Order<Charged> -> Order<Shipped>.
This notation is proposed syntax, not currently supported source.
Implementation hints
- Add protocol/state identities to TypeRefs and explicit Transition nodes; distinguish the protocol token from the structurally typed record payload.
- Make protocol tokens unforgeable within checked NLS except through approved constructors/transitions. Define runtime validation/trust at foreign boundaries.
- For transitions representing resource consumption, use affine token tracking or another explicit consumption discipline. Reject reuse through aliases; phantom state labels alone leave the old validated value available for charging again.
- Carry state through branch joins and loops; incompatible paths require an explicit union/match or are rejected.
- Model success and failure post-states explicitly. A payment timeout may leave the external state unknown; it must not automatically restore a reusable pre-charge token.
- Keep existing
[validate]labels as readable step names with no implied typestate contract. - Limit the first release to one-resource transitions. Defer general ownership/borrowing, distributed protocol proofs, and multi-resource transactions.
Acceptance criteria
- The valid Pending → Validated → Charged → Shipped path type-checks.
- Shipping Pending/Validated, fabricating Charged, and reusing a consumed token directly or through an alias are rejected.
- Branch merges and failure paths preserve conservative state information.
- Graph output shows declared transitions and does not invent them from data-use edges.
- Tests use a fake payment/fulfillment adapter and document all trusted foreign assumptions.
- Documentation distinguishes static call-order/consumption guarantees from external exactly-once execution.
Related: #3 and #86. This is a staged language extension, not a claim that existing FSM visualization is broken because it lacks a protocol type system.
Implementation ordering
Integration depends on #195, #196, #197, #198. Add the behavior/diagnostic fixtures before implementation.
Osprey-informed implementation refinements
Keep resource consumption, continuation consumption, and operation replay as separate contracts:
| Contract | Prevents | Does not establish |
|---|---|---|
| This issue's resource typestate/token | Reusing a consumed checked resource state | External exactly-once completion |
| #208's single-shot request continuation | Delivering the same request's answer to its remainder twice | That a gateway was contacted only once |
| #201's replay/idempotency policy | Retrying without an adequate replay contract | That stale aliases carry a valid post-state |
Implementation refinements:
- Retain resource-token identity through operation arguments, supported handler/callback captures, and returned values. Where escape cannot be tracked, reject it in the initial affine subset.
- Consuming a request's continuation must not silently consume, restore, or fabricate the resource token. State changes occur only through the explicit transition contract.
- A handler may make multiple externally permitted attempts before one answer. The resulting typestate must follow the operation's success/failure/post-state contract; a timeout cannot resurrect an already uncertain resource.
- Build on bug(control): check branch outputs, binding mutation, and loop-carried values before emission #196's joins and region exits so aliases captured before a transition cannot become usable after a branch or handler exit.
Additional acceptance cases:
- A stale resource token captured in a supported closure or handler cannot be reused after transition; unsupported escapes are diagnosed.
- One successful resume cannot manufacture a Charged token without a valid transition.
- An ambiguous timeout follows its explicit unknown/reconciliation state even if its request continuation has been closed.
Osprey references: affine resumption checker and two attempts / one receipt fixture. These illustrate continuation consumption, not a ready-made resource ownership or distributed payment proof.
The first one-resource protocol remains independently scoped; handler/callback integration follows the supported forms rather than requiring general ownership or multi-shot effects.
Activity
Mnehmos commentedon Sep 12, 2026
Slice plan (planning pass, 2026-09-13)
Current state:
IROperation.typestateexists as an unpopulated slot;[state]step prefixes are untyped labels;fsm_transitions()invents edges from data dependencies (exactly what this issue rejects); aType<Pending>spelling parses as an opaque unknown TypeRef and silently passes compatibility checks.Slice 1 (checker-only, no emitter changes):
@states Order: Pending, Validated, Charged, Shippeddirective; transitions expressed with<State>tokens on INPUTS/RETURNS (order: Order<Pending>→RETURNS: Order<Validated>). The tree-sitter path needs@states/<State>added to_should_use_regex_canonical_parse, andtype_ref_from_textmust splitBase<State>so emitters never see the angle form.IROperation.typestatevia a newnlsc/typestate.py(mirroringpopulate_failure_sets) — do not render it in_render_operation, so non-adopting files keep identical semantic hashes.check_typestate, called fromcheck_moduleaftercheck_control, modeled on thecontrolflowbranch/join discipline but intersecting token states:ESEM014wrong-state transition,ESEM015consumed-token reuse (direct or aliased),ESEM016fabricated token / undeclared state,ESEM017ambiguous branch join. Fatal in every mode; one resource per module in the first release.emit_fsm_mermaidwhen@statesexists; inferred edges only when nothing is declared.@statesproduce zero new diagnostics (test_fsm.pycorpus stays green).Open dependencies: #197's resource identities may later restate the resource side; the
typestatepayload should stay schema-versioned.Merge pull request #248 from Mnehmos/feat/200-typestate
Mnehmos commentedon Sep 13, 2026
Slice landed (PR #248). Against this issue's acceptance criteria:
@statesdeclares a protocol;Order<State>tokens on INPUTS/RETURNS define transitions. Wrong-state transitions areESEM014(including cross-protocol tokens), and consumed-state reuse isESEM015— directly, through aliases, and across branch joins.ESEM016— undeclared/malformed protocol or state on inputs and results, unlabeled protocol parameters, and protocol-returning transitions without a declared result state (factories included). Branch joins that disagree on a token's state areESEM017rather than silently picking one.Design notes: the checker is opt-in (files without
@statesare unaffected), static-only (it proves the specified transition order and says nothing about external systems — noted in the spec), and annotations emit the base resource type. A type-only protocolRETURNSis a contract thatnlsc cirequires implementing with@literal.Remaining for later slices: multiple resources per module (currently one protocol per module is the practical scope; the checker handles several but multi-token flows between two protocols in one operation are not yet exercised), and handler integration as #207/#208 land.