recurrence_laws.bend

bend-kit-scheduler@0.4.1.0 · 90 lines · 10 definitions

1import Base
2import bend-kit-scheduler@0.4.1.0/recurrence.bend as R
3
4law 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
10law 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.
18law 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
27law 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
38law 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.
47law 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.
57law 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.
66law 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.
72law 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.
84law 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>}