spec/math/generic.bend

bend-collections-laws-crypto@1.0.0.0 · 289 lines · 50 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/src/math/num.bend as N
4import bend-collections-laws-crypto@1.0.0.0/src/math/generic.bend as G
5import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
6import bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend as NS
7import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
8import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
9
10# Specification of src/math/generic.bend: every templated function at each
11# instance of num.bend (U32, U64 from src/math/instances.bend; F32; the
12# software F64 of src/math/f64.bend). A clause is stated once over an
13# instance model and read at each type (docs/MATH_CONTRACTS.md has the
14# function x type matrix).
15#
16# STATED AND TESTED; A FEW PROVED: the Nat functions of natural.bend are
17# the proved reference (spec/math/natural.bend); these clauses relate each
18# typed function to them and are exercised by tools/check_generic.py, which
19# names the clause of every case it checks. At U32, Abs.identity,
20# Min.agrees, Max.agrees, Sign.agrees and Clamp.agrees are proved for every
21# input (proofs/math/typed/u32.bend); the other integer clauses are
22# evaluated by the checker at concrete U32 inputs
23# (proofs/math/typed/examples.bend). Semantics follow
24# python_style_math_stdlib_design.pdf: errors are values (2.3); a fixed
25# width reports Overflow instead of wrapping (2.6); Python's min/max keep
26# the first argument on ties (3.1); float sum is a left fold (4.6 notes
27# fsum is the compensated one); float pow is binary exponentiation with
28# every product rounded (4.5).
29#
30# Integer instance model (U32: U32.to_nat / U32.from_nat, width 32;
31# U64: spec/math/w64.bend's value / of_nat, width 64):
32#   val: T -> Nat, the value;  of: Nat -> T, below 2^w;  w, the width.
33#
34#   function     integer clauses (U32, U64)     float clauses (F32, F64)
35#   gcd          Gcd.agrees                      -
36#   lcm          Lcm.checked                     -
37#   gcd_all      GcdAll.agrees                   -
38#   lcm_all      LcmAll.checked                  -
39#   isqrt        Isqrt.agrees                    -
40#   iroot        Iroot.agrees                    -
41#   ilog         Ilog.agrees                     -
42#   factorial    Factorial.checked               -
43#   perm         Perm.checked                    -
44#   comb         Comb.checked                    -
45#   pow_mod      PowMod.agrees                   -
46#   mod_inverse  ModInverse.agrees               -
47#   divmod       DivMod.agrees                   -
48#   bit_length   BitLength.agrees                -
49#   clamp        Clamp.agrees                    FClamp.select
50#   min, max     Min.agrees, Max.agrees          FMin.select, FMax.select
51#   abs          Abs.identity                    FAbs.value
52#   sign         Sign.agrees                     FSign.select
53#   sum          Sum.checked                     FSum.fold
54#   prod         Prod.checked                    FProd.fold
55#   pow          Pow.checked                     FPow.binary
56
57# ---- shared definitions ----
58
59# n fits w bits: n < 2^w (spec/lib/common.bend states it without 2^w)
60def fits(+w: Nat, +n: Nat) -> Bool:
61  C.fits(w, n)
62
63def checked_pick(~T: Data, ~of: Nat -> T, +n: Nat, ok: Bool) -> Result<&2, &2, N.NumError, T>:
64  match ok:
65    case True{}:
66      Done{of(n)}
67    case False{}:
68      Fail{N.Overflow{}}
69
70# n as a T, or Overflow when it needs more than w bits
71def checked(~T: Data, ~of: Nat -> T, +w: Nat, +n: Nat) -> Result<&2, &2, N.NumError, T>:
72  checked_pick(~T, ~of, n, fits(w, n))
73
74def err(e: M.MathError) -> N.NumError:
75  match e:
76    case M.ZeroDivision{}:
77      N.DivByZero{}
78    case M.Domain{}:
79      N.BadDomain{}
80    case M.NotInvertible{}:
81      N.NoInverse{}
82
83# a Nat result carried to T (values that are no larger than an argument)
84def lift(~T: Data, ~of: Nat -> T, r: Result<&2, &2, M.MathError, Nat>) -> Result<&2, &2, N.NumError, T>:
85  match r:
86    case Done{x}:
87      Done{of(x)}
88    case Fail{e}:
89      Fail{err(e)}
90
91def lift_nat(r: Result<&2, &2, M.MathError, Nat>) -> Result<&2, &2, N.NumError, Nat>:
92  match r:
93    case Done{x}:
94      Done{x}
95    case Fail{e}:
96      Fail{err(e)}
97
98def lift_qr(~T: Data, ~of: Nat -> T, r: Result<&2, &2, M.MathError, M.QuotRem>) -> Result<&2, &2, N.NumError, G.QuotRem<T>>:
99  match r:
100    case Done{M.QR{q, m}}:
101      Done{G.TQR{of(q), of(m)}}
102    case Fail{e}:
103      Fail{err(e)}
104
105def vals(~T: Data, ~val: T -> Nat, xs: List<&2, T>) -> List<&2, Nat>:
106  match xs:
107    case Nil{}:
108      Nil{}
109    case Con{x, t}:
110      Con{val(x), vals(~T, ~val, t)}
111
112def pick(-T: Data, c: Bool, +a: T, +b: T) -> T:
113  match c:
114    case True{}:
115      a
116    case False{}:
117      b
118
119# a fold that stops at the first prefix of w bits or more (prod, lcm_all:
120# a later 0 can shrink the value, the overflow already happened)
121def prod_go(+w: Nat, xs: List<&2, Nat>, +acc: Nat, ok: Bool) -> Nat & Bool:
122  match xs ok:
123    case Nil{} _:
124      (acc, ok)
125    case Con{x, t} False{}:
126      (acc, False{})
127    case Con{+x, t} True{}:
128      prod_go(w, t, Nat.mul(acc, x), fits(w, Nat.mul(acc, x)))
129
130def lcm_go(+w: Nat, xs: List<&2, Nat>, +acc: Nat, ok: Bool) -> Nat & Bool:
131  match xs ok:
132    case Nil{} _:
133      (acc, ok)
134    case Con{x, t} False{}:
135      (acc, False{})
136    case Con{+x, t} True{}:
137      lcm_go(w, t, M.lcm(acc, x), fits(w, M.lcm(acc, x)))
138
139def prefix_fin(~T: Data, ~of: Nat -> T, r: Nat & Bool) -> Result<&2, &2, N.NumError, T>:
140  (+n, ok) = r
141  checked_pick(~T, ~of, n, ok)
142
143# ---- integer instances (U32, U64) ----
144
145def Gcd.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +a: T, +b: T) -> Type:
146  {G.gcd(~T, ~op, ~test, a, b) == of(M.gcd(val(a), val(b))) : T}
147
148def Lcm.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, +a: T, +b: T) -> Type:
149  {G.lcm(~T, ~op, ~test, a, b) == checked(~T, ~of, w, M.lcm(val(a), val(b))) : Result<&2, &2, N.NumError, T>}
150
151def GcdAll.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, xs: List<&2, T>) -> Type:
152  {G.gcd_all(~T, ~op, ~test, xs) == of(M.gcd_all(vals(~T, ~val, xs))) : T}
153
154def LcmAll.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, xs: List<&2, T>) -> Type:
155  {G.lcm_all(~T, ~op, ~test, xs) == prefix_fin(~T, ~of, lcm_go(w, vals(~T, ~val, xs), 1n, True{})) : Result<&2, &2, N.NumError, T>}
156
157def Isqrt.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +n: T) -> Type:
158  {G.isqrt(~T, ~op, ~test, n) == of(M.isqrt(val(n))) : T}
159
160def Iroot.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +n: T, +k: Nat) -> Type:
161  {G.iroot(~T, ~op, ~test, n, k) == lift(~T, ~of, M.iroot(val(n), k)) : Result<&2, &2, N.NumError, T>}
162
163def Ilog.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +n: T, +b: T) -> Type:
164  {G.ilog(~T, ~op, ~test, n, b) == lift_nat(M.ilog(val(n), val(b))) : Result<&2, &2, N.NumError, Nat>}
165
166def Factorial.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, +n: T) -> Type:
167  {G.factorial(~T, ~op, ~test, n) == checked(~T, ~of, w, M.factorial(val(n))) : Result<&2, &2, N.NumError, T>}
168
169def Perm.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, +n: T, +k: T) -> Type:
170  {G.perm(~T, ~op, ~test, n, k) == checked(~T, ~of, w, M.perm(val(n), val(k))) : Result<&2, &2, N.NumError, T>}
171
172def Comb.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, +n: T, +k: T) -> Type:
173  {G.comb(~T, ~op, ~test, n, k) == checked(~T, ~of, w, M.comb(val(n), val(k))) : Result<&2, &2, N.NumError, T>}
174
175def PowMod.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +b: T, +e: T, +m: T) -> Type:
176  {G.pow_mod(~T, ~op, ~test, b, e, m) == lift(~T, ~of, M.pow_mod(val(b), val(e), val(m))) : Result<&2, &2, N.NumError, T>}
177
178def ModInverse.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +a: T, +m: T) -> Type:
179  {G.mod_inverse(~T, ~op, ~test, a, m) == lift(~T, ~of, M.mod_inverse(val(a), val(m))) : Result<&2, &2, N.NumError, T>}
180
181def DivMod.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +a: T, +b: T) -> Type:
182  {G.divmod(~T, ~op, ~test, a, b) == lift_qr(~T, ~of, M.divmod(val(a), val(b))) : Result<&2, &2, N.NumError, G.QuotRem<T>>}
183
184def BitLength.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, +n: T) -> Type:
185  {G.bit_length(~T, ~op, ~test, n) == M.bit_length(val(n)) : Nat}
186
187def Clamp.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +x: T, +lo: T, +hi: T) -> Type:
188  {G.clamp(~T, ~op, ~test, x, lo, hi) == lift(~T, ~of, M.clamp(val(x), val(lo), val(hi))) : Result<&2, &2, N.NumError, T>}
189
190def Min.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +a: T, +b: T) -> Type:
191  {G.min(~T, ~op, ~test, a, b) == of(Nat.min(val(a), val(b))) : T}
192
193def Max.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +a: T, +b: T) -> Type:
194  {G.max(~T, ~op, ~test, a, b) == of(Nat.max(val(a), val(b))) : T}
195
196# unsigned: |x| is x
197def Abs.identity(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T) -> Type:
198  {G.abs(~T, ~op, ~test, x) == x : T}
199
200# unsigned: 1 above zero, else 0
201def Sign.agrees(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +x: T) -> Type:
202  {G.sign(~T, ~op, ~test, x) == of(Nat.min(val(x), 1n)) : T}
203
204# the partial sums only grow, so the sum overflows exactly when the total does
205def Sum.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, xs: List<&2, T>) -> Type:
206  {G.sum(~T, ~op, ~test, xs) == checked(~T, ~of, w, NS.lsum(vals(~T, ~val, xs))) : Result<&2, &2, N.NumError, T>}
207
208def Prod.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, xs: List<&2, T>) -> Type:
209  {G.prod(~T, ~op, ~test, xs) == prefix_fin(~T, ~of, prod_go(w, vals(~T, ~val, xs), 1n, True{})) : Result<&2, &2, N.NumError, T>}
210
211def Pow.checked(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~val: T -> Nat, ~of: Nat -> T, +w: Nat, +x: T, +k: Nat) -> Type:
212  {G.pow(~T, ~op, ~test, x, k) == checked(~T, ~of, w, Nat.pow(val(x), k)) : Result<&2, &2, N.NumError, T>}
213
214# ---- float instances (F32, F64): the instance's own IEEE operations ----
215# (F32's are Base's primitives; F64's are src/math/f64.bend's, specified by
216# spec/math/f64.bend)
217
218def FMin.select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +a: T, +b: T) -> Type:
219  {G.min(~T, ~op, ~test, a, b) == pick(T, test(N.Lt{b, a}), b, a) : T}
220
221def FMax.select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +a: T, +b: T) -> Type:
222  {G.max(~T, ~op, ~test, a, b) == pick(T, test(N.Lt{a, b}), b, a) : T}
223
224def fclamp_pick(~T: Data, ~test: N.Test<T> -> Bool, +x: T, +lo: T, +hi: T, bad: Bool) -> Result<&2, &2, N.NumError, T>:
225  match bad:
226    case True{}:
227      Fail{N.BadDomain{}}
228    case False{}:
229      Done{pick(T, test(N.Lt{hi, pick(T, test(N.Lt{x, lo}), lo, x)}), hi, pick(T, test(N.Lt{x, lo}), lo, x))}
230
231# Domain when hi < lo; else min(max(x, lo), hi) by the two selections
232def FClamp.select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +lo: T, +hi: T) -> Type:
233  {G.clamp(~T, ~op, ~test, x, lo, hi) == fclamp_pick(~T, ~test, x, lo, hi, test(N.Lt{hi, lo})) : Result<&2, &2, N.NumError, T>}
234
235def FAbs.value(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T) -> Type:
236  {G.abs(~T, ~op, ~test, x) == op(N.Abs{x}) : T}
237
238# 1 above zero, -1 below, x itself otherwise (zeros keep their sign, NaN stays)
239def FSign.select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T) -> Type:
240  {G.sign(~T, ~op, ~test, x) == pick(T, test(N.Lt{op(N.ZeroOp{}), x}), op(N.One{}), pick(T, test(N.Lt{x, op(N.ZeroOp{})}), op(N.Neg{op(N.One{})}), x)) : T}
241
242def fold_add(~T: Data, ~op: N.Op<T> -> T, xs: List<&2, T>, +acc: T) -> T:
243  match xs:
244    case Nil{}:
245      acc
246    case Con{+x, t}:
247      fold_add(~T, ~op, t, op(N.Add{acc, x}))
248
249def fold_mul(~T: Data, ~op: N.Op<T> -> T, xs: List<&2, T>, +acc: T) -> T:
250  match xs:
251    case Nil{}:
252      acc
253    case Con{+x, t}:
254      fold_mul(~T, ~op, t, op(N.Mul{acc, x}))
255
256# ((0 + x0) + x1) + ..., every addition rounded
257def FSum.fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, xs: List<&2, T>) -> Type:
258  {G.sum(~T, ~op, ~test, xs) == Done{fold_add(~T, ~op, xs, op(N.ZeroOp{}))} : Result<&2, &2, N.NumError, T>}
259
260def FProd.fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, xs: List<&2, T>) -> Type:
261  {G.prod(~T, ~op, ~test, xs) == Done{fold_mul(~T, ~op, xs, op(N.One{}))} : Result<&2, &2, N.NumError, T>}
262
263# right-to-left binary exponentiation: acc *= base on a 1 bit, base *= base
264# while bits remain, each product rounded (k = 0 is a fixed point, so any
265# fuel past k's bit length gives the same result)
266def binpow(~T: Data, ~op: N.Op<T> -> T, fuel: Nat, +k: Nat, +base: T, +acc: T) -> T:
267  match fuel:
268    case 0n:
269      acc
270    case 1n+f:
271      binpow(~T, ~op, f, Nat.div(k, 2n), pick(T, Nat.is_lt(1n, k), op(N.Mul{base, base}), base), pick(T, Nat.is_eq(Nat.mod(k, 2n), 1n), op(N.Mul{acc, base}), acc))
272
273def FPow.binary(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +k: Nat) -> Type:
274  {G.pow(~T, ~op, ~test, x, k) == Done{binpow(~T, ~op, 1n+k, k, x, op(N.One{}))} : Result<&2, &2, N.NumError, T>}
275
276# ---- instance models ----
277# U32: the value and the U32 of a value below 2^32 (width 32)
278def u32_val(x: U32) -> Nat:
279  U32.to_nat(x)
280
281def u32_of(n: Nat) -> U32:
282  U32.from_nat(n)
283
284# U64: the two-limb value and the U64 of a value below 2^64 (width 64)
285def u64_val(x: W.U64) -> Nat:
286  SW.value(x)
287
288def u64_of(n: Nat) -> W.U64:
289  SW.of_nat(n)