proofs/lib/lemmas/spec/numeric.bend
bend-collections-laws-containers@1.0.0.0 · 68 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/spec/lib/numeric.bend as W
4
5# The word model lives in spec/lib/numeric.bend; its names are kept here as
6# one-line aliases for the proofs that use them, next to the cache model's
7# Int64 interpretation (expiry, deadlines).
8
9def bit_value(b: Bool) -> Nat:
10 W.bit_value(b)
11
12def unsigned(n: Nat, w: Word(n)) -> Nat:
13 W.unsigned(n, w)
14
15def sign_threshold(n: Nat) -> Word(1n+n):
16 W.sign_threshold(n)
17
18def negative(+w: Word(64n)) -> Bool:
19 W.negative(w)
20
21def zero(w: Word(64n)) -> Bool:
22 W.zero(w)
23
24def order(a: Word(64n), b: Word(64n), sign_a: Bool, sign_b: Bool) -> Bool:
25 W.order(a, b, sign_a, sign_b)
26
27def expired(deadline: T.Int64, now: T.Int64) -> Bool:
28 match deadline now:
29 case T.I64{+a} T.I64{+b}:
30 Bool.not(zero(a)) && order(a, b, negative(a), negative(b))
31
32def from_nat(n: Nat, +value: Nat) -> Word(n):
33 W.from_nat(n, value)
34
35def modulus() -> Nat:
36 W.modulus()
37
38def unsigned_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
39 W.unsigned_quotient(n, word, d)
40
41def negative_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
42 W.negative_quotient(n, word, d)
43
44def quotient_signed(bits: Word(64n), negative: Bool) -> Word(64n):
45 W.quotient_signed(bits, negative)
46
47def milliseconds(duration: T.Int64) -> T.Int64:
48 T.I64{+bits} = duration
49 T.I64{quotient_signed(bits, negative(bits))}
50
51def add(a: T.Int64, b: T.Int64) -> T.Int64:
52 match a b:
53 case T.I64{x} T.I64{y}:
54 T.I64{from_nat(64n, Nat.add(unsigned(64n, x), unsigned(64n, y)))}
55
56def expiry_choose(now: T.Int64, duration: T.Int64, forever: Bool) -> T.Int64:
57 match forever:
58 case True{}:
59 T.I64{Word.zero(64n)}
60 case False{}:
61 add(now, milliseconds(duration))
62
63def deadline(now: T.Int64, duration: T.Int64) -> T.Int64:
64 T.I64{+bits} = duration
65 expiry_choose(now, T.I64{bits}, zero(bits))
66
67def scale_binary(places: Nat, value: Nat) -> Nat:
68 W.scale_binary(places, value)