spec/lib/numeric.bend

bend-collections-laws-crypto@1.0.0.0 · 117 lines · 15 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)}