1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/math/generic.bend as SG
4	import ../../../spec/math/number.bend as SN
5	import ../../../spec/math/fixed.bend as SF
6	import ../../../src/math/u64.bend as WU
7	import ../../../src/math/fixed.bend as F
8	import ./egcd.bend as EG
9	import ./bitcount.bend as BC
10	import ./prime.bend as PR
11	import ./fixprime.bend as FP
12	import ../typed/fix32.bend as P32
13	import ../typed/fix64.bend as P64
14	import ../typed/fixbits.bend as FBI
15	import ../typed/fixbytes.bend as FBY
16	
17	# Gate for src/math/number.bend and src/math/fixed.bend: every clause of
18	# spec/math/number.bend and spec/math/fixed.bend, under the clause's name,
19	# at U32 (width 32) and U64 (width 64). None assumes a hole or an axiom.
20	#
21	#   spec/math/number.bend  BitCount.value, Egcd.gcd, Egcd.bezout, IsPrime.value
22	#   spec/math/fixed.bend   the checked_ / wrapping_ / saturating_ /
23	#                          overflowing_ families, bit_count, to_bytes /
24	#                          from_bytes (both widths); is_prime, next_prime (U32)
25	
26	# ---- Nat ----
27	
28	def bit_count(+n: Nat) -> SN.BitCount.value(n):
29	  BC.bit_count_value(n)
30	
31	def egcd_gcd(+a: Nat, +b: Nat) -> SN.Egcd.gcd(a, b):
32	  EG.egcd_gcd(a, b)
33	
34	def egcd_bezout(+a: Nat, +b: Nat) -> SN.Egcd.bezout(a, b):
35	  EG.egcd_bezout(a, b)
36	
37	def is_prime(+n: Nat) -> SN.IsPrime.value(n):
38	  PR.is_prime_value(n)
39	
40	# ---- u32 ----
41	
42	def 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	
45	def 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	
48	def 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	
51	def 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	
54	def 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	
57	def 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	
60	def 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	
63	def 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	
66	def 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	
69	def 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	
72	def 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	
75	def 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	
78	def 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	
81	def 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	
84	def 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	
87	def 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	
90	def 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	
93	def 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	
96	def 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	
99	def 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	
102	def 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	
105	def 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	
108	def 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	
111	def 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	
114	def 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	
117	def 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	
120	def 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	
123	def 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	
126	def 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	
129	def 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	
132	def 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	
135	def 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	
138	def 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	
141	def 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	
144	def 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	
147	def u32_is_prime(+a: U32) -> SF.IsPrime.value(a):
148	  FP.is_prime(a)
149	
150	def 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	
153	def 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	# ---- u64 ----
157	
158	def 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	
161	def 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	
164	def 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	
167	def 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	
170	def 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	
173	def 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	
176	def 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	
179	def 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	
182	def 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	
185	def 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	
188	def 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	
191	def 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	
194	def 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	
197	def 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	
200	def 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	
203	def 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	
206	def 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	
209	def 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	
212	def 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	
215	def 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	
218	def 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	
221	def 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	
224	def 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	
227	def 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	
230	def 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	
233	def 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	
236	def 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	
239	def 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	
242	def 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	
245	def 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	
248	def 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	
251	def 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	
254	def 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	
257	def 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	
260	def 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)