1 import Base 2 import ../lib/common.bend as C 3 import ../../src/math/num.bend as N 4 import ../../src/math/generic.bend as G 5 import ../../src/math/natural.bend as M 6 import ./natural.bend as NS 7 import ./w64.bend as SW 8 import ../../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) 60 def fits(+w: Nat, +n: Nat) -> Bool: 61 C.fits(w, n) 62 63 def 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 71 def 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 74 def 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) 84 def 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 91 def 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 98 def lift_qr(~T: Data, ~of: Nat -> T, r: Result<&2, &2, M.MathError, M.QuotRem>) -> Result<&2, &2, N.NumError, G.QuotRem>: 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 105 def 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 112 def 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) 121 def 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 130 def 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 139 def 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 145 def Gcd.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 148 def Lcm.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 151 def GcdAll.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 154 def LcmAll.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 157 def Isqrt.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> Bool, ~val: T -> Nat, ~of: Nat -> T, +n: T) -> Type: 158 {G.isqrt(~T, ~op, ~test, n) == of(M.isqrt(val(n))) : T} 159 160 def Iroot.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 163 def Ilog.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 166 def Factorial.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 169 def Perm.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 172 def Comb.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 175 def PowMod.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 178 def ModInverse.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 181 def DivMod.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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>} 183 184 def BitLength.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> Bool, ~val: T -> Nat, +n: T) -> Type: 185 {G.bit_length(~T, ~op, ~test, n) == M.bit_length(val(n)) : Nat} 186 187 def Clamp.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 190 def Min.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 193 def Max.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 197 def Abs.identity(~T: Data, ~op: N.Op -> T, ~test: N.Test -> Bool, +x: T) -> Type: 198 {G.abs(~T, ~op, ~test, x) == x : T} 199 200 # unsigned: 1 above zero, else 0 201 def Sign.agrees(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 205 def Sum.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 208 def Prod.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 211 def Pow.checked(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 218 def FMin.select(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 221 def FMax.select(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 224 def fclamp_pick(~T: Data, ~test: N.Test -> 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 232 def FClamp.select(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 235 def FAbs.value(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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) 239 def FSign.select(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 242 def fold_add(~T: Data, ~op: N.Op -> 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 249 def fold_mul(~T: Data, ~op: N.Op -> 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 257 def FSum.fold(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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 260 def FProd.fold(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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) 266 def binpow(~T: Data, ~op: N.Op -> 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 273 def FPow.binary(~T: Data, ~op: N.Op -> T, ~test: N.Test -> 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) 278 def u32_val(x: U32) -> Nat: 279 U32.to_nat(x) 280 281 def 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) 285 def u64_val(x: W.U64) -> Nat: 286 SW.value(x) 287 288 def u64_of(n: Nat) -> W.U64: 289 SW.of_nat(n)