1 import Base 2 import ../lib/common.bend as C 3 import ../../src/math/fixed.bend as F 4 import ./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 41 def 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 48 def 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 56 def cnat(+w: Nat, +n: Nat) -> Maybe<&2, Nat>: 57 keep(C.fits(w, n), n) 58 59 def ov_val(~T: Data, ~val: T -> Nat, r: F.Over) -> Nat: 60 match r: 61 case F.OV{v, f}: 62 val(v) 63 64 def ov_flag(-T: Data, r: F.Over) -> Bool: 65 match r: 66 case F.OV{v, f}: 67 f 68 69 def 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 77 def 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 86 def 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 89 def 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 92 def 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 95 def 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 98 def 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 101 def 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 104 def 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 107 def 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 112 def 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 115 def 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 118 def 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 121 def 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 124 def 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 127 def 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 132 def 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 135 def 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 138 def 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 141 def 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 146 def OverflowingAdd.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over, +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 149 def OverflowingAdd.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over, +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 152 def OverflowingSub.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over, +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 155 def OverflowingSub.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over, +a: T, +b: T) -> Type: 156 {ov_flag(T, f(a, b)) == Nat.is_lt(val(a), val(b)) : Bool} 157 158 def OverflowingMul.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over, +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 161 def OverflowingMul.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: T -> F.Over, +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 164 def OverflowingPow.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over, +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 167 def OverflowingPow.flag(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over, +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 170 def OverflowingShl.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over, +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 173 def OverflowingShl.flag(~T: Data, ~f: @+x: T -> @+y: U32 -> F.Over, +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 176 def OverflowingShr.value(~T: Data, ~val: T -> Nat, ~f: @+x: T -> @+y: U32 -> F.Over, +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 179 def OverflowingShr.flag(~T: Data, ~f: @+x: T -> @+y: U32 -> F.Over, +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 184 def 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 187 def 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 191 def 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 199 def 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 203 def 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 208 def 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 216 def 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 223 def 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 226 def 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 231 def 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 242 def 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 251 def 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 254 def 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>}