[Sequela02]

Stage 10's second slice: accord build writes a pub machine as a TypeScript module, once every obligation is proved and every example passes. The ports (ProviderRetry, opossum) come next.

The module

The reference is conformance/typescript/machine/out/switch.ts. It was written by hand before the generator, and the generator matches it byte for byte.

• export type M = { readonly field: T; … }.
• checkM$(where$, state$) reads the state once. It checks the object, each field's type and range, every invariant, and every helper invariant, then returns that snapshot. Failures throw TypeError or RangeError, naming the field or the invariant.
• An init takes its parameters and returns a state.
• An event or observer takes (state$, params…), runs only on the checked snapshot, checks its parameters and requires, and returns the next state (for an event) without changing the one it was given.
• Generated names end in $, which no Accord name can use. A module whose exported value or type names would collide is refused.
• A machine with any unproved obligation, not_inductive included, isn't written (refused-machine).

Process

• The expected module and a refused case were committed before the generator (5f74f30).
• An independent review found 3 defects. The contract was corrected first (b383518), then the code (f3c626f):
  • The check and the event each read the state, so a getter could pass the check with one value and hand the event another. Reproduced: press returned presses: -4, breaking the invariant.
  • A field named state or where produced a module that wouldn't import.
  • An enum and a machine sharing a name produced a duplicate type.

Verification

• cargo fmt --all --check and cargo clippy --workspace --all-targets --locked -- -D warnings are clean.
• cargo test --workspace --locked with the pinned solvers: 97 passed, 1 ignored. That includes:
  • every TypeScript folder byte for byte, so function-only modules are unchanged;
  • the differential test, which now runs each init, event and observer against the interpreter, including states that break an invariant or helper and must be rejected;
  • Node tests for the getter attack and for fields named state and where.
• The CI step for the E2 materials (score.py --self-test and materials.py) passes, run without a bytecode cache.
• The reviewer's attack, rerun against the generated module: every result uses the checked value.
• Sanity check on the differential test: removing the helper-invariant check made it fail. The author reports this; it wasn't rerun independently.

Not established: no reference covers i64 fields, event parameters that are text or lists, or a decision table nested in an if. tsc wasn't run; Node strips types, and the module is checked for typing only where the existing tests typecheck generated code.

Risk note

Two-way door: TypeScript output is "unstable until the first release" (docs/typescript.md), and nothing is published. Blast radius: accord build for programs with machines; function-only output is unchanged byte for byte. Evidence: the reference module, the differential test, and the review's attacks rerun.

Refs #82