1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../src/math/w64.bend as X
4	import ../../lib/nat.bend as N
5	import ../../lib/logic.bend as L
6	import ../../lib/word.bend as WD
7	import ../../lib/u32.bend as U
8	import ../../lib/u32div.bend as UD
9	import ../../lib/u32half.bend as UH
10	import ../../lib/u32alg.bend as A
11	import ../u64/u64div.bend as PD
12	import ./u32.bend as U32P
13	import ./width.bend as WW
14	
15	# A shift right by k on a word is division by 2^k: U32.shrn (a single
16	# machine shift) has the value high(k, x), the same as U32.div(x, 2^k) (two
17	# machine divisions), so the two are the same word (Mathlib
18	# Nat.shiftRight_eq_div_pow). The w64 limb code uses shrn; its proofs rewrite
19	# it back to the division by the 2^k table.
20	
21	def v(+x: U32) -> Nat:
22	  U32.to_nat(x)
23	
24	# halving, as the word library and the spec write it
25	def hlf_half(+n: Nat) -> {UH.hlf(n) == C.half(n) : Nat}:
26	  match n:
27	    case 0n:
28	      {==}
29	    case 1n:
30	      {==}
31	    case 2n+q:
32	      Equal.cong(Nat, Nat, z => 1n+z, UH.hlf(q), C.half(q), hlf_half(q))
33	
34	# high(p, half(n)) == half(high(p, n)): both halve p + 1 times
35	def high_half(+p: Nat, +n: Nat) -> {C.high(p, C.half(n)) == C.half(C.high(p, n)) : Nat}:
36	  match p:
37	    case 0n:
38	      {==}
39	    case 1n+q:
40	      high_half(q, C.half(n))
41	
42	# the value of a shift right: high(k, x), for every k
43	def shrn_high(+x: U32, +k: Nat) -> {v(U32.shrn(x, k)) == C.high(k, v(x)) : Nat}:
44	  match k:
45	    case 0n:
46	      {==}
47	    case 1n+p:
48	      +e1 = Equal.trans(Nat, v(U32.shr(U32.shrn(x, p))), UH.hlf(v(U32.shrn(x, p))), C.half(v(U32.shrn(x, p))), UH.shr_value(U32.shrn(x, p)), hlf_half(v(U32.shrn(x, p))))
49	      +e2 = Equal.cong(Nat, Nat, z => C.half(z), v(U32.shrn(x, p)), C.high(p, v(x)), shrn_high(x, p))
50	      Equal.trans(Nat, v(U32.shr(U32.shrn(x, p))), C.half(C.high(p, v(x))), C.high(1n+p, v(x)), Equal.trans(Nat, v(U32.shr(U32.shrn(x, p))), C.half(v(U32.shrn(x, p))), C.half(C.high(p, v(x))), e1, e2), Equal.sym(Nat, C.high(1n+p, v(x)), C.half(C.high(p, v(x))), high_half(p, v(x))))
51	
52	# the 2^k table is the word with bit k set
53	def p2w(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {X.pow2(k) == U32{WD.pw(32n, k)} : U32}:
54	  match k:
55	    case 0n:
56	      {==}
57	    case 1n:
58	      {==}
59	    case 2n:
60	      {==}
61	    case 3n:
62	      {==}
63	    case 4n:
64	      {==}
65	    case 5n:
66	      {==}
67	    case 6n:
68	      {==}
69	    case 7n:
70	      {==}
71	    case 8n:
72	      {==}
73	    case 9n:
74	      {==}
75	    case 10n:
76	      {==}
77	    case 11n:
78	      {==}
79	    case 12n:
80	      {==}
81	    case 13n:
82	      {==}
83	    case 14n:
84	      {==}
85	    case 15n:
86	      {==}
87	    case 16n:
88	      {==}
89	    case 17n:
90	      {==}
91	    case 18n:
92	      {==}
93	    case 19n:
94	      {==}
95	    case 20n:
96	      {==}
97	    case 21n:
98	      {==}
99	    case 22n:
100	      {==}
101	    case 23n:
102	      {==}
103	    case 24n:
104	      {==}
105	    case 25n:
106	      {==}
107	    case 26n:
108	      {==}
109	    case 27n:
110	      {==}
111	    case 28n:
112	      {==}
113	    case 29n:
114	      {==}
115	    case 30n:
116	      {==}
117	    case 31n:
118	      {==}
119	    case 32n+j:
120	      Empty.absurd({X.pow2(32n+j) == U32{WD.pw(32n, 32n+j)} : U32}, N.lt_zero_absurd(j, hk))
121	def p2v(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {v(X.pow2(k)) == C.pow2(k) : Nat}:
122	  Equal.trans(Nat, v(X.pow2(k)), WD.sc(k, 1n), C.pow2(k), PD.pow32(k, hk, 1n, {==}, X.pow2(k), p2w(k, hk)), Equal.sym(Nat, C.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)))
123	
124	def pow2_eq(+k: Nat) -> {C.pow2(k) == 1n+Nat.sub(C.pow2(k), 1n) : Nat}:
125	  Equal.sym(Nat, 1n+Nat.sub(C.pow2(k), 1n), C.pow2(k), N.sub_add(C.pow2(k), 1n, N.pow2_pos(k)))
126	
127	def is_zero_c(+a: U32, +c: Bool, +hc: {U32.is_zero(a) == c : Bool}, +n: Nat, +hn: {v(a) == n : Nat}) -> {c == Nat.is_eq(v(a), 0n) : Bool}:
128	  match c:
129	    case True{}:
130	      %Equal.sym(U32, a, 0, A.eq_of(a, 0, hc)) : {True{} == Nat.is_eq(v(_), 0n) : Bool}
131	      {==}
132	    case False{}:
133	      match n:
134	        case 0n:
135	          +hz = L.subst(U32, z => {U32.is_zero(z) == True{} : Bool}, 0, a, Equal.sym(U32, a, 0, U.injective(a, 0, hn)), {==})
136	          Empty.absurd({False{} == Nat.is_eq(v(a), 0n) : Bool}, U32P.true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(a), False{}, Equal.sym(Bool, U32.is_zero(a), True{}, hz), hc)))
137	        case 1n+ +p:
138	          %Equal.sym(Nat, v(a), 1n+p, hn) : {False{} == Nat.is_eq(_, 0n) : Bool}
139	          {==}
140	
141	def zero_nat(+a: U32) -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}:
142	  is_zero_c(a, U32.is_zero(a), {==}, v(a), {==})
143	
144	# x / 2^k on a word is high(k, x)
145	def div_p2(+x: U32, +k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {v(U32.div(x, X.pow2(k))) == C.high(k, v(x)) : Nat}:
146	  +pp = Nat.sub(C.pow2(k), 1n)
147	  +ev = Equal.trans(Nat, v(X.pow2(k)), C.pow2(k), 1n+pp, p2v(k, hk), pow2_eq(k))
148	  +nz = Equal.trans(Bool, U32.is_zero(X.pow2(k)), Nat.is_eq(v(X.pow2(k)), 0n), False{}, zero_nat(X.pow2(k)), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(X.pow2(k)), 1n+pp, ev))
149	  Equal.trans(Nat, v(U32.div(x, X.pow2(k))), Nat.div(v(x), v(X.pow2(k))), C.high(k, v(x)), UD.div_nat(x, X.pow2(k), nz), Equal.trans(Nat, Nat.div(v(x), v(X.pow2(k))), Nat.div(v(x), 1n+pp), C.high(k, v(x)), Equal.cong(Nat, Nat, t => Nat.div(v(x), t), v(X.pow2(k)), 1n+pp, ev), Equal.sym(Nat, C.high(k, v(x)), Nat.div(v(x), 1n+pp), WW.high_div(k, v(x), pp, pow2_eq(k)))))
150	
151	# U32.shrn(x, k) is U32.div(x, 2^k) for k < 32
152	def shrn_div(+x: U32, +k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}) -> {U32.shrn(x, k) == U32.div(x, X.pow2(k)) : U32}:
153	  U.injective(U32.shrn(x, k), U32.div(x, X.pow2(k)), Equal.trans(Nat, v(U32.shrn(x, k)), C.high(k, v(x)), v(U32.div(x, X.pow2(k))), shrn_high(x, k), Equal.sym(Nat, v(U32.div(x, X.pow2(k))), C.high(k, v(x)), div_p2(x, k, hk))))
154	
155	# the 16-bit split of the limb code
156	def shr16(+x: U32) -> {U32.shrn(x, 16n) == U32.div(x, 65536) : U32}:
157	  shrn_div(x, 16n, {==})