From 5f74f30b29cff32c5a9fd2c59525aa7e809aacbe Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 21:23:11 -0700
Subject: [PATCH 1/6] test: write a machine's TypeScript module before its
 generator

The TypeScript conformance folders hold the modules accord build must
write, byte for byte, written before the generator. This one fixes how a
machine crosses the boundary: a readonly state type, one check of the
state's fields, invariants and helper invariants for every event and
observer, and events that return the next state. A machine whose
invariant isn't proved inductive must be refused.

Refs #82
---
 conformance/typescript/machine/out/switch.ts  | 100 ++++++++++++++++++
 .../typescript/machine/src/switch.accord      |  47 ++++++++
 .../refused-machine/src/pair.accord           |  18 ++++
 3 files changed, 165 insertions(+)
 create mode 100644 conformance/typescript/machine/out/switch.ts
 create mode 100644 conformance/typescript/machine/src/switch.accord
 create mode 100644 conformance/typescript/refused-machine/src/pair.accord

diff --git a/conformance/typescript/machine/out/switch.ts b/conformance/typescript/machine/out/switch.ts
new file mode 100644
index 0000000..9346e25
--- /dev/null
+++ b/conformance/typescript/machine/out/switch.ts
@@ -0,0 +1,100 @@
+// Generated by accord from switch.accord. Do not edit.
+// Every obligation of these functions is proved. This TypeScript is not
+// proved equivalent to them: Accord tests its code generator against its
+// interpreter.
+// Each exported function checks its parameters and its `requires`, and
+// throws a TypeError or a RangeError when one doesn't hold.
+// A machine's events and observers also check that the state they are given
+// has its fields and meets every invariant and helper invariant. An event
+// returns the next state and leaves the one it is given unchanged.
+
+export type Light = "off" | "on";
+
+export type Switch = {
+  readonly light: Light;
+  readonly presses: number;
+};
+
+function checkSwitch$(where: string, state: Switch): void {
+  if (typeof state !== "object" || state === null) {
+    throw new TypeError(`${where}: state must be a Switch`);
+  }
+  const { light, presses } = state;
+  if (!["off", "on"].includes(light)) {
+    throw new TypeError(`${where}: state.light must be a Light`);
+  }
+  if (typeof presses !== "number") {
+    throw new TypeError(`${where}: state.presses must be an i32`);
+  }
+  if (!Number.isInteger(presses) || presses < -2147483648 || presses > 2147483647) {
+    throw new RangeError(`${where}: state.presses must be an i32`);
+  }
+  if (!((BigInt(presses) >= 0n) && (BigInt(presses) <= 100n))) {
+    throw new RangeError(`${where}: state breaks invariant pressed: presses >= 0 and presses <= 100`);
+  }
+  if (!(!(light === "on") || (BigInt(presses) > 0n))) {
+    throw new RangeError(`${where}: state breaks helper invariant on_means_pressed: light == On implies presses > 0`);
+  }
+}
+
+export function start(): Switch {
+  return start$();
+}
+
+function start$(): Switch {
+  return { light: "off", presses: 0 };
+}
+
+export function resume(fromLight: Light, fromPresses: number): Switch {
+  if (!["off", "on"].includes(fromLight)) {
+    throw new TypeError("resume: fromLight must be a Light");
+  }
+  if (typeof fromPresses !== "number") {
+    throw new TypeError("resume: fromPresses must be an i32");
+  }
+  if (!Number.isInteger(fromPresses) || fromPresses < -2147483648 || fromPresses > 2147483647) {
+    throw new RangeError("resume: fromPresses must be an i32");
+  }
+  if (!(((BigInt(fromPresses) >= 0n) && (BigInt(fromPresses) <= 100n)) && ((fromLight === "off") || (BigInt(fromPresses) > 0n)))) {
+    throw new RangeError("resume: requires from_presses >= 0 and from_presses <= 100 and (from_light == Off or from_presses > 0)");
+  }
+  return resume$(fromLight, fromPresses);
+}
+
+function resume$(fromLight: Light, fromPresses: number): Switch {
+  return { light: fromLight, presses: fromPresses };
+}
+
+export function press(state: Switch): Switch {
+  checkSwitch$("press", state);
+  const { light, presses } = state;
+  if (!(BigInt(presses) < 100n)) {
+    throw new RangeError("press: requires presses < 100");
+  }
+  return press$(light, presses);
+}
+
+function press$(light: Light, presses: number): Switch {
+  if (light === "off") return { light: "on", presses: presses + 1 };
+  return { light: "off", presses: presses + 1 };
+}
+
+export function turnOff(state: Switch): Switch {
+  checkSwitch$("turnOff", state);
+  const { light, presses } = state;
+  return turnOff$(light, presses);
+}
+
+function turnOff$(light: Light, presses: number): Switch {
+  return { light: "off", presses: presses };
+}
+
+export function atLimit(state: Switch): boolean {
+  checkSwitch$("atLimit", state);
+  const { light, presses } = state;
+  return atLimit$(light, presses);
+}
+
+function atLimit$(light: Light, presses: number): boolean {
+  return presses === 100;
+}
diff --git a/conformance/typescript/machine/src/switch.accord b/conformance/typescript/machine/src/switch.accord
new file mode 100644
index 0000000..c31c2e5
--- /dev/null
+++ b/conformance/typescript/machine/src/switch.accord
@@ -0,0 +1,47 @@
+/// Whether the light is on.
+pub enum Light { Off, On }
+
+/// A switch that counts its presses.
+pub machine Switch {
+    state {
+        light: Light,
+        presses: i32,
+    }
+
+    init start() {
+        next { light: Off, presses: 0 }
+    }
+
+    init resume(from_light: Light, from_presses: i32)
+        requires from_presses >= 0 and from_presses <= 100 and (from_light == Off or from_presses > 0)
+    {
+        next { light: from_light, presses: from_presses }
+    }
+
+    event press()
+        requires presses < 100
+    decide {
+        | light == Off => next { light: On, presses: presses + 1 }
+        | otherwise    => next { light: Off, presses: presses + 1 }
+    }
+
+    event turn_off() {
+        next { light: Off }
+    }
+
+    /// Whether the switch has reached its limit.
+    fn at_limit() -> Bool
+        ensures result implies presses == 100
+    {
+        presses == 100
+    }
+
+    invariant pressed: presses >= 0 and presses <= 100
+
+    helper invariant on_means_pressed: light == On implies presses > 0
+}
+
+example Switch
+    start()
+    press()
+    gives light == On and presses == 1
diff --git a/conformance/typescript/refused-machine/src/pair.accord b/conformance/typescript/refused-machine/src/pair.accord
new file mode 100644
index 0000000..5f0ca73
--- /dev/null
+++ b/conformance/typescript/refused-machine/src/pair.accord
@@ -0,0 +1,18 @@
+pub machine Pair {
+    state {
+        x: i32,
+        y: i32,
+    }
+
+    init start() {
+        next { x: 0, y: 0 }
+    }
+
+    event step()
+        requires x < 3
+    {
+        next { x: x + 1, y: y + 1 }
+    }
+
+    invariant y_bounded: y <= 3
+}

From 5df5f1ef9cd8492bbf4528cc5b70cc3b47ddcffc Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 21:35:36 -0700
Subject: [PATCH 2/6] feat: write a pub machine as TypeScript

A pub machine becomes a state type, a check of a state's fields and
every invariant and helper invariant, and an exported function for each
init, event and observer; the generator reuses the functions' parameter
and requires checks, expressions and decision tables. Build writes it
only when every obligation is proved, and refuses a module whose names
would collide. The differential test runs each member against the
interpreter, including states that break an invariant, which the module
must reject.

Refs #82
---
 crates/accord/src/evidence/machine.rs         |  12 +-
 crates/accord/src/syntax.rs                   |  13 ++
 crates/accord/src/typescript.rs               | 218 ++++++++++++++++--
 crates/accord/src/typescript/boundary.rs      | 190 +++++++++++++--
 crates/accord/src/typescript/differential.rs  | 105 ++++++++-
 .../src/typescript/differential/inputs.rs     |  67 +++++-
 crates/accord/src/typescript/expr.rs          |   4 +-
 crates/accord/tests/machines.rs               |  38 ++-
 8 files changed, 588 insertions(+), 59 deletions(-)

diff --git a/crates/accord/src/evidence/machine.rs b/crates/accord/src/evidence/machine.rs
index 967f42b..675e24b 100644
--- a/crates/accord/src/evidence/machine.rs
+++ b/crates/accord/src/evidence/machine.rs
@@ -11,7 +11,7 @@ use crate::obligation::{self, Claim, Obligation};
 use crate::syntax::{Machine, Program, Role};
 use crate::{
     Definition, DefinitionKind, ExampleRun, Exploration, Inputs, ObligationKind, Outcome,
-    Refutation, Run, Solvers, Standing, TraceStep, Verdict, identity, syntax,
+    Refutation, Run, Solvers, Standing, TraceStep, Verdict, identity,
 };
 
 /// What checking a machine established, short of its standing.
@@ -27,17 +27,9 @@ pub(super) struct Checked {
 /// machine's observers as functions known by their contracts, without the
 /// invariants they assume.
 fn callee_view(program: &Program, machine: &Machine) -> Program {
-    let mut functions = program.functions.clone();
-    for observer in &machine.observers {
-        let mut callee = observer.clone();
-        callee
-            .clauses
-            .retain(|c| c.kind != syntax::ClauseKind::Invariant);
-        functions.push(callee);
-    }
     Program {
         enums: program.enums.clone(),
-        functions,
+        functions: machine.functions(&program.functions),
         machines: Vec::new(),
         examples: Vec::new(),
         machine_examples: Vec::new(),
diff --git a/crates/accord/src/syntax.rs b/crates/accord/src/syntax.rs
index 098c760..8303217 100644
--- a/crates/accord/src/syntax.rs
+++ b/crates/accord/src/syntax.rs
@@ -301,6 +301,19 @@ pub(crate) struct Machine {
 }
 
 impl Machine {
+    /// The functions a member of this machine may call: `globals`, and the
+    /// machine's observers as callees know them, without the invariants they
+    /// assume of the state they read.
+    pub fn functions(&self, globals: &[Function]) -> Vec<Function> {
+        let mut functions = globals.to_vec();
+        for observer in &self.observers {
+            let mut callee = observer.clone();
+            callee.clauses.retain(|c| c.kind != ClauseKind::Invariant);
+            functions.push(callee);
+        }
+        functions
+    }
+
     /// Inits, then events, then observers: the order of the machine's
     /// obligations.
     pub fn members(&self) -> impl Iterator<Item = &Function> {
diff --git a/crates/accord/src/typescript.rs b/crates/accord/src/typescript.rs
index 791b0cf..328348f 100644
--- a/crates/accord/src/typescript.rs
+++ b/crates/accord/src/typescript.rs
@@ -14,9 +14,9 @@ mod lists;
 use std::collections::BTreeMap;
 
 use crate::openness::{Determinacy, Openness};
-use crate::syntax::{Body, Enum, Function, Program, Type, Width};
+use crate::syntax::{Body, Enum, Expr, Function, Machine, Program, Role, Type, Width};
 use crate::{Diagnostic, Outcome, Report, Run, Solvers};
-use boundary::{TEXT_CHECK, wrapper};
+use boundary::{TEXT_CHECK, state_check, state_type, wrapper};
 use expr::{Context, Scope, camel, string};
 
 const HEADER: &str = "// Every obligation of these functions is proved. This TypeScript is not
@@ -26,6 +26,12 @@ const HEADER: &str = "// Every obligation of these functions is proved. This Typ
 // throws a TypeError or a RangeError when one doesn't hold.
 ";
 
+const MACHINE_HEADER: &str =
+    "// A machine's events and observers also check that the state they are given
+// has its fields and meets every invariant and helper invariant. An event
+// returns the next state and leaves the one it is given unchanged.
+";
+
 /// One generated TypeScript module.
 #[derive(Clone, Debug, PartialEq)]
 pub struct Module {
@@ -60,16 +66,7 @@ fn proved(report: &Report) -> bool {
 /// names the functions that have one.
 pub fn build(files: &[(String, String)], solvers: &Solvers) -> Result<Build, Diagnostic> {
     let (program, names) = crate::program_of(files)?;
-    if let Some(machine) = program.machines.first() {
-        return Err(Diagnostic::new(
-            machine.line,
-            format!(
-                "`{}` is a machine: machines aren't written as TypeScript yet",
-                machine.name
-            ),
-        )
-        .in_file(&names[machine.file]));
-    }
+    check_exports(&program, &names)?;
     let report = crate::report(&program, None, &names, solvers);
     let modules = proved(&report).then(|| {
         modules(&program, &names, &report.openness)
@@ -80,6 +77,62 @@ pub fn build(files: &[(String, String)], solvers: &Solvers) -> Result<Build, Dia
     Ok(Build { report, modules })
 }
 
+/// The public machines declared in `file`.
+fn machines(program: &Program, file: usize) -> Vec<&Machine> {
+    program
+        .machines
+        .iter()
+        .filter(|m| m.file == file && m.public)
+        .collect()
+}
+
+/// Rejects a file whose module would declare one name twice: an exported
+/// function, a function's body or a machine's check, whichever it comes from.
+fn check_exports(program: &Program, names: &[String]) -> Result<(), Diagnostic> {
+    for (file, name) in names.iter().enumerate() {
+        let functions: Vec<&Function> = program
+            .functions
+            .iter()
+            .filter(|f| f.file == file && f.public)
+            .collect();
+        let mut declared: Vec<(String, usize)> = Vec::new();
+        let mut members: Vec<&Function> = Vec::new();
+        for function in &functions {
+            let exported = camel(&function.name);
+            declared.push((format!("{exported}$"), function.line));
+            declared.push((exported, function.line));
+        }
+        for machine in machines(program, file) {
+            declared.push((format!("check{}$", machine.name), machine.line));
+            for member in machine.members() {
+                let exported = camel(&member.name);
+                declared.push((format!("{exported}$"), member.line));
+                declared.push((exported, member.line));
+                members.push(member);
+            }
+        }
+        let all: Vec<&Function> = functions.iter().chain(&members).copied().collect();
+        declared.extend(
+            called(program, &all)
+                .iter()
+                .map(|f| (format!("{}$", camel(&f.name)), f.line)),
+        );
+        for (index, (declaration, line)) in declared.iter().enumerate() {
+            if declared[..index]
+                .iter()
+                .any(|(other, _)| other == declaration)
+            {
+                return Err(Diagnostic::new(
+                    *line,
+                    format!("`{declaration}` is declared twice in the module this file becomes"),
+                )
+                .in_file(name));
+            }
+        }
+    }
+    Ok(())
+}
+
 /// The modules for `program`'s files, named after `names`, in their order.
 fn modules(program: &Program, names: &[String], openness: &[Determinacy]) -> Vec<(String, String)> {
     names
@@ -98,10 +151,15 @@ fn module(program: &Program, names: &[String], file: usize, openness: &[Determin
         .iter()
         .filter(|f| f.file == file && f.public)
         .collect();
+    let machines = machines(program, file);
+    let members: Vec<&Function> = machines.iter().flat_map(|m| m.members()).collect();
     let mut out = format!(
         "// Generated by accord from {}. Do not edit.\n{HEADER}",
         names[file]
     );
+    if !machines.is_empty() {
+        out += MACHINE_HEADER;
+    }
     for function in &functions {
         let found = openness.iter().find(|d| d.function == function.name);
         match found.map(|d| &d.openness) {
@@ -121,7 +179,8 @@ fn module(program: &Program, names: &[String], file: usize, openness: &[Determin
         }
     }
     let mut items = Vec::new();
-    let imports = imports(program, names, file, &functions);
+    let everything: Vec<&Function> = functions.iter().chain(&members).copied().collect();
+    let imports = imports(program, names, file, &everything);
     if !imports.is_empty() {
         items.push(imports);
     }
@@ -135,15 +194,31 @@ fn module(program: &Program, names: &[String], file: usize, openness: &[Determin
     }
     let mut text = false;
     for function in &functions {
-        let (wrapper, uses_text) = wrapper(program, function);
+        let (wrapper, uses_text) = wrapper(program, function, None);
         text |= uses_text;
         items.push(wrapper);
-        items.push(core(function, program));
+        items.push(core(function, program, &program.functions));
+    }
+    for machine in &machines {
+        items.push(state_type(machine));
+        let (check, uses_text) = state_check(program, machine);
+        text |= uses_text;
+        items.push(check);
+        let callable = machine.functions(&program.functions);
+        for member in machine.members() {
+            let (wrapper, uses_text) = wrapper(program, member, Some(machine));
+            text |= uses_text;
+            items.push(wrapper);
+            items.push(match member.machine.map(|m| m.role) {
+                Some(Role::Observer) => core(member, program, &callable),
+                _ => transition_core(member, machine, program, &callable),
+            });
+        }
     }
     // A called function's body is written into every module that calls it,
     // unexported, so no module exports an unchecked entry point.
-    for function in called(program, &functions) {
-        items.push(core(function, program));
+    for function in called(program, &everything) {
+        items.push(core(function, program, &program.functions));
     }
     if text {
         items.push(TEXT_CHECK.to_string());
@@ -255,13 +330,116 @@ fn signature(function: &Function, name: &str, ty: fn(&Type) -> String) -> String
     format!("{name}({}): {}", params.join(", "), ty(&function.ret))
 }
 
-/// The function's body, unexported; it may call the program's functions.
-fn core(function: &Function, program: &Program) -> String {
+/// The body of an init or event, unexported: it takes the state's fields,
+/// for an event, then its own parameters, and returns the next state.
+fn transition_core(
+    function: &Function,
+    machine: &Machine,
+    program: &Program,
+    functions: &[Function],
+) -> String {
+    let skip = match function.machine {
+        Some(member) if member.role == Role::Init => member.state,
+        _ => 0,
+    };
+    let params: Vec<String> = function.params[skip..]
+        .iter()
+        .map(|(n, t)| format!("{}: {}", camel(n), inner(t)))
+        .collect();
+    let code = Scope {
+        params: &function.params,
+        context: Context::Code,
+        functions,
+        enums: &program.enums,
+        indices: &[],
+    };
+    let mut out = format!(
+        "function {}$({}): {} {{\n",
+        camel(&function.name),
+        params.join(", "),
+        machine.name
+    );
+    match &function.body {
+        Body::Expr(body) => out += &transition(&code, machine, body, "  "),
+        Body::Decide(rows, _) => {
+            for row in rows {
+                out += &match &row.condition {
+                    Some(condition) => {
+                        let condition = code.bare(condition, None);
+                        branch(&code, machine, &condition, &row.result, "  ")
+                    }
+                    None => transition(&code, machine, &row.result, "  "),
+                };
+            }
+            if rows.last().is_some_and(|row| row.condition.is_some()) {
+                out += &format!(
+                    "  throw new Error({});\n",
+                    string(&format!("{}: no row matched", camel(&function.name)))
+                );
+            }
+        }
+    }
+    out + "}\n"
+}
+
+/// The statements that return the state an `if`, or a `next`, ends in.
+fn transition(code: &Scope, machine: &Machine, expr: &Expr, indent: &str) -> String {
+    match expr {
+        Expr::If(condition, then, otherwise) => {
+            let condition = code.bare(condition, None);
+            branch(code, machine, &condition, then, indent)
+                + &transition(code, machine, otherwise, indent)
+        }
+        Expr::Next(fields, _) => {
+            format!("{indent}return {};\n", state_object(code, machine, fields))
+        }
+        _ => unreachable!("`check` ends every init and event in a `next`"),
+    }
+}
+
+/// `if (condition)` and what returns the state `then` ends in.
+fn branch(code: &Scope, machine: &Machine, condition: &str, then: &Expr, indent: &str) -> String {
+    match then {
+        Expr::Next(fields, _) => format!(
+            "{indent}if ({condition}) return {};\n",
+            state_object(code, machine, fields)
+        ),
+        _ => format!(
+            "{indent}if ({condition}) {{\n{}{indent}}}\n",
+            transition(code, machine, then, &format!("{indent}  "))
+        ),
+    }
+}
+
+/// The state as an object literal, every field in the state's order.
+fn state_object(code: &Scope, machine: &Machine, fields: &[(String, Expr)]) -> String {
+    let parts: Vec<String> = fields
+        .iter()
+        .zip(&machine.state)
+        .map(|((_, value), (field, ty))| {
+            let want = match ty {
+                Type::Int(width) => Some(*width),
+                _ => None,
+            };
+            let value = code.bare(value, want);
+            let value = if *ty == Type::Int(Width::I64) {
+                format!("Number({value})")
+            } else {
+                value
+            };
+            format!("{}: {value}", camel(field))
+        })
+        .collect();
+    format!("{{ {} }}", parts.join(", "))
+}
+
+/// The function's body, unexported; it may call `functions`.
+fn core(function: &Function, program: &Program, functions: &[Function]) -> String {
     let name = format!("{}$", camel(&function.name));
     let code = Scope {
         params: &function.params,
         context: Context::Code,
-        functions: &program.functions,
+        functions,
         enums: &program.enums,
         indices: &[],
     };
diff --git a/crates/accord/src/typescript/boundary.rs b/crates/accord/src/typescript/boundary.rs
index 9e24b4f..823dda9 100644
--- a/crates/accord/src/typescript/boundary.rs
+++ b/crates/accord/src/typescript/boundary.rs
@@ -1,10 +1,14 @@
 //! The exported function: it checks what the proofs assume of its caller,
 //! its parameters' types and ranges and each `requires`, and then calls the
 //! body. Integers in a `requires` are mathematical, so they are `bigint`s.
+//!
+//! A machine's state is a `readonly` object of its fields. An event or
+//! observer takes it first and checks it, its fields and then every
+//! invariant and helper invariant, before it checks anything else.
 
 use super::expr::{Context, Scope, camel, string};
-use super::{enumeration, outer, signature};
-use crate::syntax::{ClauseKind, Function, Program, Type, Width};
+use super::{enumeration, outer};
+use crate::syntax::{ClauseKind, Function, Machine, Program, Role, Type, Width};
 
 pub(super) const TEXT_CHECK: &str = "function isText$(value: string): boolean {
   for (const character of value) {
@@ -19,21 +23,42 @@ pub(super) const TEXT_CHECK: &str = "function isText$(value: string): boolean {
 
 const TEXT_RANGE: &str = "must hold only characters up to U+2FFFF, with no lone surrogates";
 
+/// A template literal that starts with `${where}: `, so a check of a state
+/// says which exported function it runs for. The message is escaped.
+fn template(message: &str) -> String {
+    let mut out = String::from("`${where}: ");
+    for c in message.chars() {
+        if matches!(c, '\\' | '`' | '$') {
+            out.push('\\');
+        }
+        out.push(c);
+    }
+    out.push('`');
+    out
+}
+
+/// An `if` that throws `error` with the message, a literal, when `check`.
 fn throw(check: &str, error: &str, message: &str) -> String {
-    format!(
-        "  if ({check}) {{\n    throw new {error}({});\n  }}\n",
-        string(message)
-    )
+    format!("  if ({check}) {{\n    throw new {error}({message});\n  }}\n")
 }
 
-/// The exported function, and whether it checks a text.
-pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool) {
-    let name = camel(&function.name);
-    let mut out = format!("export function {} {{\n", signature(function, &name, outer));
+/// How a check words what it found.
+struct Words<'a> {
+    /// What the value is called in a message, given its variable.
+    subject: &'a dyn Fn(&str) -> String,
+    /// A message as a TypeScript literal.
+    render: &'a dyn Fn(&str) -> String,
+}
+
+/// The checks of `params`' types and ranges, one `if` each, and whether any
+/// is of a text. Each parameter is a variable of its camel-case name.
+fn param_checks(program: &Program, params: &[(String, Type)], words: &Words) -> (String, bool) {
+    let mut out = String::new();
     let mut text = false;
-    for (param, ty) in &function.params {
+    for (param, ty) in params {
         let p = camel(param);
-        let must = |what: &str| format!("{name}: {p} must be {what}");
+        let subject = (words.subject)(&p);
+        let must = |what: &str| (words.render)(&format!("{subject} must be {what}"));
         let variants = |enum_name: &str| -> String {
             let e = enumeration(program, enum_name).expect("`check` resolves every enum");
             let values: Vec<String> = e.variants.iter().map(|v| string(&e.text(v))).collect();
@@ -81,7 +106,7 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
                 out += &throw(
                     &format!("!isText$({p})"),
                     "RangeError",
-                    &format!("{name}: {p} {TEXT_RANGE}"),
+                    &(words.render)(&format!("{subject} {TEXT_RANGE}")),
                 );
             }
             Type::Enum(e) => {
@@ -105,12 +130,113 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
                     out += &throw(
                         &format!("!{p}.every(isText$)"),
                         "RangeError",
-                        &format!("{name}: {p} {TEXT_RANGE}"),
+                        &(words.render)(&format!("{subject} {TEXT_RANGE}")),
                     );
                 }
             }
         }
     }
+    (out, text)
+}
+
+/// `const { a, b } = state;`, naming every field.
+fn destructure(machine: &Machine) -> String {
+    if machine.state.is_empty() {
+        return String::new();
+    }
+    let names: Vec<String> = machine.state.iter().map(|(n, _)| camel(n)).collect();
+    format!("  const {{ {} }} = state;\n", names.join(", "))
+}
+
+/// The machine's state as a type: its fields, in order.
+pub(super) fn state_type(machine: &Machine) -> String {
+    let mut out = format!("export type {} = {{\n", machine.name);
+    for (field, ty) in &machine.state {
+        out += &format!("  readonly {}: {};\n", camel(field), outer(ty));
+    }
+    out + "};\n"
+}
+
+/// The function that checks a state: that it is an object with the fields'
+/// types and ranges, and that it meets every invariant and then every helper
+/// invariant. Also whether it checks a text.
+pub(super) fn state_check(program: &Program, machine: &Machine) -> (String, bool) {
+    let name = &machine.name;
+    let mut out = format!("function check{name}$(where: string, state: {name}): void {{\n");
+    out += &throw(
+        "typeof state !== \"object\" || state === null",
+        "TypeError",
+        &template(&format!("state must be a {name}")),
+    );
+    out += &destructure(machine);
+    let (checks, text) = param_checks(
+        program,
+        &machine.state,
+        &Words {
+            subject: &|field| format!("state.{field}"),
+            render: &template,
+        },
+    );
+    out += &checks;
+    let spec = Scope {
+        params: &machine.state,
+        context: Context::Spec,
+        functions: &[],
+        enums: &program.enums,
+        indices: &[],
+    };
+    for helper in [false, true] {
+        for invariant in machine.invariants.iter().filter(|c| c.helper == helper) {
+            let check = format!("!({})", spec.bare(&invariant.expr, None));
+            out += &throw(
+                &check,
+                "RangeError",
+                &template(&format!("state breaks {}", invariant.text)),
+            );
+        }
+    }
+    (out + "}\n", text)
+}
+
+/// The exported function of a function, or of a machine's init, event or
+/// observer, and whether it checks a text. An event or observer takes the
+/// machine's state first; an init has none to take.
+pub(super) fn wrapper(
+    program: &Program,
+    function: &Function,
+    machine: Option<&Machine>,
+) -> (String, bool) {
+    let name = camel(&function.name);
+    let role = function.machine.map(|m| m.role);
+    let state = function.machine.map_or(0, |m| m.state);
+    let reads_state = role.is_some_and(|r| r != Role::Init);
+    let own = &function.params[state..];
+    let ret = match (role, machine) {
+        (Some(Role::Init | Role::Event), Some(machine)) => machine.name.clone(),
+        _ => outer(&function.ret),
+    };
+    let mut params: Vec<String> = Vec::new();
+    if let (true, Some(machine)) = (reads_state, machine) {
+        params.push(format!("state: {}", machine.name));
+    }
+    params.extend(
+        own.iter()
+            .map(|(n, t)| format!("{}: {}", camel(n), outer(t))),
+    );
+    let mut out = format!("export function {name}({}): {ret} {{\n", params.join(", "));
+    if let (true, Some(machine)) = (reads_state, machine) {
+        out += &format!("  check{}$({}, state);\n", machine.name, string(&name));
+        out += &destructure(machine);
+    }
+    let (checks, text) = param_checks(
+        program,
+        own,
+        &Words {
+            subject: &|p| p.to_string(),
+            render: &|message| string(&format!("{name}: {message}")),
+        },
+    );
+    out += &checks;
     let spec = Scope {
         params: &function.params,
         context: Context::Spec,
@@ -124,10 +250,13 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
         .filter(|c| c.kind == ClauseKind::Requires)
     {
         let check = format!("!({})", spec.bare(&clause.expr, None));
-        out += &throw(&check, "RangeError", &format!("{name}: {}", clause.text));
+        out += &throw(
+            &check,
+            "RangeError",
+            &string(&format!("{name}: {}", clause.text)),
+        );
     }
-    let args: Vec<String> = function
-        .params
+    let args: Vec<String> = function.params[if role == Some(Role::Init) { state } else { 0 }..]
         .iter()
         .map(|(n, t)| match t {
             Type::Int(Width::I64) => format!("BigInt({})", camel(n)),
@@ -135,16 +264,37 @@ pub(super) fn wrapper(program: &Program, function: &Function) -> (String, bool)
         })
         .collect();
     let call = format!("{name}$({})", args.join(", "));
-    if function.ret == Type::Int(Width::I64) {
+    let unsafe_fields: Vec<String> = match (role, machine) {
+        (Some(Role::Init | Role::Event), Some(machine)) => machine
+            .state
+            .iter()
+            .filter(|(_, ty)| *ty == Type::Int(Width::I64))
+            .map(|(field, _)| format!("!Number.isSafeInteger(result.{})", camel(field)))
+            .collect(),
+        _ => Vec::new(),
+    };
+    if function.machine.is_none_or(|m| m.role == Role::Observer)
+        && function.ret == Type::Int(Width::I64)
+    {
         out += &format!("  const result = {call};\n");
         out += &throw(
             "result < -9007199254740991n || result > 9007199254740991n",
             "RangeError",
-            &format!("{name}: the result is not a safe integer"),
+            &string(&format!("{name}: the result is not a safe integer")),
         );
         out += "  return Number(result);\n";
-    } else {
+    } else if unsafe_fields.is_empty() {
         out += &format!("  return {call};\n");
+    } else {
+        out += &format!("  const result = {call};\n");
+        out += &throw(
+            &unsafe_fields.join(" || "),
+            "RangeError",
+            &string(&format!(
+                "{name}: the state has a field that is not a safe integer"
+            )),
+        );
+        out += "  return result;\n";
     }
     out += "}\n";
     (out, text)
diff --git a/crates/accord/src/typescript/differential.rs b/crates/accord/src/typescript/differential.rs
index 68782db..7eaa511 100644
--- a/crates/accord/src/typescript/differential.rs
+++ b/crates/accord/src/typescript/differential.rs
@@ -25,8 +25,8 @@ mod inputs;
 use super::expr::camel;
 use crate::Solvers;
 use crate::interpret::{self, Value};
-use crate::syntax::{Enum, Function, Type, Width};
-use inputs::{SAFE, Seeded, inputs};
+use crate::syntax::{Enum, Function, Machine, Role, Type, Width};
+use inputs::{SAFE, Seeded, inputs, member_inputs};
 
 fn to_json(value: &Value, enums: &[Enum]) -> Json {
     match value {
@@ -74,6 +74,78 @@ fn expected(
     }
 }
 
+/// A state as the object the module takes and returns.
+fn state_json(machine: &Machine, values: &[Value], enums: &[Enum]) -> Json {
+    machine
+        .state
+        .iter()
+        .zip(values)
+        .map(|((field, _), value)| (camel(field), to_json(value, enums)))
+        .collect::<serde_json::Map<String, Json>>()
+        .into()
+}
+
+/// What a machine's init, event or observer must do in `state` with `args`:
+/// refuse a state that breaks an invariant or helper invariant, and
+/// otherwise behave as the interpreter does.
+fn expected_member(
+    machine: &Machine,
+    member: &Function,
+    state: &[Value],
+    args: &[Value],
+    functions: &[Function],
+    enums: &[Enum],
+) -> Json {
+    let skip = member.machine.map_or(0, |m| m.state);
+    let role = member.machine.map(|m| m.role);
+    let unsafe_i64 = |ty: &Type, v: &Value| {
+        *ty == Type::Int(Width::I64) && matches!(v, Value::Int(n) if n.abs() > SAFE)
+    };
+    let own = &member.params[skip..];
+    let mut names: interpret::Names = Vec::new();
+    if role != Some(Role::Init) {
+        names.extend(interpret::fields(member, state));
+        if machine
+            .state
+            .iter()
+            .zip(state)
+            .any(|((_, ty), v)| unsafe_i64(ty, v))
+            || !matches!(interpret::broken_invariant(member, state), Ok(None))
+        {
+            return json!({"error": "RangeError"});
+        }
+    }
+    names.extend(own.iter().map(|(n, _)| n.clone()).zip(args.iter().cloned()));
+    if own.iter().zip(args).any(|((_, ty), v)| unsafe_i64(ty, v)) {
+        return json!({"error": "RangeError"});
+    }
+    match interpret::broken_requires(member, &names) {
+        Ok(Some(_)) => return json!({"error": "RangeError"}),
+        Ok(None) => {}
+        Err(reason) => panic!("{}: requires can't be evaluated: {reason}", member.name),
+    }
+    if role == Some(Role::Observer) {
+        return match interpret::result(member, &names, functions) {
+            Ok(result) if unsafe_i64(&member.ret, &result) => json!({"error": "RangeError"}),
+            Ok(result) => json!({"ok": to_json(&result, enums)}),
+            Err(reason) => panic!("{}: no result for an admitted state: {reason}", member.name),
+        };
+    }
+    match interpret::transition(member, &names, functions) {
+        Ok(next)
+            if machine
+                .state
+                .iter()
+                .zip(&next)
+                .any(|((_, ty), v)| unsafe_i64(ty, v)) =>
+        {
+            json!({"error": "RangeError"})
+        }
+        Ok(next) => json!({"ok": state_json(machine, &next, enums)}),
+        Err(reason) => panic!("{}: no state for an admitted state: {reason}", member.name),
+    }
+}
+
 fn conformance() -> PathBuf {
     PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../../conformance")
 }
@@ -180,6 +252,35 @@ fn generated_modules_agree_with_the_interpreter() {
                 }));
             }
         }
+        for machine in program.machines.iter().filter(|m| m.public) {
+            let module = dir.join(format!(
+                "{}.ts",
+                names[machine.file]
+                    .strip_suffix(".accord")
+                    .unwrap_or(&names[machine.file])
+            ));
+            let callable = machine.functions(&program.functions);
+            for member in machine.members() {
+                let reads = member.machine.is_some_and(|m| m.role != Role::Init);
+                for (state, args) in member_inputs(&program, machine, member, &mut seeded) {
+                    wanted.push((
+                        name.clone(),
+                        member.name.clone(),
+                        expected_member(machine, member, &state, &args, &callable, &program.enums),
+                    ));
+                    let mut given: Vec<Json> = Vec::new();
+                    if reads {
+                        given.push(state_json(machine, &state, &program.enums));
+                    }
+                    given.extend(args.iter().map(|a| to_json(a, &program.enums)));
+                    calls.push(json!({
+                        "module": module.display().to_string(),
+                        "name": camel(&member.name),
+                        "args": given,
+                    }));
+                }
+            }
+        }
     }
     assert!(built > 0, "no program built");
     let runner = root.join("runner.mjs");
diff --git a/crates/accord/src/typescript/differential/inputs.rs b/crates/accord/src/typescript/differential/inputs.rs
index 906c82d..a32afd6 100644
--- a/crates/accord/src/typescript/differential/inputs.rs
+++ b/crates/accord/src/typescript/differential/inputs.rs
@@ -1,7 +1,7 @@
 //! The inputs each exported function is called with.
 
 use crate::interpret::{self, Value};
-use crate::syntax::{Body, Expr, Function, Program, Type, Width};
+use crate::syntax::{Body, Expr, Function, Machine, Program, Role, Type, Width};
 use crate::{Outcome, Report};
 
 pub(super) const LIMIT: usize = 4096;
@@ -124,6 +124,71 @@ fn combinations(domains: &[Vec<Value>], seeded: &mut Seeded) -> Vec<Vec<Value>>
     }
 }
 
+/// The integer literals in `expr`.
+fn integers(expr: &Expr, found: &mut Vec<i128>) {
+    match expr {
+        Expr::Int(n, _) if !found.contains(n) => found.push(*n),
+        Expr::Not(inner) | Expr::Neg(inner, _) => integers(inner, found),
+        Expr::Binary(_, l, r) | Expr::Arith(_, l, r, _) => {
+            integers(l, found);
+            integers(r, found);
+        }
+        Expr::If(c, a, b) => [c, a, b].iter().for_each(|e| integers(e, found)),
+        _ => {}
+    }
+}
+
+/// Every state, with every set of arguments, that `member` of `machine` is
+/// called with: the combinations of its fields' and parameters' values, which
+/// include each integer the machine's clauses name and its neighbours, so that
+/// some states meet its invariants and others break them. An init takes no
+/// state, so its states are empty.
+pub(super) fn member_inputs(
+    program: &Program,
+    machine: &Machine,
+    member: &Function,
+    seeded: &mut Seeded,
+) -> Vec<(Vec<Value>, Vec<Value>)> {
+    let words = literals(program);
+    let mut named = Vec::new();
+    for clause in machine
+        .members()
+        .flat_map(|m| m.clauses.iter())
+        .chain(&machine.invariants)
+    {
+        integers(&clause.expr, &mut named);
+    }
+    let fields = member.machine.map_or(0, |m| m.state);
+    let reads = member.machine.is_some_and(|m| m.role != Role::Init);
+    let types: Vec<&Type> = member.params[if reads { 0 } else { fields }..]
+        .iter()
+        .map(|(_, ty)| ty)
+        .collect();
+    let domains: Vec<Vec<Value>> = types
+        .iter()
+        .map(|ty| {
+            let mut values = domain(ty, program, &words, seeded);
+            if let Type::Int(width) = ty {
+                for n in named.iter().flat_map(|n| [n - 1, *n, n + 1]) {
+                    let value = Value::Int(n);
+                    if (width.min()..=width.max()).contains(&n) && !values.contains(&value) {
+                        values.push(value);
+                    }
+                }
+            }
+            values
+        })
+        .collect();
+    let split = if reads { fields } else { 0 };
+    combinations(&domains, seeded)
+        .into_iter()
+        .map(|mut all| {
+            let args = all.split_off(split);
+            (all, args)
+        })
+        .collect()
+}
+
 /// An `example` argument's value: examples are written with literals.
 fn literal(expr: &Expr) -> Option<Value> {
     match expr {
diff --git a/crates/accord/src/typescript/expr.rs b/crates/accord/src/typescript/expr.rs
index 3eb908a..bde2a05 100644
--- a/crates/accord/src/typescript/expr.rs
+++ b/crates/accord/src/typescript/expr.rs
@@ -162,7 +162,9 @@ impl Scope<'_> {
             }
             Expr::Length(list, _) => self.length(list),
             Expr::Index(list, index, _) => self.index(list, index),
-            Expr::Next(..) => unreachable!("`build` refuses a program with a machine"),
+            Expr::Next(..) => {
+                unreachable!("a `next` is written by a machine's body, never as a value")
+            }
         }
     }
 
diff --git a/crates/accord/tests/machines.rs b/crates/accord/tests/machines.rs
index 1d7e132..8ab86d5 100644
--- a/crates/accord/tests/machines.rs
+++ b/crates/accord/tests/machines.rs
@@ -113,13 +113,41 @@ fn the_receipt_names_the_outcome_and_the_exploration() {
 }
 
 #[test]
-fn a_machine_is_not_written_as_typescript() {
+fn only_a_proved_pub_machine_is_written_as_typescript() {
     let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
-    let files = [("dial.accord".to_string(), DIAL.to_string())];
-    let Err(refusal) = build(&files, &solvers) else {
-        panic!("a machine was built");
+    let build_of =
+        |source: &str| build(&[("dial.accord".to_string(), source.to_string())], &solvers);
+    // `bounded` is refuted, so nothing is written.
+    let built = build_of(DIAL).expect("the program is accepted");
+    assert!(built.modules.is_none());
+    let proved = DIAL.replace("level <= 10", "level <= 12");
+    let built = build_of(&proved.replace("machine Dial", "pub machine Dial"))
+        .expect("the program is accepted");
+    let modules = built.modules.expect("every obligation is proved");
+    assert!(
+        modules[0]
+            .source
+            .contains("export function set(state: Dial")
+    );
+    // A machine without `pub` writes nothing.
+    let built = build_of(&proved).expect("the program is accepted");
+    let modules = built.modules.expect("every obligation is proved");
+    assert!(!modules[0].source.contains("Dial"));
+}
+
+#[test]
+fn names_that_would_collide_in_a_module_are_refused() {
+    let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
+    let source = "pub fn start() -> i32 { 1 }
+pub machine M {
+    state { x: i32 }
+    init start() { next { x: 0 } }
+}
+";
+    let Err(refusal) = build(&[("m.accord".to_string(), source.to_string())], &solvers) else {
+        panic!("colliding names were built");
     };
-    assert!(refusal.message.contains("machine"), "{}", refusal.message);
+    assert!(refusal.message.contains("start"), "{}", refusal.message);
 }
 
 const STEPPED: &str = "machine Pair {

From 1f5d8a10395128d65e158141732196209aa01c79 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 21:35:37 -0700
Subject: [PATCH 3/6] docs: describe a machine's TypeScript module

Refs #82
---
 docs/design/syntax.md |  4 ++--
 docs/typescript.md    | 36 ++++++++++++++++++++++++++++++++++--
 2 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/docs/design/syntax.md b/docs/design/syntax.md
index c6a86de..64dfc3a 100644
--- a/docs/design/syntax.md
+++ b/docs/design/syntax.md
@@ -179,8 +179,8 @@ Blocks are expressions: the last expression is the block's value. There is no
 ## Machines
 
 Accepted for stage 10 ([#82](https://github.com/sequelcore/accord/issues/82)).
-`accord check` checks a machine; `accord build` doesn't write it as
-TypeScript yet. A machine is a state, the ways it starts, the events
+`accord check` checks a machine, and `accord build` writes a `pub` machine
+as TypeScript once every obligation is proved. A machine is a state, the ways it starts, the events
 that move it, and what must hold in every state it reaches:
 
 ```accord
diff --git a/docs/typescript.md b/docs/typescript.md
index ab1a230..3efd5d6 100644
--- a/docs/typescript.md
+++ b/docs/typescript.md
@@ -10,7 +10,8 @@ imports with no runtime dependency.
 when every obligation is proved and every `example` passes; otherwise it writes
 nothing and exits 1 when something failed, or 3 when something wasn't proved.
 An open case doesn't stop it: the module's header names each function with
-one.
+one. A machine is written only when all its obligations are proved: one that is
+`not_inductive` or undecided stops the build, like any other obligation.
 
 | Code | Meaning |
 | --- | --- |
@@ -38,6 +39,8 @@ Node runs them directly.
 | `i64` | `number` for the caller, `bigint` inside |
 | `List<T>` | `readonly T[]` |
 | `requires` | A check on entry |
+| `pub machine M` | A type, a state check, and an exported function for each init, event and observer, below |
+| `machine` without `pub` | Nothing |
 | `ensures`, `open when`, `example`, `intent` | Nothing: they don't run |
 
 Inside, a decision table is an `if` chain in row order. Where no row is
@@ -62,6 +65,25 @@ never import each other's functions.
 fit `i32`, so it is well inside the integers a `number` holds exactly. `i64`
 arithmetic runs in `bigint`.
 
+## Machines
+
+A `pub machine Switch` becomes `export type Switch = { readonly light: Light;
+readonly presses: number; }`, its fields in order and in `camelCase`, and
+a function `checkSwitch$` that no module exports. Each init, event and
+observer is an exported function named in `camelCase`, with its body unexported
+beside it, as for a function:
+
+- an init takes its parameters and returns the state it gives;
+- an event takes the state, then its parameters, and returns the next state,
+  a new object that lists every field; it leaves the state it was given
+  unchanged;
+- an observer takes the state, then its parameters, and returns its result.
+
+An `i64` field is a `number` in the state, and an event that would leave one
+that isn't a safe integer throws a `RangeError`, as a function does for its
+result. A module whose exported names, or their bodies' names, would collide is
+refused, and nothing is written.
+
 ## The boundary
 
 The proofs assume the caller is checked code. A TypeScript caller isn't, so
@@ -74,6 +96,13 @@ each exported function checks, in order, before it runs:
 | A text holds only characters up to U+2FFFF, the solvers' alphabet, with no lone surrogates | `RangeError` |
 | Each `requires` holds, evaluated with mathematical integers (`bigint`) | `RangeError`, naming the clause |
 
+An event or observer first checks the state it is given, before its own
+parameters: it is an object (`TypeError`), each field has its type and range
+(`TypeError`, `RangeError`, worded `state.<field> must be …`), and then it
+meets every invariant, then every helper invariant, evaluated with
+mathematical integers (`RangeError`, `state breaks invariant <name>: …`). An
+init has no state to check; its result meets the invariants by proof.
+
 An `i64` result that isn't a safe integer throws a `RangeError` instead of
 losing precision. So the generated function accepts fewer inputs than the
 proofs cover, and never runs on one they don't.
@@ -85,5 +114,8 @@ compiler's own tests compare each module with the interpreter: on every
 combination of `Bool` and enum values, each integer width's boundaries and a
 seeded sample, the program's text literals and characters beyond ASCII, each
 `example`'s call and every input a solver gave, with a seeded sample past
-4,096 combinations per function. Agreement on those inputs is evidence, not a
+4,096 combinations per function. For a machine, the same inputs for each
+init, event and observer, and for events and observers, states built from its
+fields' values and the integers its clauses name, most of them breaking an
+invariant or helper invariant, which the module must reject. Agreement on those inputs is evidence, not a
 proof.

From b383518547ffdfae7426951decbbbb2df0ebd658 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 21:44:39 -0700
Subject: [PATCH 4/6] test: read a machine's state once at the TypeScript
 boundary

A review showed the state check and the event each read the state, so an
accessor could pass the check with one value and hand the event another.
The check now returns one snapshot of the fields, which is all the event
reads, and its generated names end in $ so no field or parameter can
collide with them.

Refs #82
---
 conformance/typescript/machine/out/switch.ts | 34 +++++++++-----------
 1 file changed, 16 insertions(+), 18 deletions(-)

diff --git a/conformance/typescript/machine/out/switch.ts b/conformance/typescript/machine/out/switch.ts
index 9346e25..a4d9f45 100644
--- a/conformance/typescript/machine/out/switch.ts
+++ b/conformance/typescript/machine/out/switch.ts
@@ -15,26 +15,27 @@ export type Switch = {
   readonly presses: number;
 };
 
-function checkSwitch$(where: string, state: Switch): void {
-  if (typeof state !== "object" || state === null) {
-    throw new TypeError(`${where}: state must be a Switch`);
+function checkSwitch$(where$: string, state$: Switch): Switch {
+  if (typeof state$ !== "object" || state$ === null) {
+    throw new TypeError(`${where$}: state must be a Switch`);
   }
-  const { light, presses } = state;
+  const { light, presses } = state$;
   if (!["off", "on"].includes(light)) {
-    throw new TypeError(`${where}: state.light must be a Light`);
+    throw new TypeError(`${where$}: state.light must be a Light`);
   }
   if (typeof presses !== "number") {
-    throw new TypeError(`${where}: state.presses must be an i32`);
+    throw new TypeError(`${where$}: state.presses must be an i32`);
   }
   if (!Number.isInteger(presses) || presses < -2147483648 || presses > 2147483647) {
-    throw new RangeError(`${where}: state.presses must be an i32`);
+    throw new RangeError(`${where$}: state.presses must be an i32`);
   }
   if (!((BigInt(presses) >= 0n) && (BigInt(presses) <= 100n))) {
-    throw new RangeError(`${where}: state breaks invariant pressed: presses >= 0 and presses <= 100`);
+    throw new RangeError(`${where$}: state breaks invariant pressed: presses >= 0 and presses <= 100`);
   }
   if (!(!(light === "on") || (BigInt(presses) > 0n))) {
-    throw new RangeError(`${where}: state breaks helper invariant on_means_pressed: light == On implies presses > 0`);
+    throw new RangeError(`${where$}: state breaks helper invariant on_means_pressed: light == On implies presses > 0`);
   }
+  return { light, presses };
 }
 
 export function start(): Switch {
@@ -65,9 +66,8 @@ function resume$(fromLight: Light, fromPresses: number): Switch {
   return { light: fromLight, presses: fromPresses };
 }
 
-export function press(state: Switch): Switch {
-  checkSwitch$("press", state);
-  const { light, presses } = state;
+export function press(state$: Switch): Switch {
+  const { light, presses } = checkSwitch$("press", state$);
   if (!(BigInt(presses) < 100n)) {
     throw new RangeError("press: requires presses < 100");
   }
@@ -79,9 +79,8 @@ function press$(light: Light, presses: number): Switch {
   return { light: "off", presses: presses + 1 };
 }
 
-export function turnOff(state: Switch): Switch {
-  checkSwitch$("turnOff", state);
-  const { light, presses } = state;
+export function turnOff(state$: Switch): Switch {
+  const { light, presses } = checkSwitch$("turnOff", state$);
   return turnOff$(light, presses);
 }
 
@@ -89,9 +88,8 @@ function turnOff$(light: Light, presses: number): Switch {
   return { light: "off", presses: presses };
 }
 
-export function atLimit(state: Switch): boolean {
-  checkSwitch$("atLimit", state);
-  const { light, presses } = state;
+export function atLimit(state$: Switch): boolean {
+  const { light, presses } = checkSwitch$("atLimit", state$);
   return atLimit$(light, presses);
 }
 

From f3c626f294b0447554172d63e82d8d6f12574d24 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 21:50:29 -0700
Subject: [PATCH 5/6] fix: read a machine's state once and keep generated names
 apart

The state check returns a snapshot built from its single read, and
events and observers run on it, so a getter can't pass the check and
then give the body another value. Generated names end in $, so fields
called state or where no longer collide. Enums and machines sharing an
exported type name are refused.

Refs #82
---
 crates/accord/src/typescript.rs          |  4 +
 crates/accord/src/typescript/boundary.rs | 28 +++----
 crates/accord/tests/machines.rs          | 95 +++++++++++++++++++++++-
 3 files changed, 113 insertions(+), 14 deletions(-)

diff --git a/crates/accord/src/typescript.rs b/crates/accord/src/typescript.rs
index 328348f..3c7594f 100644
--- a/crates/accord/src/typescript.rs
+++ b/crates/accord/src/typescript.rs
@@ -102,7 +102,11 @@ fn check_exports(program: &Program, names: &[String]) -> Result<(), Diagnostic>
             declared.push((format!("{exported}$"), function.line));
             declared.push((exported, function.line));
         }
+        for e in program.enums.iter().filter(|e| e.file == file) {
+            declared.push((format!("type {}", e.name), e.line));
+        }
         for machine in machines(program, file) {
+            declared.push((format!("type {}", machine.name), machine.line));
             declared.push((format!("check{}$", machine.name), machine.line));
             for member in machine.members() {
                 let exported = camel(&member.name);
diff --git a/crates/accord/src/typescript/boundary.rs b/crates/accord/src/typescript/boundary.rs
index 823dda9..710aa2b 100644
--- a/crates/accord/src/typescript/boundary.rs
+++ b/crates/accord/src/typescript/boundary.rs
@@ -26,7 +26,7 @@ const TEXT_RANGE: &str = "must hold only characters up to U+2FFFF, with no lone
 /// A template literal that starts with `${where}: `, so a check of a state
 /// says which exported function it runs for. The message is escaped.
 fn template(message: &str) -> String {
-    let mut out = String::from("`${where}: ");
+    let mut out = String::from("`${where$}: ");
     for c in message.chars() {
         if matches!(c, '\\' | '`' | '$') {
             out.push('\\');
@@ -139,13 +139,10 @@ fn param_checks(program: &Program, params: &[(String, Type)], words: &Words) ->
     (out, text)
 }
 
-/// `const { a, b } = state;`, naming every field.
-fn destructure(machine: &Machine) -> String {
-    if machine.state.is_empty() {
-        return String::new();
-    }
+/// The fields as a comma-separated list of camel-case names.
+fn field_names(machine: &Machine) -> String {
     let names: Vec<String> = machine.state.iter().map(|(n, _)| camel(n)).collect();
-    format!("  const {{ {} }} = state;\n", names.join(", "))
+    names.join(", ")
 }
 
 /// The machine's state as a type: its fields, in order.
@@ -162,13 +159,13 @@ pub(super) fn state_type(machine: &Machine) -> String {
 /// invariant. Also whether it checks a text.
 pub(super) fn state_check(program: &Program, machine: &Machine) -> (String, bool) {
     let name = &machine.name;
-    let mut out = format!("function check{name}$(where: string, state: {name}): void {{\n");
+    let mut out = format!("function check{name}$(where$: string, state$: {name}): {name} {{\n");
     out += &throw(
-        "typeof state !== \"object\" || state === null",
+        "typeof state$ !== \"object\" || state$ === null",
         "TypeError",
         &template(&format!("state must be a {name}")),
     );
-    out += &destructure(machine);
+    out += &format!("  const {{ {} }} = state$;\n", field_names(machine));
     let (checks, text) = param_checks(
         program,
         &machine.state,
@@ -195,6 +192,7 @@ pub(super) fn state_check(program: &Program, machine: &Machine) -> (String, bool
             );
         }
     }
+    out += &format!("  return {{ {} }};\n", field_names(machine));
     (out + "}\n", text)
 }
 
@@ -217,7 +215,7 @@ pub(super) fn wrapper(
     };
     let mut params: Vec<String> = Vec::new();
     if let (true, Some(machine)) = (reads_state, machine) {
-        params.push(format!("state: {}", machine.name));
+        params.push(format!("state$: {}", machine.name));
     }
     params.extend(
         own.iter()
@@ -225,8 +223,12 @@ pub(super) fn wrapper(
     );
     let mut out = format!("export function {name}({}): {ret} {{\n", params.join(", "));
     if let (true, Some(machine)) = (reads_state, machine) {
-        out += &format!("  check{}$({}, state);\n", machine.name, string(&name));
-        out += &destructure(machine);
+        out += &format!(
+            "  const {{ {} }} = check{}$({}, state$);\n",
+            field_names(machine),
+            machine.name,
+            string(&name)
+        );
     }
     let (checks, text) = param_checks(
         program,
diff --git a/crates/accord/tests/machines.rs b/crates/accord/tests/machines.rs
index 8ab86d5..6633acb 100644
--- a/crates/accord/tests/machines.rs
+++ b/crates/accord/tests/machines.rs
@@ -127,7 +127,7 @@ fn only_a_proved_pub_machine_is_written_as_typescript() {
     assert!(
         modules[0]
             .source
-            .contains("export function set(state: Dial")
+            .contains("export function set(state$: Dial")
     );
     // A machine without `pub` writes nothing.
     let built = build_of(&proved).expect("the program is accepted");
@@ -150,6 +150,99 @@ pub machine M {
     assert!(refusal.message.contains("start"), "{}", refusal.message);
 }
 
+#[test]
+fn an_enum_and_a_machine_may_not_share_an_exported_type_name() {
+    let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
+    let source = "pub enum M { A }
+pub machine M {
+    state { x: i32 }
+    init start() { next { x: 0 } }
+}
+";
+    let Err(refusal) = build(&[("m.accord".to_string(), source.to_string())], &solvers) else {
+        panic!("colliding type names were built");
+    };
+    assert!(refusal.message.contains("type M"), "{}", refusal.message);
+}
+
+/// Writes the modules `source` builds to a folder of its own and runs
+/// `script`, a module that imports `./m.ts`, in Node; returns its output.
+fn node(source: &str, script: &str) -> String {
+    let solvers = Solvers::from_env().expect("Z3 and cvc5 are available");
+    let built = build(&[("m.accord".to_string(), source.to_string())], &solvers)
+        .expect("the program is accepted");
+    let modules = built.modules.expect("every obligation is proved");
+    let dir = std::env::temp_dir().join(format!(
+        "accord-machines-{}-{}",
+        std::process::id(),
+        script.len()
+    ));
+    let _ = std::fs::remove_dir_all(&dir);
+    std::fs::create_dir_all(&dir).expect("a folder");
+    std::fs::write(dir.join("package.json"), "{\"type\":\"module\"}\n").expect("written");
+    for module in &modules {
+        std::fs::write(dir.join(&module.name), &module.source).expect("written");
+    }
+    std::fs::write(dir.join("run.mjs"), script).expect("written");
+    let node = std::env::var("ACCORD_NODE").unwrap_or_else(|_| "node".to_string());
+    let output = std::process::Command::new(node)
+        .arg("--experimental-strip-types")
+        .arg(dir.join("run.mjs"))
+        .output()
+        .expect("Node runs");
+    assert!(
+        output.status.success(),
+        "{}",
+        String::from_utf8_lossy(&output.stderr)
+    );
+    let _ = std::fs::remove_dir_all(&dir);
+    String::from_utf8(output.stdout).expect("text")
+}
+
+#[test]
+fn a_state_is_read_once_and_the_event_runs_on_what_was_checked() {
+    let source = "pub machine Counter {
+    state { presses: i32 }
+    init start() { next { presses: 0 } }
+    event press() requires presses < 100 { next { presses: presses + 1 } }
+    event keep() { next { } }
+    fn doubled() -> i32 { presses }
+    invariant pressed: presses >= 0 and presses <= 100
+}
+";
+    let out = node(
+        source,
+        "import * as m from './m.ts';
+const attack = () => { let reads = 0; return { get presses() { return reads++ === 0 ? 5 : -5; } }; };
+console.log(JSON.stringify([
+  m.press(attack()).presses,
+  m.keep(attack()).presses,
+  m.doubled(attack()),
+]));
+",
+    );
+    assert_eq!(out.trim(), "[6,5,5]");
+}
+
+#[test]
+fn fields_named_state_and_where_build_and_import() {
+    let source = "pub machine Odd {
+    state { state: i32, where: i32 }
+    init start() { next { state: 0, where: 1 } }
+    event swap() { next { state: where, where: state } }
+    invariant small: state >= 0 and state <= 1 and where >= 0 and where <= 1
+}
+";
+    let out = node(
+        source,
+        "import * as m from './m.ts';
+const s = m.swap(m.start());
+console.log(JSON.stringify(s));
+",
+    );
+    assert_eq!(out.trim(), "{\"state\":1,\"where\":0}");
+}
+
 const STEPPED: &str = "machine Pair {
     state { x: i32, y: i32 }
     init start() { next { x: 0, y: 0 } }

From 4136ce2135fd33bd5329ad4176bb9f102bc992b4 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 21:50:29 -0700
Subject: [PATCH 6/6] docs: say a machine's state is read once

Refs #82
---
 docs/typescript.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/docs/typescript.md b/docs/typescript.md
index 3efd5d6..ef63752 100644
--- a/docs/typescript.md
+++ b/docs/typescript.md
@@ -81,7 +81,7 @@ beside it, as for a function:
 
 An `i64` field is a `number` in the state, and an event that would leave one
 that isn't a safe integer throws a `RangeError`, as a function does for its
-result. A module whose exported names, or their bodies' names, would collide is
+result. A module whose exported names, or their bodies' names, would collide, or whose exported types (enums and machines) share a name, is
 refused, and nothing is written.
 
 ## The boundary
@@ -97,7 +97,11 @@ each exported function checks, in order, before it runs:
 | Each `requires` holds, evaluated with mathematical integers (`bigint`) | `RangeError`, naming the clause |
 
 An event or observer first checks the state it is given, before its own
-parameters: it is an object (`TypeError`), each field has its type and range
+parameters. It reads the state once: the check copies the fields into a fresh
+object, and the event or observer runs on that checked copy, so a getter that
+answers differently each time can't pass the check and then give the body
+another value. The generated names in a state check end in `$`, which no Accord
+name can, so a field may be called `state` or `where`. The check: it is an object (`TypeError`), each field has its type and range
 (`TypeError`, `RangeError`, worded `state.<field> must be …`), and then it
 meets every invariant, then every helper invariant, evaluated with
 mathematical integers (`RangeError`, `state breaks invariant <name>: …`). An