def unsigned_milliseconds

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/division_quotient.bend:67

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

67# Connection to the actual duration core and the public independent numeric
68# specification's nonnegative branch. Negative sign handling is separate.
69def unsigned_milliseconds(+word: Word(64n)) -> {W.unsigned_milliseconds(word) == S.quotient_signed(word, False{}) : Word(64n)}:
70  Equal.trans(Word(64n), W.unsigned_milliseconds(word), quotient(64n, W.div_million(64n, word)), S.quotient_signed(word, False{}), native_projection(W.div_million(64n, word)), actual(64n, word))