1	import Base
2	import bend-mathlib@0.7.4.0/nat.bend as N
3	import ./recurrence.bend as R
4	import ./recurrence_laws.bend as Laws
5	
6	def Laws.invalid_zero(previous, completion, cadence):
7	  {==}
8	
9	def Laws.fixed_delay(previous, completion, p):
10	  {==}
11	
12	def Laws.fixed_rate_skip(previous, completion, p):
13	  {==}
14	
15	def Laws.fixed_rate_catch_up(previous, completion, p, bound):
16	  {==}
17	
18	def 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	
28	def 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	
36	def 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	
47	def 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	
68	def 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	
75	def 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	
86	def 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	
90	def Laws.no_wrapping(origin, period):
91	  N.le_add_right(origin, period)
92	
93	def 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	
99	def Laws.accepted_positive(previous, completion, p, cadence):
100	  {==}