spec/math/fixed.bend

bend-collections-laws-math@1.0.0.0 · 255 lines · 50 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/src/math/fixed.bend as F
4import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN
5
6# Specification of src/math/fixed.bend: fixed-width integer operations as
7# Rust defines them for u32/u64 (python_style_math_stdlib_design.pdf
8# section 2.6: checked_add, wrapping_add, saturating_add, overflowing_add
9# families; section 3.2 bit_count and to_bytes/from_bytes; section 10
10# is_prime / next_prime).
11#
12# Each clause is stated once over an instance model and read at U32
13# (U32.to_nat, width 32) and U64 (spec/math/w64.bend's value, width 64):
14#   val: T -> Nat, the value;  w, the width;  f, the function.
15# Widths are written with C.fits, C.low, C.high and C.shift (spec/lib/
16# common.bend): the checker never forms 2^32 or 2^64.
17#
18#   family        clauses (Rust u32/u64 documentation)
19#   checked_*     CheckedAdd/Sub/Mul/Div/Rem/Pow/Shl/Shr.value: the exact
20#                 result when it fits (divisor nonzero, shift below w),
21#                 None otherwise
22#   wrapping_*    WrappingAdd/Mul/Pow/Shl/Shr.value: the result mod 2^w
23#                 (shift amount mod w); WrappingSub.value: r + b ==
24#                 a + 2^w * [a < b]
25#   saturating_*  SaturatingAdd/Mul/Pow.value: the result when it fits,
26#                 else the largest value (fits w, +1 does not);
27#                 SaturatingSub.value: a - b floored at 0
28#   overflowing_* OverflowingX.value (the wrapping value) and
29#                 OverflowingX.flag (the result did not fit / a < b /
30#                 shift >= w)
31#   bit_count     BitCount.value: spec/math/number.bend's ones(w, value)
32#   is_prime      IsPrime.value (U32): spec/math/number.bend's prime
33#   next_prime    NextPrime.found, NextPrime.none (U32): the least prime
34#                 above n below 2^32, or None when there is none
35#   to_bytes_*    ToBytes.le, ToBytes.be: the w/8 base-256 digits
36#   from_bytes_*  FromBytes.le, FromBytes.be: the value of exactly w/8
37#                 digits below 256, None for any other list
38
39# ---- shared definitions ----
40
41def mval(~T: Data, ~val: T -> Nat, r: Maybe<&2, T>) -> Maybe<&2, Nat>:
42  match r:
43    case Some{x}:
44      Some{val(x)}
45    case None{}:
46      None{}
47
48def keep(ok: Bool, +n: Nat) -> Maybe<&2, Nat>:
49  match ok:
50    case True{}:
51      Some{n}
52    case False{}:
53      None{}
54
55# n when it fits w bits
56def cnat(+w: Nat, +n: Nat) -> Maybe<&2, Nat>:
57  keep(C.fits(w, n), n)
58
59def ov_val(~T: Data, ~val: T -> Nat, r: F.Over<T>) -> Nat:
60  match r:
61    case F.OV{v, f}:
62      val(v)
63
64def ov_flag(-T: Data, r: F.Over<T>) -> Bool:
65  match r:
66    case F.OV{v, f}:
67      f
68
69def bn(b: Bool) -> Nat:
70  match b:
71    case True{}:
72      1n
73    case False{}:
74      0n
75
76# r is n when n fits w bits, and the largest w-bit value otherwise
77def saturated(+w: Nat, +n: Nat, +r: Nat, ok: Bool) -> Bool:
78  match ok:
79    case True{}:
80      Nat.is_eq(r, n)
81    case False{}:
82      Bool.and(C.fits(w, r), Bool.not(C.fits(w, 1n+r)))
83
84# ---- checked ----
85
86def CheckedAdd.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> Maybe<&2, T>, +w: Nat, +a: T, +b: T) -> Type:
87  {mval(~T, ~val, f(a, b)) == cnat(w, Nat.add(val(a), val(b))) : Maybe<&2, Nat>}
88
89def CheckedSub.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> Maybe<&2, T>, +a: T, +b: T) -> Type:
90  {mval(~T, ~val, f(a, b)) == keep(Nat.is_le(val(b), val(a)), Nat.sub(val(a), val(b))) : Maybe<&2, Nat>}
91
92def CheckedMul.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> Maybe<&2, T>, +w: Nat, +a: T, +b: T) -> Type:
93  {mval(~T, ~val, f(a, b)) == cnat(w, Nat.mul(val(a), val(b))) : Maybe<&2, Nat>}
94
95def CheckedDiv.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> Maybe<&2, T>, +a: T, +b: T) -> Type:
96  {mval(~T, ~val, f(a, b)) == keep(Bool.not(Nat.is_eq(val(b), 0n)), Nat.div(val(a), val(b))) : Maybe<&2, Nat>}
97
98def CheckedRem.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> Maybe<&2, T>, +a: T, +b: T) -> Type:
99  {mval(~T, ~val, f(a, b)) == keep(Bool.not(Nat.is_eq(val(b), 0n)), Nat.mod(val(a), val(b))) : Maybe<&2, Nat>}
100
101def CheckedPow.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> Maybe<&2, T>, +w: Nat, +a: T, +e: U32) -> Type:
102  {mval(~T, ~val, f(a, e)) == cnat(w, Nat.pow(val(a), U32.to_nat(e))) : Maybe<&2, Nat>}
103
104def CheckedShl.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> Maybe<&2, T>, +w: Nat, +a: T, +s: U32) -> Type:
105  {mval(~T, ~val, f(a, s)) == keep(Nat.is_lt(U32.to_nat(s), w), C.low(w, C.shift(U32.to_nat(s), val(a)))) : Maybe<&2, Nat>}
106
107def CheckedShr.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> Maybe<&2, T>, +w: Nat, +a: T, +s: U32) -> Type:
108  {mval(~T, ~val, f(a, s)) == keep(Nat.is_lt(U32.to_nat(s), w), C.high(U32.to_nat(s), val(a))) : Maybe<&2, Nat>}
109
110# ---- wrapping ----
111
112def WrappingAdd.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> T, +w: Nat, +a: T, +b: T) -> Type:
113  {val(f(a, b)) == C.low(w, Nat.add(val(a), val(b))) : Nat}
114
115def WrappingSub.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> T, +w: Nat, +a: T, +b: T) -> Type:
116  {Nat.add(val(f(a, b)), val(b)) == Nat.add(val(a), C.shift(w, bn(Nat.is_lt(val(a), val(b))))) : Nat}
117
118def WrappingMul.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> T, +w: Nat, +a: T, +b: T) -> Type:
119  {val(f(a, b)) == C.low(w, Nat.mul(val(a), val(b))) : Nat}
120
121def WrappingPow.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> T, +w: Nat, +a: T, +e: U32) -> Type:
122  {val(f(a, e)) == C.low(w, Nat.pow(val(a), U32.to_nat(e))) : Nat}
123
124def WrappingShl.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> T, +w: Nat, +a: T, +s: U32) -> Type:
125  {val(f(a, s)) == C.low(w, C.shift(Nat.mod(U32.to_nat(s), w), val(a))) : Nat}
126
127def WrappingShr.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> T, +w: Nat, +a: T, +s: U32) -> Type:
128  {val(f(a, s)) == C.high(Nat.mod(U32.to_nat(s), w), val(a)) : Nat}
129
130# ---- saturating ----
131
132def SaturatingAdd.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> T, +w: Nat, +a: T, +b: T) -> Type:
133  {saturated(w, Nat.add(val(a), val(b)), val(f(a, b)), C.fits(w, Nat.add(val(a), val(b)))) == True{} : Bool}
134
135def SaturatingSub.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> T, +a: T, +b: T) -> Type:
136  {val(f(a, b)) == Nat.sub(val(a), val(b)) : Nat}
137
138def SaturatingMul.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> T, +w: Nat, +a: T, +b: T) -> Type:
139  {saturated(w, Nat.mul(val(a), val(b)), val(f(a, b)), C.fits(w, Nat.mul(val(a), val(b)))) == True{} : Bool}
140
141def SaturatingPow.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> T, +w: Nat, +a: T, +e: U32) -> Type:
142  {saturated(w, Nat.pow(val(a), U32.to_nat(e)), val(f(a, e)), C.fits(w, Nat.pow(val(a), U32.to_nat(e)))) == True{} : Bool}
143
144# ---- overflowing ----
145
146def OverflowingAdd.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over<T>, +w: Nat, +a: T, +b: T) -> Type:
147  {ov_val(~T, ~val, f(a, b)) == C.low(w, Nat.add(val(a), val(b))) : Nat}
148
149def OverflowingAdd.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over<T>, +w: Nat, +a: T, +b: T) -> Type:
150  {ov_flag(T, f(a, b)) == Bool.not(C.fits(w, Nat.add(val(a), val(b)))) : Bool}
151
152def OverflowingSub.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over<T>, +w: Nat, +a: T, +b: T) -> Type:
153  {Nat.add(ov_val(~T, ~val, f(a, b)), val(b)) == Nat.add(val(a), C.shift(w, bn(Nat.is_lt(val(a), val(b))))) : Nat}
154
155def OverflowingSub.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over<T>, +a: T, +b: T) -> Type:
156  {ov_flag(T, f(a, b)) == Nat.is_lt(val(a), val(b)) : Bool}
157
158def OverflowingMul.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over<T>, +w: Nat, +a: T, +b: T) -> Type:
159  {ov_val(~T, ~val, f(a, b)) == C.low(w, Nat.mul(val(a), val(b))) : Nat}
160
161def OverflowingMul.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over<T>, +w: Nat, +a: T, +b: T) -> Type:
162  {ov_flag(T, f(a, b)) == Bool.not(C.fits(w, Nat.mul(val(a), val(b)))) : Bool}
163
164def OverflowingPow.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over<T>, +w: Nat, +a: T, +e: U32) -> Type:
165  {ov_val(~T, ~val, f(a, e)) == C.low(w, Nat.pow(val(a), U32.to_nat(e))) : Nat}
166
167def OverflowingPow.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over<T>, +w: Nat, +a: T, +e: U32) -> Type:
168  {ov_flag(T, f(a, e)) == Bool.not(C.fits(w, Nat.pow(val(a), U32.to_nat(e)))) : Bool}
169
170def OverflowingShl.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over<T>, +w: Nat, +a: T, +s: U32) -> Type:
171  {ov_val(~T, ~val, f(a, s)) == C.low(w, C.shift(Nat.mod(U32.to_nat(s), w), val(a))) : Nat}
172
173def OverflowingShl.flag(~T: Data, ~f: @+x: T -> @+y: U32 -> F.Over<T>, +a: T, +s: U32, +w: Nat) -> Type:
174  {ov_flag(T, f(a, s)) == Bool.not(Nat.is_lt(U32.to_nat(s), w)) : Bool}
175
176def OverflowingShr.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over<T>, +w: Nat, +a: T, +s: U32) -> Type:
177  {ov_val(~T, ~val, f(a, s)) == C.high(Nat.mod(U32.to_nat(s), w), val(a)) : Nat}
178
179def OverflowingShr.flag(~T: Data, ~f: @+x: T -> @+y: U32 -> F.Over<T>, +a: T, +s: U32, +w: Nat) -> Type:
180  {ov_flag(T, f(a, s)) == Bool.not(Nat.is_lt(U32.to_nat(s), w)) : Bool}
181
182# ---- bit count, primality ----
183
184def BitCount.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> Nat, +w: Nat, +a: T) -> Type:
185  {f(a) == SN.ones(w, val(a)) : Nat}
186
187def IsPrime.value(+a: U32) -> Type:
188  {F.u32_is_prime(a) == SN.prime(U32.to_nat(a)) : Bool}
189
190# no prime m with lo <= m < lo + k
191def no_prime(k: Nat, +lo: Nat) -> Bool:
192  match k:
193    case 0n:
194      True{}
195    case 1n+p:
196      Bool.and(Bool.not(SN.prime(lo)), no_prime(p, 1n+lo))
197
198# a found p is a prime above n, and none lies strictly between them
199def NextPrime.found(+n: U32, +p: U32, +h: {F.u32_next_prime(n) == Some{p} : Maybe<&2, U32>}) -> Type:
200  {Bool.and(Bool.and(Nat.is_lt(U32.to_nat(n), U32.to_nat(p)), SN.prime(U32.to_nat(p))), no_prime(Nat.sub(U32.to_nat(p), 1n+U32.to_nat(n)), 1n+U32.to_nat(n))) == True{} : Bool}
201
202# None: no prime m with n < m < 2^32
203def NextPrime.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}) -> Type:
204  {SN.prime(m) == False{} : Bool}
205
206# ---- bytes ----
207
208def nats(xs: List<&2, U32>) -> List<&2, Nat>:
209  match xs:
210    case Nil{}:
211      Nil{}
212    case Con{x, t}:
213      Con{U32.to_nat(x), nats(t)}
214
215# the k lowest base-256 digits of n, least significant first
216def le_digits(k: Nat, +n: Nat) -> List<&2, Nat>:
217  match k:
218    case 0n:
219      Nil{}
220    case 1n+p:
221      Con{C.low(8n, n), le_digits(p, C.high(8n, n))}
222
223def ToBytes.le(~T: Data, ~val: T -> Nat, ~f: @+x: T -> List<&2, U32>, +nb: Nat, +a: T) -> Type:
224  {nats(f(a)) == le_digits(nb, val(a)) : List<&2, Nat>}
225
226def ToBytes.be(~T: Data, ~val: T -> Nat, ~f: @+x: T -> List<&2, U32>, +nb: Nat, +a: T) -> Type:
227  {nats(f(a)) == C.reverse(Nat, le_digits(nb, val(a))) : List<&2, Nat>}
228
229# the value of exactly k base-256 digits, least significant first; None
230# for another length or a digit of 256 or more
231def digit_on(r: Maybe<&2, Nat>, ok: Bool, +x: Nat) -> Maybe<&2, Nat>:
232  match r:
233    case Some{+v}:
234      match ok:
235        case True{}:
236          Some{Nat.add(x, C.shift(8n, v))}
237        case False{}:
238          None{}
239    case None{}:
240      None{}
241
242def from_le(k: Nat, xs: List<&2, Nat>) -> Maybe<&2, Nat>:
243  match k xs:
244    case 0n Nil{}:
245      Some{0n}
246    case 1n+p Con{+x, t}:
247      digit_on(from_le(p, t), C.fits(8n, x), x)
248    case _ _:
249      None{}
250
251def FromBytes.le(~T: Data, ~val: T -> Nat, ~f: List<&2, U32> -> Maybe<&2, T>, +nb: Nat, bs: List<&2, U32>) -> Type:
252  {mval(~T, ~val, f(bs)) == from_le(nb, nats(bs)) : Maybe<&2, Nat>}
253
254def FromBytes.be(~T: Data, ~val: T -> Nat, ~f: List<&2, U32> -> Maybe<&2, T>, +nb: Nat, bs: List<&2, U32>) -> Type:
255  {mval(~T, ~val, f(bs)) == from_le(nb, C.reverse(Nat, nats(bs))) : Maybe<&2, Nat>}