proofs/math/typed/examples.bend

bend-collections-laws-math@1.0.0.0 · 183 lines · 56 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
3import bend-collections-laws-math@1.0.0.0/spec/math/instances.bend as SI
4import bend-collections-laws-math@1.0.0.0/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
15def gcd() -> SG.Gcd.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 12, 18):
16  {==}
17
18def gcd_zero() -> SG.Gcd.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 0, 7):
19  {==}
20
21def lcm() -> SG.Lcm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 4, 6):
22  {==}
23
24def lcm_zero() -> SG.Lcm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 0, 6):
25  {==}
26
27def 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
30def gcd_all_empty() -> SG.GcdAll.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, Nil{}):
31  {==}
32
33def 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
36def 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
39def iroot() -> SG.Iroot.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 27, 3n):
40  {==}
41
42def iroot_zero_degree() -> SG.Iroot.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 27, 0n):
43  {==}
44
45def ilog() -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 100, 10):
46  {==}
47
48def ilog_zero() -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 0, 10):
49  {==}
50
51def ilog_base_one() -> SG.Ilog.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 100, 1):
52  {==}
53
54def factorial() -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 5):
55  {==}
56
57def factorial_zero() -> SG.Factorial.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 0):
58  {==}
59
60def perm() -> SG.Perm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 5, 2):
61  {==}
62
63def perm_over() -> SG.Perm.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 2, 5):
64  {==}
65
66def comb() -> SG.Comb.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 6, 3):
67  {==}
68
69def comb_over() -> SG.Comb.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 3, 6):
70  {==}
71
72def pow_mod() -> SG.PowMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 4, 5):
73  {==}
74
75def 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
78def mod_inverse() -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 7):
79  {==}
80
81def mod_inverse_not_coprime() -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 2, 4):
82  {==}
83
84def mod_inverse_zero_modulus() -> SG.ModInverse.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 0):
85  {==}
86
87def divmod() -> SG.DivMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 17, 5):
88  {==}
89
90def divmod_zero() -> SG.DivMod.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 17, 0):
91  {==}
92
93def bit_length() -> SG.BitLength.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 255):
94  {==}
95
96def bit_length_zero() -> SG.BitLength.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 0):
97  {==}
98
99def clamp() -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 5, 1, 3):
100  {==}
101
102def clamp_domain() -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 5, 3, 1):
103  {==}
104
105def min() -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 2, 5):
106  {==}
107
108def min_tie() -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 3, 3):
109  {==}
110
111def max() -> SG.Max.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 2, 5):
112  {==}
113
114def abs() -> SG.Abs.identity(~U32, ~I.u32_op, ~I.u32_is, 7):
115  {==}
116
117def sign() -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 9):
118  {==}
119
120def sign_zero() -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 0):
121  {==}
122
123def 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
126def 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
129def pow() -> SG.Pow.checked(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, 32n, 3, 4n):
130  {==}
131
132def 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
137def op_zero() -> SI.Ops.zero(~U32, ~I.u32_op, ~SG.u32_val):
138  {==}
139
140def op_one() -> SI.Ops.one(~U32, ~I.u32_op, ~SG.u32_val):
141  {==}
142
143def op_add() -> SI.Ops.add(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 7, 9, {==}):
144  {==}
145
146def test_add_over() -> SI.Tests.add_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, 7, 9):
147  {==}
148
149def op_sub() -> SI.Ops.sub(~U32, ~I.u32_op, ~SG.u32_val, 9, 7, {==}):
150  {==}
151
152def op_mul() -> SI.Ops.mul(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, 7, 9, {==}):
153  {==}
154
155def test_mul_over() -> SI.Tests.mul_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, 7, 9):
156  {==}
157
158def op_quot() -> SI.Ops.quot(~U32, ~I.u32_op, ~SG.u32_val, 17, 5, {==}):
159  {==}
160
161def op_rem() -> SI.Ops.rem(~U32, ~I.u32_op, ~SG.u32_val, 17, 5, {==}):
162  {==}
163
164def op_half() -> SI.Ops.half(~U32, ~I.u32_op, ~SG.u32_val, 17):
165  {==}
166
167def op_mulmod() -> SI.Ops.mulmod(~U32, ~I.u32_op, ~SG.u32_val, 5, 6, 7, {==}, {==}):
168  {==}
169
170def op_pow2() -> SI.Ops.pow2(~U32, ~I.u32_op, ~SG.u32_val, 32n, 5n, {==}):
171  {==}
172
173def op_abs() -> SI.Ops.abs(~U32, ~I.u32_op, 7):
174  {==}
175
176def test_lt() -> SI.Tests.lt(~U32, ~I.u32_is, ~SG.u32_val, 3, 5):
177  {==}
178
179def test_odd() -> SI.Tests.odd(~U32, ~I.u32_is, ~SG.u32_val, 7):
180  {==}
181
182def test_is_zero() -> SI.Tests.is_zero(~U32, ~I.u32_is, ~SG.u32_val, 0):
183  {==}