src/machine.bend

bend-lawful-stdlib@0.1.0.0 · 32 lines · 2 definitions

1import Base
2
3# machine.bend: invariants of state machines, over every input sequence.
4#
5#   import ./machine.bend as M
6#   M.run(~S, ~I, ~step, s, inputs)
7#
8# A state machine is a step ~step: S -> I -> S, and run folds it over a
9# list of inputs with Base's List.foldl. run_inv: if one step keeps an
10# invariant Inv, so does every run, over every input list. A caller
11# proves the one-step fact and gets the rest.
12
13def run(~S: Data, ~I: Data, ~step: S -> I -> S, s: S, xs: List<&2, I>) -> S:
14  List.foldl(~&2, ~I, ~S, ~step, xs, s)
15
16# a step that keeps Inv keeps it over any input list
17law run_inv:
18  for ~S: Data
19  for ~I: Data
20  for ~step: S -> I -> S
21  for ~Inv: S -> Type
22  for ~keep: @s: S -> @i: I -> Inv(s) -> Inv(step(s, i))
23  for xs: List<&2, I>
24  for +s: S
25  Inv(s) -> Inv(run(~S, ~I, ~step, s, xs))
26
27def run_inv(S, I, step, Inv, keep, xs, s):
28  match xs:
29    case Nil{}:
30      k => k
31    case +h <> t:
32      k => run_inv(~S, ~I, ~step, ~Inv, ~keep, t, step(s, h))(keep(s, h, k))