recurrence_proof.bend
bend-kit-scheduler@0.4.1.0 · 100 lines · 4 definitions
1import Base
2import bend-mathlib@0.7.4.0/nat.bend as N
3import bend-kit-scheduler@0.4.1.0/recurrence.bend as R
4import bend-kit-scheduler@0.4.1.0/recurrence_laws.bend as Laws
5
6def Laws.invalid_zero(previous, completion, cadence):
7 {==}
8
9def Laws.fixed_delay(previous, completion, p):
10 {==}
11
12def Laws.fixed_rate_skip(previous, completion, p):
13 {==}
14
15def Laws.fixed_rate_catch_up(previous, completion, p, bound):
16 {==}
17
18def ticks_length(count: Nat, +previous: Nat, +period: Nat)
19 -> {List.length(&2, Nat, R.ticks(count, previous, period)) == count : Nat}:
20 match count:
21 case 0n:
22 {==}
23 case 1n+n:
24 %ticks_length(n, Nat.add(previous, period), period) : {1n+List.length(&2, Nat,
25 R.ticks(n, Nat.add(previous, period), period)) == 1n+_ : Nat}
26 {==}
27
28def Laws.replay_bounded(previous, completion, p, bound):
29 %Equal.sym(Nat, List.length(&2, Nat, R.ticks(
30 Nat.min(bound, Nat.div(Nat.sub(completion, previous), 1n+p)), previous, 1n+p)),
31 Nat.min(bound, Nat.div(Nat.sub(completion, previous), 1n+p)),
32 ticks_length(Nat.min(bound, Nat.div(Nat.sub(completion, previous), 1n+p)), previous, 1n+p))
33 : {Nat.is_le(_, bound) == True{} : Bool}
34 N.min_le_left(bound, Nat.div(Nat.sub(completion, previous), 1n+p))
35
36def quotient_future(+elapsed: Nat, +p: Nat)
37 -> N.lt(elapsed, Nat.mul(1n+Nat.div(elapsed, 1n+p), 1n+p)):
38 %N.not_is_le(Nat.mul(1n+Nat.div(elapsed, 1n+p), 1n+p), elapsed)
39 : {_ == True{} : Bool}
40 %N.le_div_iff_mul_le(1n+Nat.div(elapsed, 1n+p), elapsed, p)
41 : {Bool.not(_) == True{} : Bool}
42 %Equal.sym(Bool, Nat.is_le(1n+Nat.div(elapsed, 1n+p), Nat.div(elapsed, 1n+p)),
43 False{}, N.not_le_of_lt(Nat.div(elapsed, 1n+p), 1n+Nat.div(elapsed, 1n+p),
44 N.lt_succ_self(Nat.div(elapsed, 1n+p)))) : {Bool.not(_) == True{} : Bool}
45 {==}
46
47def fixed_rate_future(+previous: Nat, +completion: Nat, +p: Nat,
48 order: Or(N.le(previous, completion), N.le(completion, previous)))
49 -> N.lt(completion,
50 Nat.add(previous, Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p))):
51 match order:
52 case Inl{h}:
53 %N.add_sub_of_le(previous, completion, h)
54 : N.lt(_, Nat.add(previous,
55 Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p)))
56 N.add_lt_add_left(Nat.sub(completion, previous),
57 Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p), previous,
58 quotient_future(Nat.sub(completion, previous), p))
59 case Inr{+h}:
60 %Equal.sym(Nat, Nat.sub(completion, previous), 0n,
61 N.sub_eq_zero_of_le(completion, previous, h))
62 : N.lt(completion, Nat.add(previous, Nat.mul(1n+Nat.div(_, 1n+p), 1n+p)))
63 %Equal.sym(Nat, Nat.add(p, 0n), p, N.add_zero(p))
64 : N.lt(completion, Nat.add(previous, 1n+_))
65 N.lt_of_le_of_lt(completion, previous, Nat.add(previous, 1n+p), h,
66 N.lt_add_of_pos_right(previous, p))
67
68def Laws.future_deadline(previous, completion, p, cadence):
69 match cadence:
70 case R.FixedDelay{}:
71 N.lt_add_of_pos_right(completion, p)
72 case R.FixedRate{policy}:
73 fixed_rate_future(previous, completion, p, N.le_total(previous, completion))
74
75def due_tick(+previous: Nat, +completion: Nat, +p: Nat, +i: Nat,
76 h: N.le(previous, completion), hi: N.le(i, Nat.div(Nat.sub(completion, previous), 1n+p)))
77 -> N.le(Nat.add(previous, Nat.mul(i, 1n+p)), completion):
78 %N.sub_add_cancel(completion, previous, h)
79 : N.le(Nat.add(previous, Nat.mul(i, 1n+p)), _)
80 %N.add_comm(previous, Nat.sub(completion, previous))
81 : N.le(Nat.add(previous, Nat.mul(i, 1n+p)), _)
82 N.add_le_add_left(Nat.mul(i, 1n+p), Nat.sub(completion, previous), previous,
83 (%N.le_div_iff_mul_le(i, Nat.sub(completion, previous), p)
84 : {_ == True{} : Bool}; hi))
85
86def Laws.last_due(previous, completion, p, h):
87 due_tick(previous, completion, p, Nat.div(Nat.sub(completion, previous), 1n+p), h,
88 N.le_refl(Nat.div(Nat.sub(completion, previous), 1n+p)))
89
90def Laws.no_wrapping(origin, period):
91 N.le_add_right(origin, period)
92
93def Laws.replay_tick_due(previous, completion, p, bound, i, h, hi):
94 due_tick(previous, completion, p, i, h,
95 N.le_trans(i, Nat.min(bound, Nat.div(Nat.sub(completion, previous), 1n+p)),
96 Nat.div(Nat.sub(completion, previous), 1n+p), hi,
97 N.min_le_right(bound, Nat.div(Nat.sub(completion, previous), 1n+p))))
98
99def Laws.accepted_positive(previous, completion, p, cadence):
100 {==}