1	import 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	
13	def 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
17	law 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	
27	def 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))