law last_due

bend-kit-scheduler@0.4.1.0 · recurrence_laws.bend:54

import Base

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}