src/float/f32.bend fails

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/float/f32.bend as MF32

2 imports

import Base
import ../nat.bend as Nat

Laws

law split_unsplit unverifiedits file does not pass the checker (fails)source · line 63 · raw

@n:Nat -> @w:Word(n) -> @s:Bool -> {(w, s) == split(n, unsplit(n, w, s)) : Pair(Word(n), Bool)}

law bool_cmp_refl unverifiedits file does not pass the checker (fails)source · line 217 · raw

@x:Bool -> {EQ{} == Bool.cmp(x, x) : Cmp}

law Word.cmp_refl unverifiedits file does not pass the checker (fails)source · line 228 · raw

@+n:Nat -> @a:Word(n) -> {EQ{} == Word.cmp(n, a, a) : Cmp}

law fin_swap unverifiedits file does not pass the checker (fails)source · line 245 · raw

@c:Cmp -> @x:Bool -> @y:Bool -> {swap(Word.cmp.fin(x, y, c)) == Word.cmp.fin(y, x, swap(c)) : Cmp}

law Word.cmp_swap unverifiedits file does not pass the checker (fails)source · line 266 · raw

@+n:Nat -> @a:Word(n) -> @b:Word(n) -> {swap(Word.cmp(n, a, b)) == Word.cmp(n, b, a) : Cmp}

law lt_notgt unverifiedits file does not pass the checker (fails)source · line 284 · raw

@c:Cmp -> @_:{Cmp.is_lt(c) == True{} : Bool} -> NotGT(c)

law notlt_swap unverifiedits file does not pass the checker (fails)source · line 297 · raw

@c:Cmp -> @_:{Cmp.is_lt(c) == False{} : Bool} -> NotGT(swap(c))

law lt_le.signs unverifiedits file does not pass the checker (fails)source · line 310 · raw

@s:Bool -> @t:Bool -> @+x:Word(31n) -> @+y:Word(31n) -> @_:{lt.signs(s, t, x, y) == True{} : Bool} -> le.signs(s, t, x, y)

law lt_le.key unverifiedits file does not pass the checker (fails)source · line 329 · raw

@a:Key -> @b:Key -> @_:{lt.key(a, b) == True{} : Bool} -> LE.key(a, b)

a < b gives a <= b

law lt_key unverifiedits file does not pass the checker (fails)source · line 346 · raw

@a:Key -> @b:Key -> @_:{lt.key(a, b) == True{} : Bool} -> IsKey(a)

only an ordered value is below something

law le_key_l unverifiedits file does not pass the checker (fails)source · line 362 · raw

@a:Key -> @b:Key -> @_:LE.key(a, b) -> IsKey(a)

law le_key_r unverifiedits file does not pass the checker (fails)source · line 378 · raw

@a:Key -> @b:Key -> @_:LE.key(a, b) -> IsKey(b)

law le_refl.signs unverifiedits file does not pass the checker (fails)source · line 394 · raw

@s:Bool -> @+m:Word(31n) -> le.signs(s, s, m, m)

law le_refl.key unverifiedits file does not pass the checker (fails)source · line 408 · raw

@k:Key -> @_:IsKey(k) -> LE.key(k, k)

law total.same unverifiedits file does not pass the checker (fails)source · line 419 · raw

@+x:Word(31n) -> @+y:Word(31n) -> @e:{Cmp.is_lt(Word.cmp(31n, x, y)) == False{} : Bool} -> NotGT(Word.cmp(31n, y, x))

law total.mixed unverifiedits file does not pass the checker (fails)source · line 429 · raw

@+x:Word(31n) -> @+y:Word(31n) -> @e:{lt.signs(True{}, False{}, x, y) == False{} : Bool} -> 0x5f97f469d15c04a181dae0e4e64e1d3d/src/nat.IsFalse(lt.signs(True{}, False{}, x, y))

law total.signs unverifiedits file does not pass the checker (fails)source · line 439 · raw

@s:Bool -> @t:Bool -> @+x:Word(31n) -> @+y:Word(31n) -> @_:{lt.signs(s, t, x, y) == False{} : Bool} -> le.signs(t, s, y, x)

law total.key unverifiedits file does not pass the checker (fails)source · line 458 · raw

@a:Key -> @b:Key -> @_:IsKey(a) -> @_:IsKey(b) -> @_:{lt.key(a, b) == False{} : Bool} -> LE.key(b, a)

two ordered values: not a < b gives b <= a

law bits_lt unverifiedits file does not pass the checker (fails)source · line 486 · raw

@-lt:LtOk -> @+a:F32 -> @+b:F32 -> @-c:Bool -> @e:{F32.is_lt(a, b) == c : Bool} -> {lt_bits(a, b) == c : Bool}

law min_le_r.go unverifiedits file does not pass the checker (fails)source · line 501 · raw

@-lt:LtOk -> @+a:F32 -> @+b:F32 -> @c:Bool -> @e:{F32.is_lt(a, b) == c : Bool} -> @bb:LE(b, b) -> LE(Bool.pick(F32, c, a, b), b)

law clamp_le_hi unverifiedits file does not pass the checker (fails)source · line 518 · raw

@-lt:LtOk -> @+x:F32 -> @+lo:F32 -> @+hi:F32 -> @lh:LE(lo, hi) -> LE(F32.clamp(x, lo, hi), hi)

clamp(x, lo, hi) <= hi for every x, NaN and infinities included

law lo_le_clamp.go unverifiedits file does not pass the checker (fails)source · line 530 · raw

@-lt:LtOk -> @+x:F32 -> @+lo:F32 -> @+hi:F32 -> @c1:Bool -> @e1:{F32.is_lt(x, lo) == c1 : Bool} -> @c2:Bool -> @e2:{F32.is_lt(Bool.pick(F32, c1, lo, x), hi) == c2 : Bool} -> @lh:LE(lo, hi) -> LE(lo, Bool.pick(F32, c2, Bool.pick(F32, c1, lo, x), hi))

law lo_le_clamp unverifiedits file does not pass the checker (fails)source · line 554 · raw

@-lt:LtOk -> @+x:F32 -> @+lo:F32 -> @+hi:F32 -> @lh:LE(lo, hi) -> LE(lo, F32.clamp(x, lo, hi))

lo <= clamp(x, lo, hi) for every x, when lo <= hi

law neg_mag.go unverifiedits file does not pass the checker (fails)source · line 568 · raw

@r:Pair(Word(31n), Bool) -> {first(r) == first(split(31n, neg.go(r))) : Word(31n)}

law neg_mag.bits unverifiedits file does not pass the checker (fails)source · line 576 · raw

@a:F32 -> {mag(a) == mag(neg_bits(a)) : Word(31n)}

law neg_mag unverifiedits file does not pass the checker (fails)source · line 586 · raw

@-ng:NegOk -> @+a:F32 -> @ka:IsKey(key(a)) -> {mag(a) == mag(F32.neg(a)) : Word(31n)}

|-a| is |a|, bit for bit

law key_sign unverifiedits file does not pass the checker (fails)source · line 597 · raw

@s:Bool -> @t:Bool -> @m:Word(31n) -> @c:Cmp -> @_:IsKey(key.cls(s, m, c)) -> IsKey(key.cls(t, m, c))

whether a value is NaN does not depend on its sign

law neg_key.go unverifiedits file does not pass the checker (fails)source · line 613 · raw

@r:Pair(Word(31n), Bool) -> @_:IsKey(key.go(r)) -> IsKey(key.go(split(31n, neg.go(r))))

law neg_key.bits unverifiedits file does not pass the checker (fails)source · line 622 · raw

@a:F32 -> @_:IsKey(key(a)) -> IsKey(key(neg_bits(a)))

law neg_key unverifiedits file does not pass the checker (fails)source · line 632 · raw

@-ng:NegOk -> @+a:F32 -> @+ka:IsKey(key(a)) -> IsKey(key(F32.neg(a)))

the negation of a non-NaN is not NaN

Types

type Key source · line 103 · raw

Data

how the IEEE order reads a float: NaN, or a number with a sign and a magnitude. Magnitudes are ordered as integers; above infinity's they are NaNs.

KNaN
```
Key
```
Num
```
@neg:Bool -> @mag:Word(31n) -> Key
```

Definitions

def void source · line 18 · raw

@-A:Type -> @v:Empty -> A

def no_f source · line 22 · raw

@e:{False{} == True{} : Bool} -> Empty

{False == True} and {True == False} are empty

def no_t source · line 26 · raw

@e:{True{} == False{} : Bool} -> Empty

def first source · line 33 · raw

@r:Pair(Word(31n), Bool) -> Word(31n)

def split.cons source · line 37 · raw

@-n:Nat -> @b:Bool -> @r:Pair(Word(n), Bool) -> Pair(Word(1n+n), Bool)

def split source · line 42 · raw

@n:Nat -> @w:Word(1n+n) -> Pair(Word(n), Bool)

a word's first n bits, and its last bit (the sign, for n = 31)

def unsplit source · line 54 · raw

@n:Nat -> @w:Word(n) -> @s:Bool -> Word(1n+n)

a word with s appended as its last bit

def mag source · line 82 · raw

@x:F32 -> Word(31n)

the 31 bits below the sign: exponent and fraction

def neg.go source · line 87 · raw

@r:Pair(Word(31n), Bool) -> Word(32n)

def neg_bits source · line 92 · raw

@x:F32 -> F32

IEEE 754 negation: the sign bit flipped

def IsKey source · line 107 · raw

@k:Key -> Data

def inf_mag.go source · line 115 · raw

@x:U32 -> F32

infinity's magnitude, 0x7F800000

def inf_mag source · line 120 · raw

F32

def key.cls source · line 123 · raw

@s:Bool -> @m:Word(31n) -> @c:Cmp -> Key

def key.go source · line 132 · raw

@r:Pair(Word(31n), Bool) -> Key

def key source · line 136 · raw

@x:F32 -> Key

def zero source · line 141 · raw

@m:Word(31n) -> Bool

def lt.signs source · line 144 · raw

@s:Bool -> @t:Bool -> @+x:Word(31n) -> @+y:Word(31n) -> Bool

def lt.key source · line 155 · raw

@a:Key -> @b:Key -> Bool

def lt_bits source · line 167 · raw

@a:F32 -> @b:F32 -> Bool

IEEE 754 a < b: false when either is NaN; -0 and +0 are equal

def NotGT source · line 170 · raw

@c:Cmp -> Data

def le.signs source · line 179 · raw

@s:Bool -> @t:Bool -> @+x:Word(31n) -> @+y:Word(31n) -> Type

def LE.key source · line 190 · raw

@a:Key -> @b:Key -> Type

def LE source · line 202 · raw

@a:F32 -> @b:F32 -> Type

a <= b in the IEEE order, as a type: Empty when either is NaN

def swap source · line 208 · raw

@c:Cmp -> Cmp

def LtOk source · line 478 · raw

Type

the hardware's < is IEEE 754's

def NegOk source · line 483 · raw

Type

the hardware's negation flips the sign bit of every non-NaN float. A NaN's sign and payload are left out: the JS lane does not keep them.