1	import Base
2	import ../../../spec/math/generic.bend as SG
3	import ../../../spec/lib/common.bend as SC
4	import ../../../src/math/generic.bend as G
5	import ../../../src/math/instances.bend as I
6	import ../../../src/math/num.bend as NM
7	import ../../../src/math/natural.bend as M
8	import ../../lib/nat.bend as N
9	import ../../lib/u32.bend as U
10	import ../../lib/u32div.bend as UD
11	import ../../lib/lemmas/spec/numeric.bend as S
12	import ../../lib/words32.bend as W32
13	import ../../lib/word.bend as WD
14	
15	# The cheap clauses of spec/math/generic.bend proved at U32 for every input:
16	# Abs.identity, Min.agrees, Max.agrees, Sign.agrees and Clamp.agrees (the selections go
17	# through U32.is_lt, which is Nat's order on the values). The other U32
18	# clauses and every U64, F32 and F64 clause are stated and tested
19	# (docs/MATH_CONTRACTS.md).
20	
21	# ---- Nat.min and Nat.max from the order ----
22	
23	def min_of_ge(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == False{} : Bool}) -> {Nat.min(a, b) == a : Nat}:
24	  match a b:
25	    case 0n bb:
26	      {==}
27	    case 1n+ap 0n:
28	      Empty.absurd({Nat.min(1n+ap, 0n) == 1n+ap : Nat}, N.zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
29	    case 1n+ap 1n+bp:
30	      N.succ_cong(Nat.min(ap, bp), ap, min_of_ge(ap, bp, h))
31	
32	def min_of_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == True{} : Bool}) -> {Nat.min(a, b) == b : Nat}:
33	  match a b:
34	    case 0n bb:
35	      Empty.absurd({Nat.min(0n, bb) == bb : Nat}, N.lt_zero_absurd(bb, h))
36	    case 1n+ap 0n:
37	      {==}
38	    case 1n+ap 1n+bp:
39	      N.succ_cong(Nat.min(ap, bp), bp, min_of_lt(ap, bp, h))
40	
41	def max_of_lt(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
42	  match a b:
43	    case 0n bb:
44	      {==}
45	    case 1n+ap 0n:
46	      Empty.absurd({Nat.max(1n+ap, 0n) == 0n : Nat}, N.lt_zero_absurd(1n+ap, h))
47	    case 1n+ap 1n+bp:
48	      N.succ_cong(Nat.max(ap, bp), bp, max_of_lt(ap, bp, h))
49	
50	def max_of_ge(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.max(a, b) == a : Nat}:
51	  match a b:
52	    case 0n 0n:
53	      {==}
54	    case 0n 1n+bp:
55	      Empty.absurd({Nat.max(0n, 1n+bp) == 0n : Nat}, N.zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
56	    case 1n+ap 0n:
57	      {==}
58	    case 1n+ap 1n+bp:
59	      N.succ_cong(Nat.max(ap, bp), ap, max_of_ge(ap, bp, h))
60	
61	# ---- U32 round trip ----
62	
63	# (one and k stay symbolic, so 2^32 is never expanded)
64	def val_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {k == 32n : Nat}, +a: U32) -> {Nat.is_lt(U32.to_nat(a), SC.pow2(k)) == True{} : Bool}:
65	  %Equal.sym(Nat, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k)) : {Nat.is_lt(U32.to_nat(a), _) == True{} : Bool}
66	  %Equal.sym(Nat, k, 32n, hk) : {Nat.is_lt(U32.to_nat(a), WD.sc(_, one)) == True{} : Bool}
67	  UD.vb(one, h1, a)
68	
69	def le_k(+k: Nat, +hk: {k == 32n : Nat}) -> {Nat.is_le(k, 32n) == True{} : Bool}:
70	  %Equal.sym(Nat, k, 32n, hk) : {Nat.is_le(_, 32n) == True{} : Bool}
71	  {==}
72	
73	# a U32 is the U32 of its value
74	def round_trip_k(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {k == 32n : Nat}, +a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
75	  U.injective(U32.from_nat(U32.to_nat(a)), a, U.to_nat_from_nat(U32.to_nat(a), k, le_k(k, hk), val_lt(one, h1, k, hk, a)))
76	
77	def round_trip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
78	  round_trip_k(1n, {==}, 32n, {==}, a)
79	
80	# ---- the clauses ----
81	
82	def abs_identity(+x: U32) -> SG.Abs.identity(~U32, ~I.u32_op, ~I.u32_is, x):
83	  {==}
84	
85	def min_c(+a: U32, +b: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(b), U32.to_nat(a)) == c : Bool}) -> {G.pick(U32, c, b, a) == U32.from_nat(Nat.min(U32.to_nat(a), U32.to_nat(b))) : U32}:
86	  match c:
87	    case True{}:
88	      %Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b), min_of_lt(U32.to_nat(a), U32.to_nat(b), hc)) : {b == U32.from_nat(_) : U32}
89	      Equal.sym(U32, U32.from_nat(U32.to_nat(b)), b, round_trip(b))
90	    case False{}:
91	      %Equal.sym(Nat, Nat.min(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a), min_of_ge(U32.to_nat(a), U32.to_nat(b), hc)) : {a == U32.from_nat(_) : U32}
92	      Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, round_trip(a))
93	
94	def min_agrees(+a: U32, +b: U32) -> SG.Min.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
95	  %Equal.sym(Bool, U32.is_lt(b, a), Nat.is_lt(U32.to_nat(b), U32.to_nat(a)), U.is_lt_nat(b, a)) : {G.pick(U32, _, b, a) == U32.from_nat(Nat.min(U32.to_nat(a), U32.to_nat(b))) : U32}
96	  min_c(a, b, Nat.is_lt(U32.to_nat(b), U32.to_nat(a)), {==})
97	
98	def max_c(+a: U32, +b: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == c : Bool}) -> {G.pick(U32, c, b, a) == U32.from_nat(Nat.max(U32.to_nat(a), U32.to_nat(b))) : U32}:
99	  match c:
100	    case True{}:
101	      %Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(b), max_of_lt(U32.to_nat(a), U32.to_nat(b), hc)) : {b == U32.from_nat(_) : U32}
102	      Equal.sym(U32, U32.from_nat(U32.to_nat(b)), b, round_trip(b))
103	    case False{}:
104	      %Equal.sym(Nat, Nat.max(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(a), max_of_ge(U32.to_nat(a), U32.to_nat(b), hc)) : {a == U32.from_nat(_) : U32}
105	      Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, round_trip(a))
106	
107	def max_agrees(+a: U32, +b: U32) -> SG.Max.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, a, b):
108	  %Equal.sym(Bool, U32.is_lt(a, b), Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), U.is_lt_nat(a, b)) : {G.pick(U32, _, b, a) == U32.from_nat(Nat.max(U32.to_nat(a), U32.to_nat(b))) : U32}
109	  max_c(a, b, Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), {==})
110	
111	# ---- sign: 1 above zero, else the value itself (0) ----
112	
113	def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
114	  N.zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h)))
115	
116	def lt_zero_false(+n: Nat) -> {Nat.is_lt(n, 0n) == False{} : Bool}:
117	  match n:
118	    case 0n:
119	      {==}
120	    case 1n+p:
121	      {==}
122	
123	# 0 < n gives not n < 1
124	def pos_ge_one(+n: Nat, +h: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(n, 1n) == False{} : Bool}:
125	  match n:
126	    case 0n:
127	      Empty.absurd({Nat.is_lt(0n, 1n) == False{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
128	    case 1n+p:
129	      lt_zero_false(p)
130	
131	# not 0 < n gives n < 1
132	def zero_lt_one(+n: Nat, +h: {Nat.is_lt(0n, n) == False{} : Bool}) -> {Nat.is_lt(n, 1n) == True{} : Bool}:
133	  match n:
134	    case 0n:
135	      {==}
136	    case 1n+p:
137	      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, true_ne_false(h))
138	
139	def sign_c(+x: U32, +c: Bool, +hc: {Nat.is_lt(0n, U32.to_nat(x)) == c : Bool}) -> {G.sign_above(~U32, ~I.u32_op, ~I.u32_is, x, c) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}:
140	  match c:
141	    case True{}:
142	      %Equal.sym(Nat, Nat.min(U32.to_nat(x), 1n), 1n, N.min_right(U32.to_nat(x), 1n, pos_ge_one(U32.to_nat(x), hc))) : {1 == U32.from_nat(_) : U32}
143	      {==}
144	    case False{}:
145	      %Equal.sym(Bool, U32.is_lt(x, 0), Nat.is_lt(U32.to_nat(x), 0n), U.is_lt_nat(x, 0)) : {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
146	      %Equal.sym(Bool, Nat.is_lt(U32.to_nat(x), 0n), False{}, lt_zero_false(U32.to_nat(x))) : {G.sign_below(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
147	      %Equal.sym(Nat, Nat.min(U32.to_nat(x), 1n), U32.to_nat(x), N.min_left(U32.to_nat(x), 1n, zero_lt_one(U32.to_nat(x), hc))) : {x == U32.from_nat(_) : U32}
148	      Equal.sym(U32, U32.from_nat(U32.to_nat(x)), x, round_trip(x))
149	
150	def sign_agrees(+x: U32) -> SG.Sign.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x):
151	  %Equal.sym(Bool, U32.is_lt(0, x), Nat.is_lt(0n, U32.to_nat(x)), U.is_lt_nat(0, x)) : {G.sign_above(~U32, ~I.u32_op, ~I.u32_is, x, _) == U32.from_nat(Nat.min(U32.to_nat(x), 1n)) : U32}
152	  sign_c(x, Nat.is_lt(0n, U32.to_nat(x)), {==})
153	
154	# ---- clamp: Domain when hi < lo, else min(max(x, lo), hi) ----
155	
156	def max_val_c(+x: U32, +lo: U32, +c: Bool, +hc: {Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)) == c : Bool}) -> {U32.to_nat(G.pick(U32, c, lo, x)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}:
157	  match c:
158	    case True{}:
159	      Equal.sym(Nat, Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(lo), max_of_lt(U32.to_nat(x), U32.to_nat(lo), hc))
160	    case False{}:
161	      Equal.sym(Nat, Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(x), max_of_ge(U32.to_nat(x), U32.to_nat(lo), hc))
162	
163	# the value of max(x, lo) is the larger value
164	def max_val(+x: U32, +lo: U32) -> {U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}:
165	  %Equal.sym(Bool, U32.is_lt(x, lo), Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)), U.is_lt_nat(x, lo)) : {U32.to_nat(G.pick(U32, _, lo, x)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}
166	  max_val_c(x, lo, Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)), {==})
167	
168	def clamp_c(+x: U32, +lo: U32, +hi: U32, +c: Bool) -> {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, c) == SG.lift(~U32, ~SG.u32_of, M.clamp_ok(U32.to_nat(x), U32.to_nat(lo), U32.to_nat(hi), c)) : Result<&2, &2, NM.NumError, U32>}:
169	  match c:
170	    case True{}:
171	      {==}
172	    case False{}:
173	      %Equal.sym(U32, G.min(~U32, ~I.u32_op, ~I.u32_is, G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo), hi), U32.from_nat(Nat.min(U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)), U32.to_nat(hi))), min_agrees(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo), hi)) : {Done{_} == Done{U32.from_nat(Nat.min(Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(hi)))} : Result<&2, &2, NM.NumError, U32>}
174	      %Equal.sym(Nat, U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)), Nat.max(U32.to_nat(x), U32.to_nat(lo)), max_val(x, lo)) : {Done{U32.from_nat(Nat.min(_, U32.to_nat(hi)))} == Done{U32.from_nat(Nat.min(Nat.max(U32.to_nat(x), U32.to_nat(lo)), U32.to_nat(hi)))} : Result<&2, &2, NM.NumError, U32>}
175	      {==}
176	
177	def clamp_agrees(+x: U32, +lo: U32, +hi: U32) -> SG.Clamp.agrees(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, ~SG.u32_of, x, lo, hi):
178	  %Equal.sym(Bool, U32.is_lt(hi, lo), Nat.is_lt(U32.to_nat(hi), U32.to_nat(lo)), U.is_lt_nat(hi, lo)) : {G.clamp_ok(~U32, ~I.u32_op, ~I.u32_is, x, lo, hi, _) == SG.lift(~U32, ~SG.u32_of, M.clamp(U32.to_nat(x), U32.to_nat(lo), U32.to_nat(hi))) : Result<&2, &2, NM.NumError, U32>}
179	  clamp_c(x, lo, hi, Nat.is_lt(U32.to_nat(hi), U32.to_nat(lo)))