feat: write a proved machine as TypeScript

conformance/typescript/machine/out/switch.ts

@@ -0,0 +1,98 @@
+// 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): Switch {
+  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`);
+  }
+  return { light, presses };
+}
+
+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 {
+  const { light, presses } = checkSwitch$("press", 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 {
+  const { light, presses } = checkSwitch$("turnOff", state$);
+  return turnOff$(light, presses);
+}
+
+function turnOff$(light: Light, presses: number): Switch {
+  return { light: "off", presses: presses };
+}
+
+export function atLimit(state$: Switch): boolean {
+  const { light, presses } = checkSwitch$("atLimit", state$);
+  return atLimit$(light, presses);
+}
+
+function atLimit$(light: Light, presses: number): boolean {
+  return presses === 100;
+}

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

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
+}

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(),

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> {