1	import Base
2	import ../../../spec/math/generic.bend as SG
3	import ../../../src/math/generic.bend as G
4	import ../../../src/math/num.bend as N
5	import ../../../src/math/instances.bend as I
6	import ../../../src/math/f64.bend as F
7	
8	# The float clauses of spec/math/generic.bend (FMin.select, FMax.select,
9	# FClamp.select, FAbs.value, FSign.select, FSum.fold, FProd.fold,
10	# FPow.binary), proved once for every instance whose over-tests are False
11	# and then read at F32 (Base's primitives) and F64 (src/math/f64.bend).
12	#
13	# The clauses say how each generic function combines the instance's own
14	# operations (which operation, on which arguments, in which order); they do
15	# not depend on what the operations compute, so they hold for any
16	# operations, IEEE's included. This is the parametric style of Mathlib's
17	# lemmas over a structure (Mathlib.Algebra.Order.*: statements over any
18	# LinearOrder / ring, instantiated per type), and of the "free theorems"
19	# of parametric polymorphism (Wadler, Theorems for free!, 1989).
20	
21	# the instance never reports an overflow (floats round instead)
22	def NoAddOver(~T: Data, ~test: N.Test<T> -> Bool) -> Type:
23	  @+a: T -> @+b: T -> {test(N.AddOver{a, b}) == False{} : Bool}
24	
25	def NoMulOver(~T: Data, ~test: N.Test<T> -> Bool) -> Type:
26	  @+a: T -> @+b: T -> {test(N.MulOver{a, b}) == False{} : Bool}
27	
28	# ---- selections: the two picks agree ----
29	
30	def pick_eq(-T: Data, +c: Bool, +a: T, +b: T) -> {G.pick(T, c, a, b) == SG.pick(T, c, a, b) : T}:
31	  match c:
32	    case True{}:
33	      {==}
34	    case False{}:
35	      {==}
36	
37	def fmin_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +a: T, +b: T) -> SG.FMin.select(~T, ~op, ~test, a, b):
38	  pick_eq(T, test(N.Lt{b, a}), b, a)
39	
40	def fmax_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +a: T, +b: T) -> SG.FMax.select(~T, ~op, ~test, a, b):
41	  pick_eq(T, test(N.Lt{a, b}), b, a)
42	
43	def fclamp_c(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +lo: T, +hi: T, +c: Bool) -> {G.clamp_ok(~T, ~op, ~test, x, lo, hi, c) == SG.fclamp_pick(~T, ~test, x, lo, hi, c) : Result<&2, &2, N.NumError, T>}:
44	  match c:
45	    case True{}:
46	      {==}
47	    case False{}:
48	      %Equal.sym(T, G.pick(T, test(N.Lt{x, lo}), lo, x), SG.pick(T, test(N.Lt{x, lo}), lo, x), pick_eq(T, test(N.Lt{x, lo}), lo, x)) : {Done{G.pick(T, test(N.Lt{hi, _}), hi, _)} == Done{SG.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x))} : Result<&2, &2, N.NumError, T>}
49	      %Equal.sym(T, G.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)), SG.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)), pick_eq(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x))) : {Done{_} == Done{SG.pick(T, test(N.Lt{hi, SG.pick(T, test(N.Lt{x, lo}), lo, x)}), hi, SG.pick(T, test(N.Lt{x, lo}), lo, x))} : Result<&2, &2, N.NumError, T>}
50	      {==}
51	
52	def fclamp_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +lo: T, +hi: T) -> SG.FClamp.select(~T, ~op, ~test, x, lo, hi):
53	  fclamp_c(~T, ~op, ~test, x, lo, hi, test(N.Lt{hi, lo}))
54	
55	def fabs_value(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T) -> SG.FAbs.value(~T, ~op, ~test, x):
56	  {==}
57	
58	def sign_b(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +c: Bool) -> {G.sign_below(~T, ~op, ~test, x, c) == SG.pick(T, c, op(N.Neg{op(N.One{})}), x) : T}:
59	  match c:
60	    case True{}:
61	      {==}
62	    case False{}:
63	      {==}
64	
65	def sign_a(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T, +c: Bool) -> {G.sign_above(~T, ~op, ~test, x, c) == SG.pick(T, c, op(N.One{}), SG.pick(T, test(N.Lt{x, op(N.ZeroOp{})}), op(N.Neg{op(N.One{})}), x)) : T}:
66	  match c:
67	    case True{}:
68	      {==}
69	    case False{}:
70	      sign_b(~T, ~op, ~test, x, test(N.Lt{x, op(N.ZeroOp{})}))
71	
72	def fsign_select(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, +x: T) -> SG.FSign.select(~T, ~op, ~test, x):
73	  sign_a(~T, ~op, ~test, x, test(N.Lt{op(N.ZeroOp{}), x}))
74	
75	# ---- folds: with no overflow the checked fold is the plain fold ----
76	
77	def sum_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~ao: NoAddOver(~T, ~test), xs: List<&2, T>, +acc: T) -> {G.sum_go(~T, ~op, ~test, xs, Some{acc}) == Some{SG.fold_add(~T, ~op, xs, acc)} : Maybe<&2, T>}:
78	  match xs:
79	    case Nil{}:
80	      {==}
81	    case Con{+x, t}:
82	      %Equal.sym(Bool, test(N.AddOver{acc, x}), False{}, ao(acc, x)) : {G.sum_go(~T, ~op, ~test, t, G.fits(T, _, op(N.Add{acc, x}))) == Some{SG.fold_add(~T, ~op, t, op(N.Add{acc, x}))} : Maybe<&2, T>}
83	      sum_fold(~T, ~op, ~test, ~ao, t, op(N.Add{acc, x}))
84	
85	def fsum_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~ao: NoAddOver(~T, ~test), xs: List<&2, T>) -> SG.FSum.fold(~T, ~op, ~test, xs):
86	  %Equal.sym(Maybe<&2, T>, G.sum_go(~T, ~op, ~test, xs, Some{op(N.ZeroOp{})}), Some{SG.fold_add(~T, ~op, xs, op(N.ZeroOp{}))}, sum_fold(~T, ~op, ~test, ~ao, xs, op(N.ZeroOp{}))) : {G.ok(T, _) == Done{SG.fold_add(~T, ~op, xs, op(N.ZeroOp{}))} : Result<&2, &2, N.NumError, T>}
87	  {==}
88	
89	def prod_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), xs: List<&2, T>, +acc: T) -> {G.prod_go(~T, ~op, ~test, xs, Some{acc}) == Some{SG.fold_mul(~T, ~op, xs, acc)} : Maybe<&2, T>}:
90	  match xs:
91	    case Nil{}:
92	      {==}
93	    case Con{+x, t}:
94	      %Equal.sym(Bool, test(N.MulOver{acc, x}), False{}, mo(acc, x)) : {G.prod_go(~T, ~op, ~test, t, G.fits(T, _, op(N.Mul{acc, x}))) == Some{SG.fold_mul(~T, ~op, t, op(N.Mul{acc, x}))} : Maybe<&2, T>}
95	      prod_fold(~T, ~op, ~test, ~mo, t, op(N.Mul{acc, x}))
96	
97	def fprod_fold(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), xs: List<&2, T>) -> SG.FProd.fold(~T, ~op, ~test, xs):
98	  %Equal.sym(Maybe<&2, T>, G.prod_go(~T, ~op, ~test, xs, Some{op(N.One{})}), Some{SG.fold_mul(~T, ~op, xs, op(N.One{}))}, prod_fold(~T, ~op, ~test, ~mo, xs, op(N.One{}))) : {G.ok(T, _) == Done{SG.fold_mul(~T, ~op, xs, op(N.One{}))} : Result<&2, &2, N.NumError, T>}
99	  {==}
100	
101	# ---- pow: square-and-multiply is the specification's binary exponentiation ----
102	
103	# k = 0 is a fixed point of the specification's loop
104	def binpow_zero(~T: Data, ~op: N.Op<T> -> T, fuel: Nat, +b: T, +a: T) -> {SG.binpow(~T, ~op, fuel, 0n, b, a) == a : T}:
105	  match fuel:
106	    case 0n:
107	      {==}
108	    case 1n+f:
109	      binpow_zero(~T, ~op, f, b, a)
110	
111	def sq_val_eq(~T: Data, ~op: N.Op<T> -> T, +c: Bool, +b: T) -> {G.sq_val(~T, ~op, c, b) == SG.pick(T, c, op(N.Mul{b, b}), b) : T}:
112	  match c:
113	    case True{}:
114	      {==}
115	    case False{}:
116	      {==}
117	
118	def sq_ok_eq(~T: Data, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +c: Bool, +b: T) -> {G.sq_ok(~T, ~test, c, b, True{}) == True{} : Bool}:
119	  match c:
120	    case True{}:
121	      %Equal.sym(Bool, test(N.MulOver{b, b}), False{}, mo(b, b)) : {Bool.and(True{}, Bool.not(_)) == True{} : Bool}
122	      {==}
123	    case False{}:
124	      {==}
125	
126	def mul_st_eq(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +d: Bool, +b: T, +a: T) -> {G.mul_st(~T, ~op, ~test, d, b, True{}, (a, True{})) == (SG.pick(T, d, op(N.Mul{a, b}), a), True{}) : T & Bool}:
127	  match d:
128	    case True{}:
129	      %Equal.sym(Bool, test(N.MulOver{a, b}), False{}, mo(a, b)) : {(op(N.Mul{a, b}), Bool.and(Bool.and(True{}, True{}), Bool.not(_))) == (op(N.Mul{a, b}), True{}) : T & Bool}
130	      {==}
131	    case False{}:
132	      {==}
133	
134	def pow_bin(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +fuel: Nat, +k: Nat, +b: T, +a: T) -> {G.pow_go(~T, ~op, ~test, fuel, k, b, True{}, (a, True{})) == Some{SG.binpow(~T, ~op, fuel, k, b, a)} : Maybe<&2, T>}:
135	  match fuel k:
136	    case 0n _:
137	      {==}
138	    case 1n+ +f 0n:
139	      %Equal.sym(T, SG.binpow(~T, ~op, f, 0n, b, a), a, binpow_zero(~T, ~op, f, b, a)) : {Some{a} == Some{_} : Maybe<&2, T>}
140	      {==}
141	    case 1n+ +f 1n+ +j:
142	      %Equal.sym(T & Bool, G.mul_st(~T, ~op, ~test, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), b, True{}, (a, True{})), (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{}), mul_st_eq(~T, ~op, ~test, ~mo, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), b, a)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), G.sq_ok(~T, ~test, Nat.is_lt(1n, 1n+j), b, True{}), _) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
143	      %Equal.sym(Bool, G.sq_ok(~T, ~test, Nat.is_lt(1n, 1n+j), b, True{}), True{}, sq_ok_eq(~T, ~test, ~mo, Nat.is_lt(1n, 1n+j), b)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), _, (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{})) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
144	      %Equal.sym(T, G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), sq_val_eq(~T, ~op, Nat.is_lt(1n, 1n+j), b)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), _, True{}, (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{})) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
145	      pow_bin(~T, ~op, ~test, ~mo, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))
146	
147	def fpow_binary(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +x: T, +k: Nat) -> SG.FPow.binary(~T, ~op, ~test, x, k):
148	  %Equal.sym(Maybe<&2, T>, G.pow_go(~T, ~op, ~test, 1n+k, k, x, True{}, (op(N.One{}), True{})), Some{SG.binpow(~T, ~op, 1n+k, k, x, op(N.One{}))}, pow_bin(~T, ~op, ~test, ~mo, 1n+k, k, x, op(N.One{}))) : {G.ok(T, _) == Done{SG.binpow(~T, ~op, 1n+k, k, x, op(N.One{}))} : Result<&2, &2, N.NumError, T>}
149	  {==}
150	
151	# ---- F32 and F64: the over-tests are False ----
152	
153	def f32_ao(+a: F32, +b: F32) -> {I.f32_is(N.AddOver{a, b}) == False{} : Bool}:
154	  {==}
155	
156	def f32_mo(+a: F32, +b: F32) -> {I.f32_is(N.MulOver{a, b}) == False{} : Bool}:
157	  {==}
158	
159	def f64_ao(+a: F.F64, +b: F.F64) -> {F.f64_is(N.AddOver{a, b}) == False{} : Bool}:
160	  {==}
161	
162	def f64_mo(+a: F.F64, +b: F.F64) -> {F.f64_is(N.MulOver{a, b}) == False{} : Bool}:
163	  {==}
164	
165	def f32_min(+a: F32, +b: F32) -> SG.FMin.select(~F32, ~I.f32_op, ~I.f32_is, a, b):
166	  fmin_select(~F32, ~I.f32_op, ~I.f32_is, a, b)
167	
168	def f32_max(+a: F32, +b: F32) -> SG.FMax.select(~F32, ~I.f32_op, ~I.f32_is, a, b):
169	  fmax_select(~F32, ~I.f32_op, ~I.f32_is, a, b)
170	
171	def f32_clamp(+x: F32, +lo: F32, +hi: F32) -> SG.FClamp.select(~F32, ~I.f32_op, ~I.f32_is, x, lo, hi):
172	  fclamp_select(~F32, ~I.f32_op, ~I.f32_is, x, lo, hi)
173	
174	def f32_abs(+x: F32) -> SG.FAbs.value(~F32, ~I.f32_op, ~I.f32_is, x):
175	  fabs_value(~F32, ~I.f32_op, ~I.f32_is, x)
176	
177	def f32_sign(+x: F32) -> SG.FSign.select(~F32, ~I.f32_op, ~I.f32_is, x):
178	  fsign_select(~F32, ~I.f32_op, ~I.f32_is, x)
179	
180	def f32_sum(xs: List<&2, F32>) -> SG.FSum.fold(~F32, ~I.f32_op, ~I.f32_is, xs):
181	  fsum_fold(~F32, ~I.f32_op, ~I.f32_is, ~(a => b => f32_ao(a, b)), xs)
182	
183	def f32_prod(xs: List<&2, F32>) -> SG.FProd.fold(~F32, ~I.f32_op, ~I.f32_is, xs):
184	  fprod_fold(~F32, ~I.f32_op, ~I.f32_is, ~(a => b => f32_mo(a, b)), xs)
185	
186	def f32_pow(+x: F32, +k: Nat) -> SG.FPow.binary(~F32, ~I.f32_op, ~I.f32_is, x, k):
187	  fpow_binary(~F32, ~I.f32_op, ~I.f32_is, ~(a => b => f32_mo(a, b)), x, k)
188	
189	def f64_min(+a: F.F64, +b: F.F64) -> SG.FMin.select(~F.F64, ~F.f64_op, ~F.f64_is, a, b):
190	  fmin_select(~F.F64, ~F.f64_op, ~F.f64_is, a, b)
191	
192	def f64_max(+a: F.F64, +b: F.F64) -> SG.FMax.select(~F.F64, ~F.f64_op, ~F.f64_is, a, b):
193	  fmax_select(~F.F64, ~F.f64_op, ~F.f64_is, a, b)
194	
195	def f64_clamp(+x: F.F64, +lo: F.F64, +hi: F.F64) -> SG.FClamp.select(~F.F64, ~F.f64_op, ~F.f64_is, x, lo, hi):
196	  fclamp_select(~F.F64, ~F.f64_op, ~F.f64_is, x, lo, hi)
197	
198	def f64_abs(+x: F.F64) -> SG.FAbs.value(~F.F64, ~F.f64_op, ~F.f64_is, x):
199	  fabs_value(~F.F64, ~F.f64_op, ~F.f64_is, x)
200	
201	def f64_sign(+x: F.F64) -> SG.FSign.select(~F.F64, ~F.f64_op, ~F.f64_is, x):
202	  fsign_select(~F.F64, ~F.f64_op, ~F.f64_is, x)
203	
204	def f64_sum(xs: List<&2, F.F64>) -> SG.FSum.fold(~F.F64, ~F.f64_op, ~F.f64_is, xs):
205	  fsum_fold(~F.F64, ~F.f64_op, ~F.f64_is, ~(a => b => f64_ao(a, b)), xs)
206	
207	def f64_prod(xs: List<&2, F.F64>) -> SG.FProd.fold(~F.F64, ~F.f64_op, ~F.f64_is, xs):
208	  fprod_fold(~F.F64, ~F.f64_op, ~F.f64_is, ~(a => b => f64_mo(a, b)), xs)
209	
210	def f64_pow(+x: F.F64, +k: Nat) -> SG.FPow.binary(~F.F64, ~F.f64_op, ~F.f64_is, x, k):
211	  fpow_binary(~F.F64, ~F.f64_op, ~F.f64_is, ~(a => b => f64_mo(a, b)), x, k)