proofs/lib/lemmas/proofs/duration_refinement.bend
bend-collections-laws-containers@1.0.0.0 · 29 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/signed_division.bend as Signed
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as Numeric
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as Addition
9
10def milliseconds(ns: T.Int64) -> {Time.milliseconds(ns) == S.milliseconds(ns) : T.Int64}:
11 match ns:
12 case T.I64{+word}:
13 %Equal.sym(Bool, S.negative(word), W.last(64n, word), Numeric.sign_threshold_correspondence(63n, word)) : {T.I64{W.milliseconds(word)} == T.I64{S.quotient_signed(word, _)} : T.Int64}
14 Equal.cong(Word(64n), T.Int64, w => T.I64{w}, W.milliseconds(word), S.quotient_signed(word, W.last(64n, word)), Signed.branch(word, W.last(64n, word), {==}))
15
16def choose(+now: T.Int64, +ns: T.Int64, immortal: Bool) -> {Time.deadline_choose(now, ns, immortal) == S.expiry_choose(now, ns, immortal) : T.Int64}:
17 match immortal:
18 case True{}: {==}
19 case False{}:
20 Equal.trans(T.Int64, Time.add(now, Time.milliseconds(ns)), S.add(now, Time.milliseconds(ns)), S.add(now, S.milliseconds(ns)), Addition.time_add_refines(now, Time.milliseconds(ns)), Equal.cong(T.Int64, T.Int64, duration => S.add(now, duration), Time.milliseconds(ns), S.milliseconds(ns), milliseconds(ns)))
21
22# All 64-bit durations and samples, including minimum signed duration, wrapped
23# sums, sub-millisecond truncation, and the original zero sentinel. No bounds or
24# successful-conversion premises are imposed on native bit-pattern inputs.
25def deadline(+now: T.Int64, ns: T.Int64) -> {Time.deadline(now, ns) == S.deadline(now, ns) : T.Int64}:
26 match ns:
27 case T.I64{+word}:
28 %Equal.sym(Bool, S.zero(word), W.is_zero(64n, word), Numeric.zero_comparison_correspondence(64n, word)) : {Time.deadline(now, T.I64{word}) == S.expiry_choose(now, T.I64{word}, _) : T.Int64}
29 choose(now, T.I64{word}, W.is_zero(64n, word))