src/float/f32.bend

bend-lawful-stdlib@0.1.0.0 · 640 lines · 58 definitions

1import Base
2import bend-lawful-stdlib@0.1.0.0/src/nat.bend as Nat
3
4# f32.bend: laws about Base's F32 functions, under named hardware
5# hypotheses.
6#
7#   import ./f32.bend as F32
8#   F32.clamp_le_hi(~lt, x, lo, hi, lh)   # clamp(x, lo, hi) <= hi, any x
9#
10# Base's F32 operations are unfilled laws, so the checker cannot compute
11# them. Comparison and negation are specified here on the float's bits,
12# where it can: lt_bits is IEEE 754's a < b, neg_bits flips the sign bit.
13# A law about Base's F32.is_lt or F32.neg takes the hypothesis that the
14# hardware matches them (~lt: LtOk(), ~ng: NegOk()) as a template
15# argument, so each law states what it assumes. IEEE 754 comparison and
16# negation are exact; C, CUDA, Metal and JS implement them this way.
17
18def void(-A: Type, v: Empty) -> A:
19  match v:
20
21# {False == True} and {True == False} are empty
22def no_f(e: {False{} == True{} : Bool}) -> Empty:
23  %e : Nat.IsFalse(_)
24  Unit{}
25
26def no_t(e: {True{} == False{} : Bool}) -> Empty:
27  %e : Nat.IsTrue(_)
28  Unit{}
29
30# Bits
31# ----
32
33def first(r: Word(31n) & Bool) -> Word(31n):
34  (m, s) = r
35  m
36
37def split.cons(-n: Nat, b: Bool, r: Word(n) & Bool) -> Word(1n+n) & Bool:
38  (w, s) = r
39  (WCon{b, w}, s)
40
41# a word's first n bits, and its last bit (the sign, for n = 31)
42def split(n: Nat, w: Word(1n+n)) -> Word(n) & Bool:
43  match n:
44    case 0n:
45      match w:
46        case WCon{b, t}:
47          (WNil{}, b)
48    case 1n+p:
49      match w:
50        case WCon{b, t}:
51          split.cons(p, b, split(p, t))
52
53# a word with s appended as its last bit
54def unsplit(n: Nat, w: Word(n), s: Bool) -> Word(1n+n):
55  match n:
56    case 0n:
57      WCon{s, WNil{}}
58    case 1n+p:
59      match w:
60        case WCon{b, t}:
61          WCon{b, unsplit(p, t, s)}
62
63law split_unsplit:
64  for n: Nat
65  for w: Word(n)
66  for s: Bool
67  {(w, s) == split(n, unsplit(n, w, s)) : Word(n) & Bool}
68
69def split_unsplit(n, w, s):
70  match n:
71    case 0n:
72      match w:
73        case WNil{}:
74          {==}
75    case 1n+p:
76      match w:
77        case WCon{b, +t}:
78          %split_unsplit(p, t, s) : {(WCon{b, t}, s) == split.cons(p, b, _) : Word(1n+p) & Bool}
79          {==}
80
81# the 31 bits below the sign: exponent and fraction
82def mag(x: F32) -> Word(31n):
83  match x:
84    case F32{w}:
85      first(split(31n, w))
86
87def neg.go(r: Word(31n) & Bool) -> Word(32n):
88  (m, s) = r
89  unsplit(31n, m, Bool.not(s))
90
91# IEEE 754 negation: the sign bit flipped
92def neg_bits(x: F32) -> F32:
93  match x:
94    case F32{w}:
95      F32{neg.go(split(31n, w))}
96
97# Order
98# -----
99
100# how the IEEE order reads a float: NaN, or a number with a sign and a
101# magnitude.
102# Magnitudes are ordered as integers; above infinity's they are NaNs.
103type Key is Data:
104  KNaN{}
105  Num{neg: Bool, mag: Word(31n)}
106
107def IsKey(k: Key) -> Data:
108  match k:
109    case KNaN{}:
110      Empty
111    case Num{s, m}:
112      Unit
113
114# infinity's magnitude, 0x7F800000
115def inf_mag.go(x: U32) -> F32:
116  match x:
117    case U32{w}:
118      F32{w}
119
120def inf_mag() -> F32:
121  inf_mag.go(2139095040)
122
123def key.cls(s: Bool, m: Word(31n), c: Cmp) -> Key:
124  match c:
125    case LT{}:
126      Num{s, m}
127    case EQ{}:
128      Num{s, m}
129    case GT{}:
130      KNaN{}
131
132def key.go(r: Word(31n) & Bool) -> Key:
133  (+m, s) = r
134  key.cls(s, m, Word.cmp(31n, m, mag(inf_mag())))
135
136def key(x: F32) -> Key:
137  match x:
138    case F32{w}:
139      key.go(split(31n, w))
140
141def zero(m: Word(31n)) -> Bool:
142  Cmp.is_eq(Word.cmp(31n, m, Word.zero(31n)))
143
144def lt.signs(s: Bool, t: Bool, +x: Word(31n), +y: Word(31n)) -> Bool:
145  match s t:
146    case False{} False{}:
147      Cmp.is_lt(Word.cmp(31n, x, y))
148    case True{} True{}:
149      Cmp.is_lt(Word.cmp(31n, y, x))
150    case True{} False{}:
151      Bool.not(Bool.and(zero(x), zero(y)))
152    case False{} True{}:
153      False{}
154
155def lt.key(a: Key, b: Key) -> Bool:
156  match a b:
157    case KNaN{} KNaN{}:
158      False{}
159    case KNaN{} Num{t, y}:
160      False{}
161    case Num{s, x} KNaN{}:
162      False{}
163    case Num{s, x} Num{t, y}:
164      lt.signs(s, t, x, y)
165
166# IEEE 754 a < b: false when either is NaN; -0 and +0 are equal
167def lt_bits(a: F32, b: F32) -> Bool:
168  lt.key(key(a), key(b))
169
170def NotGT(c: Cmp) -> Data:
171  match c:
172    case LT{}:
173      Unit
174    case EQ{}:
175      Unit
176    case GT{}:
177      Empty
178
179def le.signs(s: Bool, t: Bool, +x: Word(31n), +y: Word(31n)) -> Type:
180  match s t:
181    case False{} False{}:
182      NotGT(Word.cmp(31n, x, y))
183    case True{} True{}:
184      NotGT(Word.cmp(31n, y, x))
185    case True{} False{}:
186      Unit
187    case False{} True{}:
188      Nat.IsFalse(lt.signs(True{}, False{}, y, x))
189
190def LE.key(a: Key, b: Key) -> Type:
191  match a b:
192    case KNaN{} KNaN{}:
193      Empty
194    case KNaN{} Num{t, y}:
195      Empty
196    case Num{s, x} KNaN{}:
197      Empty
198    case Num{s, x} Num{t, y}:
199      le.signs(s, t, x, y)
200
201# a <= b in the IEEE order, as a type: Empty when either is NaN
202def LE(a: F32, b: F32) -> Type:
203  LE.key(key(a), key(b))
204
205# Order laws
206# ----------
207
208def swap(c: Cmp) -> Cmp:
209  match c:
210    case LT{}:
211      GT{}
212    case EQ{}:
213      EQ{}
214    case GT{}:
215      LT{}
216
217law bool_cmp_refl:
218  for x: Bool
219  {EQ{} == Bool.cmp(x, x) : Cmp}
220
221def bool_cmp_refl(x):
222  match x:
223    case False{}:
224      {==}
225    case True{}:
226      {==}
227
228law Word.cmp_refl:
229  for +n: Nat
230  for a: Word(n)
231  {EQ{} == Word.cmp(n, a, a) : Cmp}
232
233def Word.cmp_refl(n, a):
234  match n:
235    case 0n:
236      match a:
237        case WNil{}:
238          {==}
239    case 1n+p:
240      match a:
241        case WCon{+x, +at}:
242          %Word.cmp_refl(p, at) : {EQ{} == Word.cmp.fin(x, x, _) : Cmp}
243          bool_cmp_refl(x)
244
245law fin_swap:
246  for c: Cmp
247  for x: Bool
248  for y: Bool
249  {swap(Word.cmp.fin(x, y, c)) == Word.cmp.fin(y, x, swap(c)) : Cmp}
250
251def fin_swap(c, x, y):
252  match c x y:
253    case LT{} x y:
254      {==}
255    case GT{} x y:
256      {==}
257    case EQ{} False{} False{}:
258      {==}
259    case EQ{} False{} True{}:
260      {==}
261    case EQ{} True{} False{}:
262      {==}
263    case EQ{} True{} True{}:
264      {==}
265
266law Word.cmp_swap:
267  for +n: Nat
268  for a: Word(n)
269  for b: Word(n)
270  {swap(Word.cmp(n, a, b)) == Word.cmp(n, b, a) : Cmp}
271
272def Word.cmp_swap(n, a, b):
273  match n:
274    case 0n:
275      match a b:
276        case WNil{} WNil{}:
277          {==}
278    case 1n+p:
279      match a b:
280        case WCon{+x, +at} WCon{+y, +bt}:
281          %Word.cmp_swap(p, at, bt) : {swap(Word.cmp.fin(x, y, Word.cmp(p, at, bt))) == Word.cmp.fin(y, x, _) : Cmp}
282          fin_swap(Word.cmp(p, at, bt), x, y)
283
284law lt_notgt:
285  for c: Cmp
286  {Cmp.is_lt(c) == True{} : Bool} -> NotGT(c)
287
288def lt_notgt(c):
289  match c:
290    case LT{}:
291      e => Unit{}
292    case EQ{}:
293      e => Unit{}
294    case GT{}:
295      e => no_f(e)
296
297law notlt_swap:
298  for c: Cmp
299  {Cmp.is_lt(c) == False{} : Bool} -> NotGT(swap(c))
300
301def notlt_swap(c):
302  match c:
303    case LT{}:
304      e => no_t(e)
305    case EQ{}:
306      e => Unit{}
307    case GT{}:
308      e => Unit{}
309
310law lt_le.signs:
311  for s: Bool
312  for t: Bool
313  for +x: Word(31n)
314  for +y: Word(31n)
315  {lt.signs(s, t, x, y) == True{} : Bool} -> le.signs(s, t, x, y)
316
317def lt_le.signs(s, t, x, y):
318  match s t:
319    case False{} False{}:
320      lt_notgt(Word.cmp(31n, x, y))
321    case True{} True{}:
322      lt_notgt(Word.cmp(31n, y, x))
323    case True{} False{}:
324      e => Unit{}
325    case False{} True{}:
326      e => void(Nat.IsFalse(lt.signs(True{}, False{}, y, x)), no_f(e))
327
328# a < b gives a <= b
329law lt_le.key:
330  for a: Key
331  for b: Key
332  {lt.key(a, b) == True{} : Bool} -> LE.key(a, b)
333
334def lt_le.key(a, b):
335  match a b:
336    case KNaN{} KNaN{}:
337      e => no_f(e)
338    case KNaN{} Num{t, y}:
339      e => no_f(e)
340    case Num{s, x} KNaN{}:
341      e => no_f(e)
342    case Num{s, x} Num{t, y}:
343      lt_le.signs(s, t, x, y)
344
345# only an ordered value is below something
346law lt_key:
347  for a: Key
348  for b: Key
349  {lt.key(a, b) == True{} : Bool} -> IsKey(a)
350
351def lt_key(a, b):
352  match a b:
353    case KNaN{} KNaN{}:
354      e => no_f(e)
355    case KNaN{} Num{t, y}:
356      e => no_f(e)
357    case Num{s, x} KNaN{}:
358      e => Unit{}
359    case Num{s, x} Num{t, y}:
360      e => Unit{}
361
362law le_key_l:
363  for a: Key
364  for b: Key
365  LE.key(a, b) -> IsKey(a)
366
367def le_key_l(a, b):
368  match a b:
369    case KNaN{} KNaN{}:
370      l => l
371    case KNaN{} Num{t, y}:
372      l => l
373    case Num{s, x} KNaN{}:
374      l => Unit{}
375    case Num{s, x} Num{t, y}:
376      l => Unit{}
377
378law le_key_r:
379  for a: Key
380  for b: Key
381  LE.key(a, b) -> IsKey(b)
382
383def le_key_r(a, b):
384  match a b:
385    case KNaN{} KNaN{}:
386      l => l
387    case KNaN{} Num{t, y}:
388      l => void(Unit, l)
389    case Num{s, x} KNaN{}:
390      l => l
391    case Num{s, x} Num{t, y}:
392      l => Unit{}
393
394law le_refl.signs:
395  for s: Bool
396  for +m: Word(31n)
397  le.signs(s, s, m, m)
398
399def le_refl.signs(s, m):
400  match s:
401    case False{}:
402      %Word.cmp_refl(31n, m) : NotGT(_)
403      Unit{}
404    case True{}:
405      %Word.cmp_refl(31n, m) : NotGT(_)
406      Unit{}
407
408law le_refl.key:
409  for k: Key
410  IsKey(k) -> LE.key(k, k)
411
412def le_refl.key(k):
413  match k:
414    case KNaN{}:
415      h => h
416    case Num{s, m}:
417      h => le_refl.signs(s, m)
418
419law total.same:
420  for +x: Word(31n)
421  for +y: Word(31n)
422  for e: {Cmp.is_lt(Word.cmp(31n, x, y)) == False{} : Bool}
423  NotGT(Word.cmp(31n, y, x))
424
425def total.same(x, y, e):
426  %Word.cmp_swap(31n, x, y) : NotGT(_)
427  notlt_swap(Word.cmp(31n, x, y))(e)
428
429law total.mixed:
430  for +x: Word(31n)
431  for +y: Word(31n)
432  for e: {lt.signs(True{}, False{}, x, y) == False{} : Bool}
433  Nat.IsFalse(lt.signs(True{}, False{}, x, y))
434
435def total.mixed(x, y, e):
436  %Equal.sym(Bool, lt.signs(True{}, False{}, x, y), False{}, e) : Nat.IsFalse(_)
437  Unit{}
438
439law total.signs:
440  for s: Bool
441  for t: Bool
442  for +x: Word(31n)
443  for +y: Word(31n)
444  {lt.signs(s, t, x, y) == False{} : Bool} -> le.signs(t, s, y, x)
445
446def total.signs(s, t, x, y):
447  match s t:
448    case False{} False{}:
449      e => total.same(x, y, e)
450    case True{} True{}:
451      e => total.same(y, x, e)
452    case True{} False{}:
453      e => total.mixed(x, y, e)
454    case False{} True{}:
455      e => Unit{}
456
457# two ordered values: not a < b gives b <= a
458law total.key:
459  for a: Key
460  for b: Key
461  IsKey(a) -> IsKey(b) -> {lt.key(a, b) == False{} : Bool} -> LE.key(b, a)
462
463def total.key(a, b):
464  match a b:
465    case KNaN{} KNaN{}:
466      ha => hb => e => ha
467    case KNaN{} Num{t, y}:
468      ha => hb => e => ha
469    case Num{s, x} KNaN{}:
470      ha => hb => e => hb
471    case Num{s, x} Num{t, y}:
472      ha => hb => total.signs(s, t, x, y)
473
474# Laws about Base's F32
475# ---------------------
476
477# the hardware's < is IEEE 754's
478def LtOk() -> Type:
479  @a: F32 -> @b: F32 -> {F32.is_lt(a, b) == lt_bits(a, b) : Bool}
480
481# the hardware's negation flips the sign bit of every non-NaN float. A
482# NaN's sign and payload are left out: the JS lane does not keep them.
483def NegOk() -> Type:
484  @a: F32 -> IsKey(key(a)) -> {F32.neg(a) == neg_bits(a) : F32}
485
486law bits_lt:
487  for ~lt: LtOk()
488  for +a: F32
489  for +b: F32
490  for -c: Bool
491  for e: {F32.is_lt(a, b) == c : Bool}
492  {lt_bits(a, b) == c : Bool}
493
494def bits_lt(lt, a, b, c, e):
495  %lt(a, b) : {_ == c : Bool}
496  e
497
498# Base's F32.min(a, b) is Bool.pick(F32.is_lt(a, b), a, b); as in
499# u32.bend, each .go lemma takes the test's result c and its equation.
500
501law min_le_r.go:
502  for ~lt: LtOk()
503  for +a: F32
504  for +b: F32
505  for c: Bool
506  for e: {F32.is_lt(a, b) == c : Bool}
507  for bb: LE(b, b)
508  LE(Bool.pick(F32, c, a, b), b)
509
510def min_le_r.go(lt, a, b, c, e, bb):
511  match c:
512    case True{}:
513      lt_le.key(key(a), key(b))(bits_lt(~lt, a, b, True{}, e))
514    case False{}:
515      bb
516
517# clamp(x, lo, hi) <= hi for every x, NaN and infinities included
518law clamp_le_hi:
519  for ~lt: LtOk()
520  for +x: F32
521  for +lo: F32
522  for +hi: F32
523  for lh: LE(lo, hi)
524  LE(F32.clamp(x, lo, hi), hi)
525
526def clamp_le_hi(lt, x, lo, hi, lh):
527  +m = F32.max(x, lo)
528  min_le_r.go(~lt, m, hi, F32.is_lt(m, hi), {==}, le_refl.key(key(hi))(le_key_r(key(lo), key(hi))(lh)))
529
530law lo_le_clamp.go:
531  for ~lt: LtOk()
532  for +x: F32
533  for +lo: F32
534  for +hi: F32
535  for c1: Bool
536  for e1: {F32.is_lt(x, lo) == c1 : Bool}
537  for c2: Bool
538  for e2: {F32.is_lt(Bool.pick(F32, c1, lo, x), hi) == c2 : Bool}
539  for lh: LE(lo, hi)
540  LE(lo, Bool.pick(F32, c2, Bool.pick(F32, c1, lo, x), hi))
541
542def lo_le_clamp.go(lt, x, lo, hi, c1, e1, c2, e2, lh):
543  match c1 c2:
544    case True{} True{}:
545      le_refl.key(key(lo))(le_key_l(key(lo), key(hi))(lh))
546    case False{} True{}:
547      total.key(key(x), key(lo))(lt_key(key(x), key(hi))(bits_lt(~lt, x, hi, True{}, e2)))(le_key_l(key(lo), key(hi))(lh))(bits_lt(~lt, x, lo, False{}, e1))
548    case True{} False{}:
549      lh
550    case False{} False{}:
551      lh
552
553# lo <= clamp(x, lo, hi) for every x, when lo <= hi
554law lo_le_clamp:
555  for ~lt: LtOk()
556  for +x: F32
557  for +lo: F32
558  for +hi: F32
559  for lh: LE(lo, hi)
560  LE(lo, F32.clamp(x, lo, hi))
561
562def lo_le_clamp(lt, x, lo, hi, lh):
563  lo_le_clamp.go(~lt, x, lo, hi, F32.is_lt(x, lo), {==}, F32.is_lt(F32.max(x, lo), hi), {==}, lh)
564
565# Negation
566# --------
567
568law neg_mag.go:
569  for r: Word(31n) & Bool
570  {first(r) == first(split(31n, neg.go(r))) : Word(31n)}
571
572def neg_mag.go(r):
573  (+m, +s) = r
574  Equal.cong(Word(31n) & Bool, Word(31n), first, (m, Bool.not(s)), split(31n, unsplit(31n, m, Bool.not(s))), split_unsplit(31n, m, Bool.not(s)))
575
576law neg_mag.bits:
577  for a: F32
578  {mag(a) == mag(neg_bits(a)) : Word(31n)}
579
580def neg_mag.bits(a):
581  match a:
582    case F32{w}:
583      neg_mag.go(split(31n, w))
584
585# |-a| is |a|, bit for bit
586law neg_mag:
587  for ~ng: NegOk()
588  for +a: F32
589  for ka: IsKey(key(a))
590  {mag(a) == mag(F32.neg(a)) : Word(31n)}
591
592def neg_mag(ng, a, ka):
593  %Equal.sym(F32, F32.neg(a), neg_bits(a), ng(a, ka)) : {mag(a) == mag(_) : Word(31n)}
594  neg_mag.bits(a)
595
596# whether a value is NaN does not depend on its sign
597law key_sign:
598  for s: Bool
599  for t: Bool
600  for m: Word(31n)
601  for c: Cmp
602  IsKey(key.cls(s, m, c)) -> IsKey(key.cls(t, m, c))
603
604def key_sign(s, t, m, c):
605  match c:
606    case LT{}:
607      h => Unit{}
608    case EQ{}:
609      h => Unit{}
610    case GT{}:
611      h => h
612
613law neg_key.go:
614  for r: Word(31n) & Bool
615  IsKey(key.go(r)) -> IsKey(key.go(split(31n, neg.go(r))))
616
617def neg_key.go(r):
618  (+m, +s) = r
619  %split_unsplit(31n, m, Bool.not(s)) : IsKey(key.go((m, s))) -> IsKey(key.go(_))
620  key_sign(s, Bool.not(s), m, Word.cmp(31n, m, mag(inf_mag())))
621
622law neg_key.bits:
623  for a: F32
624  IsKey(key(a)) -> IsKey(key(neg_bits(a)))
625
626def neg_key.bits(a):
627  match a:
628    case F32{w}:
629      neg_key.go(split(31n, w))
630
631# the negation of a non-NaN is not NaN
632law neg_key:
633  for ~ng: NegOk()
634  for +a: F32
635  for +ka: IsKey(key(a))
636  IsKey(key(F32.neg(a)))
637
638def neg_key(ng, a, ka):
639  %Equal.sym(F32, F32.neg(a), neg_bits(a), ng(a, ka)) : IsKey(key(_))
640  neg_key.bits(a)(ka)