1	import Base
2	import ./recurrence.bend as R
3	
4	law invalid_zero:
5	  for previous: Nat
6	  for completion: Nat
7	  for cadence: R.Cadence
8	  {R.plan(previous, completion, 0n, cadence) == None{} : Maybe<&2, R.Plan>}
9	
10	law fixed_delay:
11	  for previous: Nat
12	  for completion: Nat
13	  for p: Nat
14	  {R.plan(previous, completion, 1n+p, R.FixedDelay{}) ==
15	    Some{R.Planned{Nil{}, Nat.add(completion, 1n+p)}} : Maybe<&2, R.Plan>}
16	
17	# These equations specify named policies, phase anchoring, and exact replay prefix.
18	law fixed_rate_skip:
19	  for +previous: Nat
20	  for +completion: Nat
21	  for +p: Nat
22	  {R.plan(previous, completion, 1n+p, R.FixedRate{R.Skip{}}) ==
23	    Some{R.Planned{Nil{}, Nat.add(previous,
24	      Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p))}}
25	    : Maybe<&2, R.Plan>}
26	
27	law fixed_rate_catch_up:
28	  for +previous: Nat
29	  for +completion: Nat
30	  for +p: Nat
31	  for +bound: Nat
32	  {R.plan(previous, completion, 1n+p, R.FixedRate{R.CatchUp{bound}}) ==
33	    Some{R.Planned{R.ticks(Nat.min(bound, Nat.div(Nat.sub(completion, previous), 1n+p)),
34	      previous, 1n+p), Nat.add(previous,
35	      Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p))}}
36	    : Maybe<&2, R.Plan>}
37	
38	law replay_bounded:
39	  for +previous: Nat
40	  for +completion: Nat
41	  for +p: Nat
42	  for +bound: Nat
43	  {Nat.is_le(List.length(&2, Nat, R.replay(R.positive(R.FixedRate{R.CatchUp{bound}},
44	    previous, completion, 1n+p))), bound) == True{} : Bool}
45	
46	# Every positive planner branch returns a deadline strictly beyond completion.
47	law future_deadline:
48	  for +previous: Nat
49	  for +completion: Nat
50	  for +p: Nat
51	  for cadence: R.Cadence
52	  {Nat.is_lt(completion, R.next(R.positive(cadence, previous, completion, 1n+p))) == True{} : Bool}
53	
54	# The last skipped/replayed rate tick is not in the future (when the previous
55	# scheduled tick has completed). Together with future_deadline this proves
56	# the returned deadline is the first future anchored tick, not just any one.
57	law last_due:
58	  for +previous: Nat
59	  for +completion: Nat
60	  for +p: Nat
61	  for h: {Nat.is_le(previous, completion) == True{} : Bool}
62	  {Nat.is_le(Nat.add(previous,
63	    Nat.mul(Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p)), completion) == True{} : Bool}
64	
65	# Addition is monotone on arbitrary Nat: deadlines never wrap below their origin.
66	law no_wrapping:
67	  for +origin: Nat
68	  for period: Nat
69	  {Nat.is_le(origin, Nat.add(origin, period)) == True{} : Bool}
70	
71	# For any one-based index in the exact replay prefix, its anchored tick is due.
72	law replay_tick_due:
73	  for +previous: Nat
74	  for +completion: Nat
75	  for +p: Nat
76	  for +bound: Nat
77	  for +i: Nat
78	  for h: {Nat.is_le(previous, completion) == True{} : Bool}
79	  for hi: {Nat.is_le(i, Nat.min(bound,
80	    Nat.div(Nat.sub(completion, previous), 1n+p))) == True{} : Bool}
81	  {Nat.is_le(Nat.add(previous, Nat.mul(i, 1n+p)), completion) == True{} : Bool}
82	
83	# Exposed validation entry point is connected to the planner used by safety laws.
84	law accepted_positive:
85	  for +previous: Nat
86	  for +completion: Nat
87	  for +p: Nat
88	  for +cadence: R.Cadence
89	  {R.plan(previous, completion, 1n+p, cadence) ==
90	    Some{R.positive(cadence, previous, completion, 1n+p)} : Maybe<&2, R.Plan>}