src/float/sf32.bend

bend-lawful-stdlib@0.1.0.0 · 150 lines · 22 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/float/bin.bend as Bin
3import bend-lawful-stdlib@0.1.0.0/src/float/format.bend as Fmt
4import bend-lawful-stdlib@0.1.0.0/src/float/num.bend as Num
5
6# sf32.bend: binary32 floats in software, and the two F32 implementations.
7#
8#   import ./sf32.bend as SF32
9#   SF32.add(a, b)          # software IEEE add on F32 bit patterns
10#   SF32.soft(), SF32.hard() # Num.Impl<F32>: software, and hardware
11#
12# decode and encode convert between F32 bits (sign, 8 exponent bits, 23
13# mantissa bits) and exact values. The software operations are the spec
14# itself: decode, exact operation and rounding, encode. They compute in
15# the checker and give the same bits on every backend; they are also far
16# slower than hardware. A faster algorithm can be another Num.Impl.
17#
18# hard() uses Base's F32.add and F32.mul, which the checker cannot
19# compute. HardOk is the assumption that they are correctly rounded:
20# a law that needs it takes ~ok: HardOk, and it stays a named hypothesis.
21
22def bits(x: F32) -> U32:
23  match x:
24    case F32{w}:
25      U32{w}
26
27def of_bits(x: U32) -> F32:
28  match x:
29    case U32{w}:
30      F32{w}
31
32# Decoding
33# --------
34# The fields are read off the word in one pass (23 mantissa bits, 8
35# exponent bits, the sign), not with U32 shifts and masks: the checker
36# evaluates a U32 operation bit by bit, and each shift costs a full pass.
37
38def decode.go(neg: Bool, e: Nat, f: Bin.Bin, top: Bool, low: Bool, fz: Bool) -> Fmt.Val:
39  match top low fz:
40    case True{} low True{}:
41      Fmt.Inf{neg}
42    case True{} low False{}:
43      Fmt.NaN{}
44    case False{} True{} True{}:
45      Fmt.Z{neg}
46    case False{} True{} False{}:
47      Fmt.Fin{neg, f, 151n}
48    case False{} False{} fz:
49      Fmt.Fin{neg, Bin.add(f, Bin.pow2(23n)), Nat.add(e, 150n)}
50
51def decode.cls(neg: Bool, +e: Nat, +f: Bin.Bin) -> Fmt.Val:
52  decode.go(neg, e, f, Nat.is_eq(e, 255n), Nat.is_eq(e, 0n), Bin.is_zero(f))
53
54def decode.sign(f: Bin.Bin, e: Bin.Bin, w: Word(1n)) -> Fmt.Val:
55  match w:
56    case WCon{s, t}:
57      decode.cls(s, Bin.to_nat(e), f)
58
59def decode.exp(f: Bin.Bin, p: Bin.Bin & Word(1n)) -> Fmt.Val:
60  (e, w) = p
61  decode.sign(f, e, w)
62
63def decode.man(p: Bin.Bin & Word(9n)) -> Fmt.Val:
64  (f, w) = p
65  decode.exp(f, Bin.take(8n, 1n, w))
66
67# the exact value of a float
68def decode(x: F32) -> Fmt.Val:
69  match x:
70    case F32{w}:
71      decode.man(Bin.take(23n, 9n, w))
72
73# Encoding
74# --------
75
76# the sign bit, as it sits above the 8 exponent bits
77def sign(neg: Bool) -> Bin.Bin:
78  match neg:
79    case True{}:
80      Bin.pow2(8n)
81    case False{}:
82      Bin.BZ{}
83
84# a word from its fields: 23 mantissa bits, then exponent and sign above
85def word(frac: Bin.Bin, exp: Bin.Bin, neg: Bool) -> F32:
86  F32{Bin.to_word(32n, Bin.add(Bin.low(23n, frac), Bin.shl(Bin.add(exp, sign(neg)), 23n)))}
87
88def first(r: Bin.Bin & Bool & Bool) -> Bin.Bin:
89  (q, a, b) = r
90  q
91
92# m moved to have its last bit at exponent t
93def align(m: Bin.Bin, +e: Nat, +t: Nat, right: Bool) -> Bin.Bin:
94  match right:
95    case True{}:
96      first(Bin.shr(Nat.sub(t, e), m, False{}, False{}))
97    case False{}:
98      Bin.shl(m, Nat.sub(e, t))
99
100def field(+t: Nat, normal: Bool) -> Bin.Bin:
101  match normal:
102    case True{}:
103      Bin.of_nat(Nat.sub(t, 150n))
104    case False{}:
105      Bin.BZ{}
106
107def put(neg: Bool, t: Nat, +m: Bin.Bin) -> F32:
108  word(m, field(t, Nat.is_eq(Bin.len(m), 24n)), neg)
109
110# a finite value that fits binary32, as bits: 24 mantissa bits when
111# normal, fewer at the smallest exponent when subnormal
112def encode.fin(neg: Bool, +m: Bin.Bin, +e: Nat) -> F32:
113  +t = Nat.max(Nat.sub(Nat.add(e, Bin.len(m)), 24n), 151n)
114  put(neg, t, align(m, e, t, Nat.is_ge(t, e)))
115
116def encode(v: Fmt.Val) -> F32:
117  match v:
118    case Fmt.Z{neg}:
119      word(Bin.BZ{}, Bin.BZ{}, neg)
120    case Fmt.Inf{neg}:
121      word(Bin.BZ{}, Bin.of_nat(255n), neg)
122    case Fmt.NaN{}:
123      of_bits(2143289344) # 0x7FC00000, the quiet NaN
124    case Fmt.Fin{neg, m, e}:
125      encode.fin(neg, m, e)
126
127# Software operations
128# -------------------
129
130def add(a: F32, b: F32) -> F32:
131  encode(Fmt.spec_add(Fmt.binary32(), decode(a), decode(b)))
132
133def sub(a: F32, b: F32) -> F32:
134  encode(Fmt.spec_sub(Fmt.binary32(), decode(a), decode(b)))
135
136def mul(a: F32, b: F32) -> F32:
137  encode(Fmt.spec_mul(Fmt.binary32(), decode(a), decode(b)))
138
139# Implementations
140# ---------------
141
142def soft() -> Num.Impl<F32>:
143  Num.Impl{Fmt.binary32(), decode, add, mul}
144
145def hard() -> Num.Impl<F32>:
146  Num.Impl{Fmt.binary32(), decode, F32.add, F32.mul}
147
148# the hardware assumption: Base's F32.add and F32.mul are correctly rounded
149def HardOk() -> Type:
150  Num.Correct<F32, hard()>