1	import Base
2	import ../src/wide.bend as W
3	import ../src/time.bend as Time
4	import ../spec/numeric.bend as S
5	import ../types/model.bend as T
6	import ./signed_division.bend as Signed
7	import ./numeric.bend as Numeric
8	import ./modular_addition.bend as Addition
9	
10	def 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	
16	def 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.
25	def 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))