spec/lib/numeric.bend
bend-collections-laws-containers@1.0.0.0 · 117 lines · 0 definitions
1import Base
2
3# The 64-bit word model: a Word(n) denotes the natural number of its bits
4# (least significant first), and machine operations are specified through
5# Nat arithmetic (modulo 2^n, unsigned and signed quotients). Shared by the
6# src/math specs (u64, w64, hash) and by the proofs about words and U32s.
7
8# Independent mathematical interpretation. Nat here is a specification value;
9# no public executable conversion of a 64-bit number through Nat is required.
10def bit_value(b: Bool) -> Nat:
11 match b:
12 case False{}:
13 0n
14 case True{}:
15 1n
16
17def unsigned(n: Nat, w: Word(n)) -> Nat:
18 match n:
19 case 0n:
20 0n
21 case 1n+p:
22 match w:
23 case WCon{b, tail}:
24 Nat.add(bit_value(b), Nat.double(unsigned(p, tail)))
25
26def sign_threshold(n: Nat) -> Word(1n+n):
27 match n:
28 case 0n:
29 WCon{True{}, WNil{}}
30 case 1n+p:
31 WCon{False{}, sign_threshold(p)}
32
33def negative(+w: Word(64n)) -> Bool:
34 Cmp.is_ge(Word.cmp(64n, w, sign_threshold(63n)))
35
36def zero(w: Word(64n)) -> Bool:
37 Cmp.is_eq(Word.cmp(64n, w, Word.zero(64n)))
38
39def order(a: Word(64n), b: Word(64n), sign_a: Bool, sign_b: Bool) -> Bool:
40 match sign_a sign_b:
41 case False{} True{}:
42 False{}
43 case True{} False{}:
44 True{}
45 case x y:
46 Cmp.is_le(Word.cmp(64n, a, b))
47
48# These mathematical definitions specify modulo arithmetic through Nat values,
49# independently of the implementation's ripple addition and binary long division.
50def from_nat(n: Nat, +value: Nat) -> Word(n):
51 match n:
52 case 0n:
53 WNil{}
54 case 1n+p:
55 WCon{Nat.is_eq(Nat.mod(value, 2n), 1n), from_nat(p, Nat.div(value, 2n))}
56
57def modulus() -> Nat:
58 Nat.pow(2n, 64n)
59
60# Observe the input constructor before evaluating mathematical division. This
61# has the same from_nat(unsigned(input) / divisor) meaning; the structural guard
62# keeps fixed large denominators from being expanded while input is unknown.
63def unsigned_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
64 match n:
65 case 0n: WNil{}
66 case 1n+ +p:
67 match word:
68 case WCon{bit, tail}:
69 from_nat(1n+p, Nat.div(unsigned(1n+p, WCon{bit, tail}), U32.to_nat(d)))
70
71def negative_quotient(n: Nat, word: Word(n), d: U32) -> Word(n):
72 match n:
73 case 0n: WNil{}
74 case 1n+ +p:
75 match word:
76 case WCon{bit, tail}:
77 from_nat(1n+p, Nat.sub(Nat.pow(2n, 1n+p), Nat.div(Nat.sub(Nat.pow(2n, 1n+p), unsigned(1n+p, WCon{bit, tail})), U32.to_nat(d))))
78
79def quotient_signed(bits: Word(64n), negative: Bool) -> Word(64n):
80 match negative:
81 case False{}:
82 unsigned_quotient(64n, bits, 1000000)
83 case True{}:
84 negative_quotient(64n, bits, 1000000)
85
86# Mathematical multiplication by 2^places, specified without machine shifts.
87def scale_binary(places: Nat, value: Nat) -> Nat:
88 match places:
89 case 0n:
90 value
91 case 1n+p:
92 Nat.double(scale_binary(p, value))
93
94# A 64-bit word from two 32-bit limbs (low first).
95def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):
96 match n:
97 case 0n:
98 b
99 case 1n+p:
100 match a:
101 case WCon{h, tail}:
102 WCon{h, join(p, m, tail, b)}
103
104def pack(low: U32, high: U32) -> Word(64n):
105 match low high:
106 case U32{lo} U32{hi}:
107 join(32n, 32n, lo, hi)
108
109# The low k bits set, the rest clear.
110def mask(+n: Nat, +k: Nat) -> Word(n):
111 match n k:
112 case 0n _:
113 WNil{}
114 case 1n+p 0n:
115 WCon{False{}, mask(p, 0n)}
116 case 1n+p 1n+j:
117 WCon{True{}, mask(p, j)}