proofs/math/number/proof.bend
bend-collections-laws-math@1.0.0.0 · 261 lines · 77 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
4import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
5import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/src/math/fixed.bend as F
8import bend-collections-laws-math@1.0.0.0/proofs/math/number/egcd.bend as EG
9import bend-collections-laws-math@1.0.0.0/proofs/math/number/bitcount.bend as BC
10import bend-collections-laws-math@1.0.0.0/proofs/math/number/prime.bend as PR
11import bend-collections-laws-math@1.0.0.0/proofs/math/number/fixprime.bend as FP
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as P32
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix64.bend as P64
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbits.bend as FBI
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend as FBY
16
17
18
19
20
21
22
23
24
25
26
27
28def bit_count(+n: Nat) -> SN.BitCount.value(n):
29 BC.bit_count_value(n)
30
31def egcd_gcd(+a: Nat, +b: Nat) -> SN.Egcd.gcd(a, b):
32 EG.egcd_gcd(a, b)
33
34def egcd_bezout(+a: Nat, +b: Nat) -> SN.Egcd.bezout(a, b):
35 EG.egcd_bezout(a, b)
36
37def is_prime(+n: Nat) -> SN.IsPrime.value(n):
38 PR.is_prime_value(n)
39
40
41
42def u32_checked_add(+a: U32, +b: U32) -> SF.CheckedAdd.value(~U32, ~SG.u32_val, ~F.u32_checked_add, 32n, a, b):
43 P32.checked_add(a, b)
44
45def u32_checked_sub(+a: U32, +b: U32) -> SF.CheckedSub.value(~U32, ~SG.u32_val, ~F.u32_checked_sub, a, b):
46 P32.checked_sub(a, b)
47
48def u32_checked_mul(+a: U32, +b: U32) -> SF.CheckedMul.value(~U32, ~SG.u32_val, ~F.u32_checked_mul, 32n, a, b):
49 P32.checked_mul(a, b)
50
51def u32_checked_div(+a: U32, +b: U32) -> SF.CheckedDiv.value(~U32, ~SG.u32_val, ~F.u32_checked_div, a, b):
52 P32.checked_div(a, b)
53
54def u32_checked_rem(+a: U32, +b: U32) -> SF.CheckedRem.value(~U32, ~SG.u32_val, ~F.u32_checked_rem, a, b):
55 P32.checked_rem(a, b)
56
57def u32_checked_pow(+a: U32, +e: U32) -> SF.CheckedPow.value(~U32, ~SG.u32_val, ~F.u32_checked_pow, 32n, a, e):
58 P32.checked_pow(a, e)
59
60def u32_checked_shl(+a: U32, +s: U32) -> SF.CheckedShl.value(~U32, ~SG.u32_val, ~F.u32_checked_shl, 32n, a, s):
61 P32.checked_shl(a, s)
62
63def u32_checked_shr(+a: U32, +s: U32) -> SF.CheckedShr.value(~U32, ~SG.u32_val, ~F.u32_checked_shr, 32n, a, s):
64 P32.checked_shr(a, s)
65
66def u32_wrapping_add(+a: U32, +b: U32) -> SF.WrappingAdd.value(~U32, ~SG.u32_val, ~F.u32_wrapping_add, 32n, a, b):
67 P32.wrapping_add(a, b)
68
69def u32_wrapping_sub(+a: U32, +b: U32) -> SF.WrappingSub.value(~U32, ~SG.u32_val, ~F.u32_wrapping_sub, 32n, a, b):
70 P32.wrapping_sub(a, b)
71
72def u32_wrapping_mul(+a: U32, +b: U32) -> SF.WrappingMul.value(~U32, ~SG.u32_val, ~F.u32_wrapping_mul, 32n, a, b):
73 P32.wrapping_mul(a, b)
74
75def u32_wrapping_pow(+a: U32, +e: U32) -> SF.WrappingPow.value(~U32, ~SG.u32_val, ~F.u32_wrapping_pow, 32n, a, e):
76 P32.wrapping_pow(a, e)
77
78def u32_wrapping_shl(+a: U32, +s: U32) -> SF.WrappingShl.value(~U32, ~SG.u32_val, ~F.u32_wrapping_shl, 32n, a, s):
79 P32.wrapping_shl(a, s)
80
81def u32_wrapping_shr(+a: U32, +s: U32) -> SF.WrappingShr.value(~U32, ~SG.u32_val, ~F.u32_wrapping_shr, 32n, a, s):
82 P32.wrapping_shr(a, s)
83
84def u32_saturating_add(+a: U32, +b: U32) -> SF.SaturatingAdd.value(~U32, ~SG.u32_val, ~F.u32_saturating_add, 32n, a, b):
85 P32.saturating_add(a, b)
86
87def u32_saturating_sub(+a: U32, +b: U32) -> SF.SaturatingSub.value(~U32, ~SG.u32_val, ~F.u32_saturating_sub, a, b):
88 P32.saturating_sub(a, b)
89
90def u32_saturating_mul(+a: U32, +b: U32) -> SF.SaturatingMul.value(~U32, ~SG.u32_val, ~F.u32_saturating_mul, 32n, a, b):
91 P32.saturating_mul(a, b)
92
93def u32_saturating_pow(+a: U32, +e: U32) -> SF.SaturatingPow.value(~U32, ~SG.u32_val, ~F.u32_saturating_pow, 32n, a, e):
94 P32.saturating_pow(a, e)
95
96def u32_overflowing_add_value(+a: U32, +b: U32) -> SF.OverflowingAdd.value(~U32, ~SG.u32_val, ~F.u32_overflowing_add, 32n, a, b):
97 P32.overflowing_add_value(a, b)
98
99def u32_overflowing_add_flag(+a: U32, +b: U32) -> SF.OverflowingAdd.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_add, 32n, a, b):
100 P32.overflowing_add_flag(a, b)
101
102def u32_overflowing_sub_value(+a: U32, +b: U32) -> SF.OverflowingSub.value(~U32, ~SG.u32_val, ~F.u32_overflowing_sub, 32n, a, b):
103 P32.overflowing_sub_value(a, b)
104
105def u32_overflowing_sub_flag(+a: U32, +b: U32) -> SF.OverflowingSub.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_sub, a, b):
106 P32.overflowing_sub_flag(a, b)
107
108def u32_overflowing_mul_value(+a: U32, +b: U32) -> SF.OverflowingMul.value(~U32, ~SG.u32_val, ~F.u32_overflowing_mul, 32n, a, b):
109 P32.overflowing_mul_value(a, b)
110
111def u32_overflowing_mul_flag(+a: U32, +b: U32) -> SF.OverflowingMul.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_mul, 32n, a, b):
112 P32.overflowing_mul_flag(a, b)
113
114def u32_overflowing_pow_value(+a: U32, +e: U32) -> SF.OverflowingPow.value(~U32, ~SG.u32_val, ~F.u32_overflowing_pow, 32n, a, e):
115 P32.overflowing_pow_value(a, e)
116
117def u32_overflowing_pow_flag(+a: U32, +e: U32) -> SF.OverflowingPow.flag(~U32, ~SG.u32_val, ~F.u32_overflowing_pow, 32n, a, e):
118 P32.overflowing_pow_flag(a, e)
119
120def u32_overflowing_shl_value(+a: U32, +s: U32) -> SF.OverflowingShl.value(~U32, ~SG.u32_val, ~F.u32_overflowing_shl, 32n, a, s):
121 P32.overflowing_shl_value(a, s)
122
123def u32_overflowing_shl_flag(+a: U32, +s: U32) -> SF.OverflowingShl.flag(~U32, ~F.u32_overflowing_shl, a, s, 32n):
124 P32.overflowing_shl_flag(a, s)
125
126def u32_overflowing_shr_value(+a: U32, +s: U32) -> SF.OverflowingShr.value(~U32, ~SG.u32_val, ~F.u32_overflowing_shr, 32n, a, s):
127 P32.overflowing_shr_value(a, s)
128
129def u32_overflowing_shr_flag(+a: U32, +s: U32) -> SF.OverflowingShr.flag(~U32, ~F.u32_overflowing_shr, a, s, 32n):
130 P32.overflowing_shr_flag(a, s)
131
132def u32_bit_count(+a: U32) -> SF.BitCount.value(~U32, ~SG.u32_val, ~F.u32_bit_count, 32n, a):
133 FBI.u32_bit_count(a)
134
135def u32_to_bytes_le(+a: U32) -> SF.ToBytes.le(~U32, ~SG.u32_val, ~F.u32_to_bytes_le, 4n, a):
136 FBY.u32_to_le(a)
137
138def u32_to_bytes_be(+a: U32) -> SF.ToBytes.be(~U32, ~SG.u32_val, ~F.u32_to_bytes_be, 4n, a):
139 FBY.u32_to_be(a)
140
141def u32_from_bytes_le(bs: List<&2, U32>) -> SF.FromBytes.le(~U32, ~SG.u32_val, ~F.u32_from_bytes_le, 4n, bs):
142 FBY.u32_from_le(bs)
143
144def u32_from_bytes_be(bs: List<&2, U32>) -> SF.FromBytes.be(~U32, ~SG.u32_val, ~F.u32_from_bytes_be, 4n, bs):
145 FBY.u32_from_be(bs)
146
147def u32_is_prime(+a: U32) -> SF.IsPrime.value(a):
148 FP.is_prime(a)
149
150def u32_next_prime_found(+n: U32, +p: U32, +h: {F.u32_next_prime(n) == Some{p} : Maybe<&2, U32>}) -> SF.NextPrime.found(n, p, h):
151 FP.found(n, p, h)
152
153def u32_next_prime_none(+n: U32, +h: {F.u32_next_prime(n) == None{} : Maybe<&2, U32>}, +m: Nat, +hm: {Nat.is_lt(U32.to_nat(n), m) == True{} : Bool}, +hf: {C.fits(32n, m) == True{} : Bool}) -> SF.NextPrime.none(n, h, m, hm, hf):
154 FP.none(n, h, m, hm, hf)
155
156
157
158def u64_checked_add(+a: WU.U64, +b: WU.U64) -> SF.CheckedAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_add, 64n, a, b):
159 P64.checked_add(a, b)
160
161def u64_checked_sub(+a: WU.U64, +b: WU.U64) -> SF.CheckedSub.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_sub, a, b):
162 P64.checked_sub(a, b)
163
164def u64_checked_mul(+a: WU.U64, +b: WU.U64) -> SF.CheckedMul.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_mul, 64n, a, b):
165 P64.checked_mul(a, b)
166
167def u64_checked_div(+a: WU.U64, +b: WU.U64) -> SF.CheckedDiv.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_div, a, b):
168 P64.checked_div(a, b)
169
170def u64_checked_rem(+a: WU.U64, +b: WU.U64) -> SF.CheckedRem.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_rem, a, b):
171 P64.checked_rem(a, b)
172
173def u64_checked_pow(+a: WU.U64, +e: U32) -> SF.CheckedPow.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_pow, 64n, a, e):
174 P64.checked_pow(a, e)
175
176def u64_checked_shl(+a: WU.U64, +s: U32) -> SF.CheckedShl.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_shl, 64n, a, s):
177 P64.checked_shl(a, s)
178
179def u64_checked_shr(+a: WU.U64, +s: U32) -> SF.CheckedShr.value(~WU.U64, ~SG.u64_val, ~F.u64_checked_shr, 64n, a, s):
180 P64.checked_shr(a, s)
181
182def u64_wrapping_add(+a: WU.U64, +b: WU.U64) -> SF.WrappingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_add, 64n, a, b):
183 P64.wrapping_add(a, b)
184
185def u64_wrapping_sub(+a: WU.U64, +b: WU.U64) -> SF.WrappingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_sub, 64n, a, b):
186 P64.wrapping_sub(a, b)
187
188def u64_wrapping_mul(+a: WU.U64, +b: WU.U64) -> SF.WrappingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_mul, 64n, a, b):
189 P64.wrapping_mul(a, b)
190
191def u64_wrapping_pow(+a: WU.U64, +e: U32) -> SF.WrappingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_pow, 64n, a, e):
192 P64.wrapping_pow(a, e)
193
194def u64_wrapping_shl(+a: WU.U64, +s: U32) -> SF.WrappingShl.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_shl, 64n, a, s):
195 P64.wrapping_shl(a, s)
196
197def u64_wrapping_shr(+a: WU.U64, +s: U32) -> SF.WrappingShr.value(~WU.U64, ~SG.u64_val, ~F.u64_wrapping_shr, 64n, a, s):
198 P64.wrapping_shr(a, s)
199
200def u64_saturating_add(+a: WU.U64, +b: WU.U64) -> SF.SaturatingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_add, 64n, a, b):
201 P64.saturating_add(a, b)
202
203def u64_saturating_sub(+a: WU.U64, +b: WU.U64) -> SF.SaturatingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_sub, a, b):
204 P64.saturating_sub(a, b)
205
206def u64_saturating_mul(+a: WU.U64, +b: WU.U64) -> SF.SaturatingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_mul, 64n, a, b):
207 P64.saturating_mul(a, b)
208
209def u64_saturating_pow(+a: WU.U64, +e: U32) -> SF.SaturatingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_saturating_pow, 64n, a, e):
210 P64.saturating_pow(a, e)
211
212def u64_overflowing_add_value(+a: WU.U64, +b: WU.U64) -> SF.OverflowingAdd.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_add, 64n, a, b):
213 P64.overflowing_add_value(a, b)
214
215def u64_overflowing_add_flag(+a: WU.U64, +b: WU.U64) -> SF.OverflowingAdd.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_add, 64n, a, b):
216 P64.overflowing_add_flag(a, b)
217
218def u64_overflowing_sub_value(+a: WU.U64, +b: WU.U64) -> SF.OverflowingSub.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_sub, 64n, a, b):
219 P64.overflowing_sub_value(a, b)
220
221def u64_overflowing_sub_flag(+a: WU.U64, +b: WU.U64) -> SF.OverflowingSub.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_sub, a, b):
222 P64.overflowing_sub_flag(a, b)
223
224def u64_overflowing_mul_value(+a: WU.U64, +b: WU.U64) -> SF.OverflowingMul.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_mul, 64n, a, b):
225 P64.overflowing_mul_value(a, b)
226
227def u64_overflowing_mul_flag(+a: WU.U64, +b: WU.U64) -> SF.OverflowingMul.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_mul, 64n, a, b):
228 P64.overflowing_mul_flag(a, b)
229
230def u64_overflowing_pow_value(+a: WU.U64, +e: U32) -> SF.OverflowingPow.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_pow, 64n, a, e):
231 P64.overflowing_pow_value(a, e)
232
233def u64_overflowing_pow_flag(+a: WU.U64, +e: U32) -> SF.OverflowingPow.flag(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_pow, 64n, a, e):
234 P64.overflowing_pow_flag(a, e)
235
236def u64_overflowing_shl_value(+a: WU.U64, +s: U32) -> SF.OverflowingShl.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_shl, 64n, a, s):
237 P64.overflowing_shl_value(a, s)
238
239def u64_overflowing_shl_flag(+a: WU.U64, +s: U32) -> SF.OverflowingShl.flag(~WU.U64, ~F.u64_overflowing_shl, a, s, 64n):
240 P64.overflowing_shl_flag(a, s)
241
242def u64_overflowing_shr_value(+a: WU.U64, +s: U32) -> SF.OverflowingShr.value(~WU.U64, ~SG.u64_val, ~F.u64_overflowing_shr, 64n, a, s):
243 P64.overflowing_shr_value(a, s)
244
245def u64_overflowing_shr_flag(+a: WU.U64, +s: U32) -> SF.OverflowingShr.flag(~WU.U64, ~F.u64_overflowing_shr, a, s, 64n):
246 P64.overflowing_shr_flag(a, s)
247
248def u64_bit_count(+a: WU.U64) -> SF.BitCount.value(~WU.U64, ~SG.u64_val, ~F.u64_bit_count, 64n, a):
249 FBI.u64_bit_count(a)
250
251def u64_to_bytes_le(+a: WU.U64) -> SF.ToBytes.le(~WU.U64, ~SG.u64_val, ~F.u64_to_bytes_le, 8n, a):
252 FBY.u64_to_le(a)
253
254def u64_to_bytes_be(+a: WU.U64) -> SF.ToBytes.be(~WU.U64, ~SG.u64_val, ~F.u64_to_bytes_be, 8n, a):
255 FBY.u64_to_be(a)
256
257def u64_from_bytes_le(bs: List<&2, U32>) -> SF.FromBytes.le(~WU.U64, ~SG.u64_val, ~F.u64_from_bytes_le, 8n, bs):
258 FBY.u64_from_le(bs)
259
260def u64_from_bytes_be(bs: List<&2, U32>) -> SF.FromBytes.be(~WU.U64, ~SG.u64_val, ~F.u64_from_bytes_be, 8n, bs):
261 FBY.u64_from_be(bs)