1	import Base
2	import ../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	
18	def void(-A: Type, v: Empty) -> A:
19	  match v:
20	
21	# {False == True} and {True == False} are empty
22	def no_f(e: {False{} == True{} : Bool}) -> Empty:
23	  %e : Nat.IsFalse(_)
24	  Unit{}
25	
26	def no_t(e: {True{} == False{} : Bool}) -> Empty:
27	  %e : Nat.IsTrue(_)
28	  Unit{}
29	
30	# Bits
31	# ----
32	
33	def first(r: Word(31n) & Bool) -> Word(31n):
34	  (m, s) = r
35	  m
36	
37	def 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)
42	def 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
54	def 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	
63	law 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	
69	def 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
82	def mag(x: F32) -> Word(31n):
83	  match x:
84	    case F32{w}:
85	      first(split(31n, w))
86	
87	def 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
92	def 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.
103	type Key is Data:
104	  KNaN{}
105	  Num{neg: Bool, mag: Word(31n)}
106	
107	def 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
115	def inf_mag.go(x: U32) -> F32:
116	  match x:
117	    case U32{w}:
118	      F32{w}
119	
120	def inf_mag() -> F32:
121	  inf_mag.go(2139095040)
122	
123	def 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	
132	def key.go(r: Word(31n) & Bool) -> Key:
133	  (+m, s) = r
134	  key.cls(s, m, Word.cmp(31n, m, mag(inf_mag())))
135	
136	def key(x: F32) -> Key:
137	  match x:
138	    case F32{w}:
139	      key.go(split(31n, w))
140	
141	def zero(m: Word(31n)) -> Bool:
142	  Cmp.is_eq(Word.cmp(31n, m, Word.zero(31n)))
143	
144	def 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	
155	def 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
167	def lt_bits(a: F32, b: F32) -> Bool:
168	  lt.key(key(a), key(b))
169	
170	def NotGT(c: Cmp) -> Data:
171	  match c:
172	    case LT{}:
173	      Unit
174	    case EQ{}:
175	      Unit
176	    case GT{}:
177	      Empty
178	
179	def 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	
190	def 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
202	def LE(a: F32, b: F32) -> Type:
203	  LE.key(key(a), key(b))
204	
205	# Order laws
206	# ----------
207	
208	def swap(c: Cmp) -> Cmp:
209	  match c:
210	    case LT{}:
211	      GT{}
212	    case EQ{}:
213	      EQ{}
214	    case GT{}:
215	      LT{}
216	
217	law bool_cmp_refl:
218	  for x: Bool
219	  {EQ{} == Bool.cmp(x, x) : Cmp}
220	
221	def bool_cmp_refl(x):
222	  match x:
223	    case False{}:
224	      {==}
225	    case True{}:
226	      {==}
227	
228	law Word.cmp_refl:
229	  for +n: Nat
230	  for a: Word(n)
231	  {EQ{} == Word.cmp(n, a, a) : Cmp}
232	
233	def 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	
245	law 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	
251	def 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	
266	law 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	
272	def 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	
284	law lt_notgt:
285	  for c: Cmp
286	  {Cmp.is_lt(c) == True{} : Bool} -> NotGT(c)
287	
288	def 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	
297	law notlt_swap:
298	  for c: Cmp
299	  {Cmp.is_lt(c) == False{} : Bool} -> NotGT(swap(c))
300	
301	def 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	
310	law 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	
317	def 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
329	law lt_le.key:
330	  for a: Key
331	  for b: Key
332	  {lt.key(a, b) == True{} : Bool} -> LE.key(a, b)
333	
334	def 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
346	law lt_key:
347	  for a: Key
348	  for b: Key
349	  {lt.key(a, b) == True{} : Bool} -> IsKey(a)
350	
351	def 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	
362	law le_key_l:
363	  for a: Key
364	  for b: Key
365	  LE.key(a, b) -> IsKey(a)
366	
367	def 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	
378	law le_key_r:
379	  for a: Key
380	  for b: Key
381	  LE.key(a, b) -> IsKey(b)
382	
383	def 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	
394	law le_refl.signs:
395	  for s: Bool
396	  for +m: Word(31n)
397	  le.signs(s, s, m, m)
398	
399	def 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	
408	law le_refl.key:
409	  for k: Key
410	  IsKey(k) -> LE.key(k, k)
411	
412	def 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	
419	law 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	
425	def total.same(x, y, e):
426	  %Word.cmp_swap(31n, x, y) : NotGT(_)
427	  notlt_swap(Word.cmp(31n, x, y))(e)
428	
429	law 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	
435	def total.mixed(x, y, e):
436	  %Equal.sym(Bool, lt.signs(True{}, False{}, x, y), False{}, e) : Nat.IsFalse(_)
437	  Unit{}
438	
439	law 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	
446	def 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
458	law 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	
463	def 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
478	def 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.
483	def NegOk() -> Type:
484	  @a: F32 -> IsKey(key(a)) -> {F32.neg(a) == neg_bits(a) : F32}
485	
486	law 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	
494	def 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	
501	law 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	
510	def 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
518	law 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	
526	def 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	
530	law 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	
542	def 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
554	law 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	
562	def 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	
568	law neg_mag.go:
569	  for r: Word(31n) & Bool
570	  {first(r) == first(split(31n, neg.go(r))) : Word(31n)}
571	
572	def 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	
576	law neg_mag.bits:
577	  for a: F32
578	  {mag(a) == mag(neg_bits(a)) : Word(31n)}
579	
580	def 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
586	law 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	
592	def 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
597	law 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	
604	def 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	
613	law neg_key.go:
614	  for r: Word(31n) & Bool
615	  IsKey(key.go(r)) -> IsKey(key.go(split(31n, neg.go(r))))
616	
617	def 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	
622	law neg_key.bits:
623	  for a: F32
624	  IsKey(key(a)) -> IsKey(key(neg_bits(a)))
625	
626	def 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
632	law neg_key:
633	  for ~ng: NegOk()
634	  for +a: F32
635	  for +ka: IsKey(key(a))
636	  IsKey(key(F32.neg(a)))
637	
638	def 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)