feat: check machines with the solvers and an explorer

conformance/README.md

@@ -22,6 +22,24 @@ listed after every obligation, in source order; `error` means the file must
 be rejected before any obligation is generated. A case named `x-fault` or `x-<what>-fault`
 plants a fault in the correct case `x`, and must be refuted or fail.
 
+A machine's obligations come in source order with its functions':
+
+- for each `init`, in order: that some input is allowed, when it has a
+  `requires`; that its state meets every invariant and helper invariant;
+  then its arithmetic and decision tables, as a function's;
+- for each event, in order: that it preserves every invariant and helper
+  invariant; that it is allowed in some state an `init` reaches; then its
+  arithmetic and decision tables, as a function's, each assuming the
+  invariants and helper invariants;
+- its observers, as functions.
+
+An invariant is refuted only by a trace from an `init`, which the explorer
+finds and the interpreter replays. Where the solvers refute an obligation
+from a state no trace reaches, its outcome is `not_inductive`. An event is
+allowed in a reachable state when the explorer reaches one where its
+`requires` holds. A machine's `example` is listed as `passed` or `failed`
+with the other examples.
+
 `cargo test --test conformance` runs every case through both solvers. It
 needs Z3 and cvc5: on the `PATH` as `z3` and `cvc5`, or named by the
 `ACCORD_Z3` and `ACCORD_CVC5` environment variables. Without them the

conformance/cases/machine-dead-event-fault.accord

@@ -0,0 +1,33 @@
+// expect: proved, proved, proved, proved, proved, proved, refuted
+// `reset` needs more presses than the invariant allows, so no state the
+// machine reaches allows it: the solvers prove that none does.
+enum Light { Off, On }
+
+machine Switch {
+    state {
+        light: Light,
+        presses: i32,
+    }
+
+    init start() {
+        next { light: Off, presses: 0 }
+    }
+
+    event press()
+        requires presses < 100
+    {
+        if light == Off {
+            next { light: On, presses: presses + 1 }
+        } else {
+            next { light: Off, presses: presses + 1 }
+        }
+    }
+
+    event reset()
+        requires presses > 100
+    {
+        next { light: Off, presses: 0 }
+    }
+
+    invariant pressed: presses >= 0 and presses <= 100
+}

conformance/cases/machine-decide.accord

@@ -0,0 +1,25 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved
+// An event whose body is a decision table: every state the invariant allows
+// reaches a row, each row can be the first to hold, and each row's addition
+// stays within `i32`.
+enum Light { Off, On }
+
+machine Switch {
+    state {
+        light: Light,
+        presses: i32,
+    }
+
+    init start() {
+        next { light: Off, presses: 0 }
+    }
+
+    event press()
+        requires presses < 100
+    decide {
+        | light == Off => next { light: On, presses: presses + 1 }
+        | otherwise    => next { light: Off, presses: presses + 1 }
+    }
+
+    invariant pressed: presses >= 0 and presses <= 100
+}

conformance/cases/machine-event-ensures.accord

@@ -0,0 +1,17 @@
+// expect: error
+// An event takes `intent` and `requires` only: it has no result to ensure.
+machine Switch {
+    state {
+        presses: i32,
+    }
+
+    init start() {
+        next { presses: 0 }
+    }
+
+    event press()
+        ensures presses >= 0
+    {
+        next { presses: presses + 1 }
+    }
+}

conformance/cases/machine-fault.accord

@@ -0,0 +1,32 @@
+// expect: proved, refuted, proved, proved, proved, passed
+// `press` is allowed at 100 presses, so a run of 101 presses breaks the
+// invariant.
+enum Light { Off, On }
+
+machine Switch {
+    state {
+        light: Light,
+        presses: i32,
+    }
+
+    init start() {
+        next { light: Off, presses: 0 }
+    }
+
+    event press()
+        requires presses <= 100
+    {
+        if light == Off {
+            next { light: On, presses: presses + 1 }
+        } else {
+            next { light: Off, presses: presses + 1 }
+        }
+    }
+
+    invariant pressed: presses >= 0 and presses <= 100
+}
+
+example Switch
+    start()
+    press()
+    gives light == On and presses == 1

conformance/cases/machine-helped.accord

@@ -0,0 +1,23 @@
+// expect: proved, proved, proved, proved, proved
+// The machine of `machine-unhelped.accord`, with the helper invariant that `y`
+// moves with `x`: the invariant is now proved inductive.
+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
+
+    helper invariant together: x == y
+}

conformance/cases/machine-init-fault.accord

@@ -0,0 +1,31 @@
+// expect: proved, refuted, proved, proved, proved, proved
+// `broken` starts past the bound the invariant sets, so the run that is only
+// `broken()` breaks it.
+enum Light { Off, On }
+
+machine Switch {
+    state {
+        light: Light,
+        presses: i32,
+    }
+
+    init start() {
+        next { light: Off, presses: 0 }
+    }
+
+    init broken() {
+        next { light: Off, presses: 101 }
+    }
+
+    event press()
+        requires presses < 100
+    {
+        if light == Off {
+            next { light: On, presses: presses + 1 }
+        } else {
+            next { light: Off, presses: presses + 1 }
+        }
+    }
+
+    invariant pressed: presses >= 0 and presses <= 100
+}

conformance/cases/machine-init-missing-field.accord

@@ -0,0 +1,12 @@
+// expect: error
+// An `init` must give every field a value: `start` leaves `presses` out.
+machine Switch {
+    state {
+        on: Bool,
+        presses: i32,
+    }
+
+    init start() {
+        next { on: false }
+    }
+}

conformance/cases/machine-init-overflow-fault.accord

@@ -0,0 +1,17 @@
+// expect: proved, proved, refuted
+// `start(2147483647)` overflows in its own addition; the invariant is proved
+// assuming the addition stays in range, and the addition's obligation is
+// refuted by that run.
+machine Counter {
+    state {
+        value: i32,
+    }
+
+    init start(from: i32)
+        requires from >= 0
+    {
+        next { value: from + 1 }
+    }
+
+    invariant positive: value > 0
+}

conformance/cases/machine-invariant-call.accord

@@ -0,0 +1,17 @@
+// expect: error
+// An invariant is a specification, and no specification can call a function.
+machine Switch {
+    state {
+        presses: i32,
+    }
+
+    init start() {
+        next { presses: 0 }
+    }
+
+    fn many() -> Bool {
+        presses > 10
+    }
+
+    invariant few: not many()
+}

conformance/cases/machine-invariant-twice.accord

@@ -0,0 +1,16 @@
+// expect: error
+// Invariants are named so a run can say which one it breaks: two can't
+// share a name.
+machine Switch {
+    state {
+        presses: i32,
+    }
+
+    init start() {
+        next { presses: 0 }
+    }
+
+    invariant bounded: presses >= 0
+
+    invariant bounded: presses <= 100
+}

conformance/cases/machine-next-twice.accord

@@ -0,0 +1,11 @@
+// expect: error
+// A `next` gives each field one value.
+machine Switch {
+    state {
+        presses: i32,
+    }
+
+    init start() {
+        next { presses: 0, presses: 1 }
+    }
+}

conformance/cases/machine-no-init.accord

@@ -0,0 +1,11 @@
+// expect: error
+// A machine needs a way to start.
+machine Switch {
+    state {
+        presses: i32,
+    }
+
+    event press() {
+        next { presses: presses + 1 }
+    }
+}

conformance/cases/machine-observer.accord

@@ -0,0 +1,30 @@
+// expect: proved, proved, proved, proved, proved, proved
+// `press` asks the observer `at_limit` whether to count, and knows its answer
+// only through its contract. The observer's own `ensures` is proved too.
+machine Counter {
+    state {
+        presses: i32,
+    }
+
+    init start() {
+        next { presses: 0 }
+    }
+
+    event press() {
+        if at_limit() {
+            next { }
+        } else {
+            next { presses: presses + 1 }
+        }
+    }
+
+    /// Whether another press would pass the limit.
+    fn at_limit() -> Bool
+        ensures result implies presses == 100
+        ensures presses == 100 implies result
+    {
+        presses == 100
+    }
+
+    invariant pressed: presses >= 0 and presses <= 100
+}

conformance/cases/machine-overflow-fault.accord

@@ -0,0 +1,18 @@
+// expect: proved, proved, proved, refuted
+// Without its `requires`, the third increment overflows `i32`.
+machine Counter {
+    state {
+        value: i32,
+    }
+
+    init near_top() {
+        next { value: 2147483645 }
+    }
+
+    event increment()
+    {
+        next { value: value + 1 }
+    }
+
+    invariant non_negative: value >= 0
+}

conformance/cases/machine-overflow-step-fault.accord

@@ -0,0 +1,21 @@
+// expect: proved, proved, proved, refuted
+// `increment` overflows from the state `start` gives. That is a failure of
+// the addition, and only the addition's obligation reports it: an event's
+// invariants are proved assuming its arithmetic stays in range, since that
+// is an obligation of its own.
+machine Counter {
+    state {
+        value: i32,
+    }
+
+    init start() {
+        next { value: 2147483647 }
+    }
+
+    event increment()
+    {
+        next { value: value + 1 }
+    }
+
+    invariant capped: value <= 2147483647
+}

conformance/cases/machine-overflow.accord

@@ -0,0 +1,19 @@
+// expect: proved, proved, proved, proved
+// A counter that starts near the top of `i32` and stops below it.
+machine Counter {
+    state {
+        value: i32,
+    }
+
+    init near_top() {
+        next { value: 2147483645 }
+    }
+
+    event increment()
+        requires value < 2147483647
+    {
+        next { value: value + 1 }
+    }
+
+    invariant non_negative: value >= 0
+}

conformance/cases/machine-param-field.accord

@@ -0,0 +1,11 @@
+// expect: error
+// A parameter can't share a field's name.
+machine Switch {
+    state {
+        presses: i32,
+    }
+
+    init start(presses: i32) {
+        next { presses: presses }
+    }
+}