proofs/lib/lemmas/src/time.bend

bend-collections-laws-containers@1.0.0.0 · 41 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
4
5def add(a: T.Int64, b: T.Int64) -> T.Int64:
6  match a b:
7    case T.I64{x} T.I64{y}:
8      T.I64{W.add(x, y)}
9
10def milliseconds(ns: T.Int64) -> T.Int64:
11  T.I64{w} = ns
12  T.I64{W.milliseconds(w)}
13
14def is_zero(t: T.Int64) -> Bool:
15  T.I64{w} = t
16  W.is_zero(64n, w)
17
18def deadline_choose(now: T.Int64, ns: T.Int64, immortal: Bool) -> T.Int64:
19  match immortal:
20    case True{}:
21      T.I64{W.zero()}
22    case False{}:
23      add(now, milliseconds(ns))
24
25def deadline(now: T.Int64, +ns: T.Int64) -> T.Int64:
26  deadline_choose(now, ns, is_zero(ns))
27
28def le(a: T.Int64, b: T.Int64) -> Bool:
29  match a b:
30    case T.I64{x} T.I64{y}:
31      W.le(x, y)
32
33def expired_choose(d: T.Int64, now: T.Int64, immortal: Bool) -> Bool:
34  match immortal:
35    case True{}:
36      False{}
37    case False{}:
38      le(d, now)
39
40def expired(+deadline: T.Int64, now: T.Int64) -> Bool:
41  expired_choose(deadline, now, is_zero(deadline))