[Sequela02]

Stage 10's first slice: Accord now checks machine declarations, as #82's decisions and docs/design/syntax.md ("Machines", decision 7) describe. TypeScript output for machines and the ports come next.

What it does

• Parses and checks machines. That covers state, init, event, observers, invariant and helper invariant, and next { … } bodies through if or decide. Sequence examples use example M … gives.
  • It rejects: a missing or unknown field, a field set twice, a parameter named like a field, next used as a name, an event with ensures, an invariant that calls a function, a machine with no init, and two invariants with one name.
• Obligations, through the existing machinery. Each init and event becomes a function with the fields as parameters, so types, SMT terms, overflow, decision tables and contracts are reused.
  • New: an init meets every invariant; an event preserves them; an event is allowed in some state an init reaches.
  • Invariants and helpers are proved assuming the arithmetic they evaluate stays in its type, which is an obligation of its own.
• Explorer. It runs breadth-first from every init and enumerates only finite domains: Bool, enum, or integers pinned to literals or to a literal range of at most 1,024 values, clamped to their type. It caps at 100,000 states and 2,000,000 steps.
  • Every trace is replayed by the interpreter before it counts.
  • An invariant is refuted only by such a trace.
  • A solver refutation without one is the new outcome not_inductive, carrying the state the solvers found. It makes standing incomplete, not failed, and has code ACC0015, add_helper_invariant.
  • Exploration coverage is an annotation on the obligation, never an outcome.
• Receipt version 4: not_inductive, trace refutations, exploration annotations, helper invariants as support, and typed inputs for every parameter.
• accord build and accord diff refuse machines for now.

Process

• The 21 machine* cases were committed before their code (cce0d9d and cbddd1b) and none of their expected lines changed. Two cases renamed a field from count to value, because count is a quantifier keyword.
• An independent review found 4 defects plus 2 minor ones. Each got a case first, then a fix (20240a7):
  • an argument outside its type proved an event "allowed";
  • an overflowing step refuted an invariant it never broke;
  • diff reported a machine's lost invariants as kept;
  • the hash ignored member roles and helper flags;
  • duplicate invariant names were accepted;
  • stale reused flags.

Verification

• cargo fmt --all --check and cargo clippy --workspace --all-targets --locked -- -D warnings are clean.
• cargo test --workspace --locked with the pinned solvers: 93 passed, 1 ignored (the existing solver-timeout helper). That includes all 21 machine cases and 6 tests in tests/machines.rs.
• No regression for functions: I built main (70a624d) and this branch, and ran all 120 non-machine cases through both. Definition hashes and every outcome are identical: 507 obligations and examples, and every standing. The only difference is the receipt version (3 to 4).

Not established:

• the 100,000-state and 2,000,000-step caps, which no test reaches;
• a machine in a multi-file folder;
• the ProviderRetry and opossum ports, which are the next slices.

Risk note

One-way-ish for the receipt format: version 4 adds an outcome, and consumers that match outcomes exhaustively must handle not_inductive. Nothing is published yet, so this is still reversible. The function path is unchanged, as shown above. Blast radius: the checker and receipt for programs that declare machines. Evidence: the conformance cases, the review's reproductions now passing, and the base comparison.

Refs #82