1	import Base
2	import ../../../spec/math/generic.bend as SG
3	import ../../../spec/math/instances.bend as SI
4	import ../../../src/math/instances.bend as I
5	
6	# Concrete instances of spec/math/generic.bend's integer clauses at U32,
7	# checked by the proof checker (each normalises both sides). The typed
8	# functions are not proved; these check that the stated clauses are the
9	# right statements (argument order, error mapping, ties, zeros) on small
10	# inputs, next to tools/check_generic.py's randomised tests. Larger values
11	# and U64 are beyond what the checker evaluates in reasonable time, and
12	# isqrt (an F32 estimate: Base's float primitives do not evaluate in the
13	# checker) has none.
14	
15	def gcd() -> SG.Gcd.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 12, 18):
16	  {==}
17	
18	def gcd_zero() -> SG.Gcd.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 0, 7):
19	  {==}
20	
21	def lcm() -> SG.Lcm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 4, 6):
22	  {==}
23	
24	def lcm_zero() -> SG.Lcm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 0, 6):
25	  {==}
26	
27	def gcd_all() -> SG.GcdAll.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, Con{12, Con{18, Con{8, Nil{}}}}):
28	  {==}
29	
30	def gcd_all_empty() -> SG.GcdAll.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, Nil{}):
31	  {==}
32	
33	def lcm_all() -> SG.LcmAll.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, Con{2, Con{3, Con{4, Nil{}}}}):
34	  {==}
35	
36	def lcm_all_zero() -> SG.LcmAll.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, Con{2, Con{0, Con{3, Nil{}}}}):
37	  {==}
38	
39	def iroot() -> SG.Iroot.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 27, 3n):
40	  {==}
41	
42	def iroot_zero_degree() -> SG.Iroot.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 27, 0n):
43	  {==}
44	
45	def ilog() -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 100, 10):
46	  {==}
47	
48	def ilog_zero() -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 0, 10):
49	  {==}
50	
51	def ilog_base_one() -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 100, 1):
52	  {==}
53	
54	def factorial() -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 5):
55	  {==}
56	
57	def factorial_zero() -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 0):
58	  {==}
59	
60	def perm() -> SG.Perm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 5, 2):
61	  {==}
62	
63	def perm_over() -> SG.Perm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 2, 5):
64	  {==}
65	
66	def comb() -> SG.Comb.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 6, 3):
67	  {==}
68	
69	def comb_over() -> SG.Comb.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 3, 6):
70	  {==}
71	
72	def pow_mod() -> SG.PowMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 4, 5):
73	  {==}
74	
75	def pow_mod_zero_modulus() -> SG.PowMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 4, 0):
76	  {==}
77	
78	def mod_inverse() -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 7):
79	  {==}
80	
81	def mod_inverse_not_coprime() -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 2, 4):
82	  {==}
83	
84	def mod_inverse_zero_modulus() -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 0):
85	  {==}
86	
87	def divmod() -> SG.DivMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 17, 5):
88	  {==}
89	
90	def divmod_zero() -> SG.DivMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 17, 0):
91	  {==}
92	
93	def bit_length() -> SG.BitLength.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 255):
94	  {==}
95	
96	def bit_length_zero() -> SG.BitLength.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 0):
97	  {==}
98	
99	def clamp() -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 5, 1, 3):
100	  {==}
101	
102	def clamp_domain() -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 5, 3, 1):
103	  {==}
104	
105	def min() -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 2, 5):
106	  {==}
107	
108	def min_tie() -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 3):
109	  {==}
110	
111	def max() -> SG.Max.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 2, 5):
112	  {==}
113	
114	def abs() -> SG.Abs.identity(~U32, ~I.u32_op, ~I.u32_is, 7):
115	  {==}
116	
117	def sign() -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 9):
118	  {==}
119	
120	def sign_zero() -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 0):
121	  {==}
122	
123	def sum() -> SG.Sum.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, Con{1, Con{2, Con{3, Nil{}}}}):
124	  {==}
125	
126	def prod() -> SG.Prod.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, Con{2, Con{3, Con{0, Nil{}}}}):
127	  {==}
128	
129	def pow() -> SG.Pow.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 3, 4n):
130	  {==}
131	
132	def pow_zero() -> SG.Pow.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 0, 0n):
133	  {==}
134	
135	# the instance laws of spec/math/instances.bend at U32 (Sqrt is F32-based: none)
136	
137	def op_zero() -> SI.Ops.zero(~U32, ~I.u32_op, ~SG.u32_val):
138	  {==}
139	
140	def op_one() -> SI.Ops.one(~U32, ~I.u32_op, ~SG.u32_val):
141	  {==}
142	
143	def op_add() -> SI.Ops.add(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 7, 9, {==}):
144	  {==}
145	
146	def test_add_over() -> SI.Tests.add_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, 7, 9):
147	  {==}
148	
149	def op_sub() -> SI.Ops.sub(~U32, ~I.u32_op, ~SG.u32_val, 9, 7, {==}):
150	  {==}
151	
152	def op_mul() -> SI.Ops.mul(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 7, 9, {==}):
153	  {==}
154	
155	def test_mul_over() -> SI.Tests.mul_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, 7, 9):
156	  {==}
157	
158	def op_quot() -> SI.Ops.quot(~U32, ~I.u32_op, ~SG.u32_val, 17, 5, {==}):
159	  {==}
160	
161	def op_rem() -> SI.Ops.rem(~U32, ~I.u32_op, ~SG.u32_val, 17, 5, {==}):
162	  {==}
163	
164	def op_half() -> SI.Ops.half(~U32, ~I.u32_op, ~SG.u32_val, 17):
165	  {==}
166	
167	def op_mulmod() -> SI.Ops.mulmod(~U32, ~I.u32_op, ~SG.u32_val, 5, 6, 7, {==}, {==}):
168	  {==}
169	
170	def op_pow2() -> SI.Ops.pow2(~U32, ~I.u32_op, ~SG.u32_val, 32n, 5n, {==}):
171	  {==}
172	
173	def op_abs() -> SI.Ops.abs(~U32, ~I.u32_op, 7):
174	  {==}
175	
176	def test_lt() -> SI.Tests.lt(~U32, ~I.u32_is, ~SG.u32_val, 3, 5):
177	  {==}
178	
179	def test_odd() -> SI.Tests.odd(~U32, ~I.u32_is, ~SG.u32_val, 7):
180	  {==}
181	
182	def test_is_zero() -> SI.Tests.is_zero(~U32, ~I.u32_is, ~SG.u32_val, 0):
183	  {==}