PROOF.bend

bend-osdev-word64@0.1.1.0 · 297 lines · 15 definitions

1import Base
2import bend-osdev-u32@0.1.0.0/u32.bend as U
3import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
4import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
5import bend-osdev-word64@0.1.1.0/word64.bend as W
6import bend-osdev-word64@0.1.1.0/proof_value.bend as P
7import bend-osdev-word64@0.1.1.0/proof_shift.bend as PS
8import bend-osdev-word64@0.1.1.0/LAWS.bend as Laws
9import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
10import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
11
12def Laws.add_wraps():
13  {==}
14
15def Laws.sub_wraps():
16  {==}
17
18def Laws.hi_of_parts():
19  {==}
20
21def Laws.lo_of_parts():
22  {==}
23
24def Laws.shl_crosses_halves():
25  {==}
26
27def Laws.shr_crosses_halves():
28  {==}
29
30def Laws.mul_of_max_halves():
31  {==}
32
33def Laws.show_max():
34  {==}
35
36def Laws.show_hex_parts():
37  {==}
38
39def Laws.show_hex_zero():
40  {==}
41
42def Laws.lo_from_u32(a):
43  {==}
44
45def Laws.hi_from_parts(h, l):
46  {==}
47
48def Laws.lo_from_parts(h, l):
49  {==}
50
51def Laws.from_parts_zero_hi(a):
52  {==}
53
54def Laws.from_parts_zero():
55  {==}
56
57def Laws.parts_of(v):
58  match v:
59    case W.W64{h, l}:
60      {==}
61
62# The value and the order (proof_value.bend: the order of two halves of any
63# width, instantiated at 32)
64
65def Laws.to_nat_parts(h, l):
66  {==}
67
68def wp.pick_lex(c: Cmp, -al: U32, -bl: U32) -> {W.W64.cmp.pick(c, al, bl) == P.wv.lex(c, U32.cmp(al, bl)) : Cmp}:
69  match c:
70    case LT{}:
71      {==}
72    case EQ{}:
73      {==}
74    case GT{}:
75      {==}
76
77def Laws.cmp_value(a, b):
78  match a b:
79    case W.W64{U32{+ahw}, U32{+alw}} W.W64{U32{+bhw}, U32{+blw}}:
80      Equal.trans(Cmp, W.W64.cmp.pick(Word.cmp(32n, ahw, bhw), U32{alw}, U32{blw}), P.wv.lex(Word.cmp(32n, ahw, bhw), Word.cmp(32n, alw, blw)), Nat.cmp(P.wv.V(32n, ahw, alw), P.wv.V(32n, bhw, blw)), wp.pick_lex(Word.cmp(32n, ahw, bhw), U32{alw}, U32{blw}), P.wv.gcmp(32n, ahw, alw, bhw, blw))
81
82def Laws.lt_value(a, b):
83  %Laws.cmp_value(a, b) : {Cmp.is_lt(W.W64.cmp(a, b)) == Cmp.is_lt(_) : Bool}
84  {==}
85
86def Laws.le_value(a, b):
87  %Laws.cmp_value(a, b) : {Cmp.is_le(W.W64.cmp(a, b)) == Cmp.is_le(_) : Bool}
88  {==}
89
90def Laws.eq_value(a, b):
91  %Laws.cmp_value(a, b) : {Cmp.is_eq(W.W64.cmp(a, b)) == Cmp.is_eq(_) : Bool}
92  {==}
93
94def wp.of_halves(p: Word(32n) & Word(32n)) -> W.W64:
95  (h, l) = p
96  W.W64{U32{h}, U32{l}}
97
98def Laws.value_eq(a, b, e):
99  match a b:
100    case W.W64{U32{+ahw}, U32{+alw}} W.W64{U32{+bhw}, U32{+blw}}:
101      Equal.cong(Word(32n) & Word(32n), W.W64, p => wp.of_halves(p), (ahw, alw), (bhw, blw), P.wv.halves_eq(32n, ahw, alw, bhw, blw, e))
102
103def Laws.cmp_hi_lt(a, b, h):
104  match a b:
105    case W.W64{ah, al} W.W64{bh, bl}:
106      %Equal.sym(Cmp, U32.cmp(ah, bh), LT{}, h) : {W.W64.cmp.pick(_, al, bl) == LT{} : Cmp}
107      {==}
108
109def Laws.cmp_hi_gt(a, b, h):
110  match a b:
111    case W.W64{ah, al} W.W64{bh, bl}:
112      %Equal.sym(Cmp, U32.cmp(ah, bh), GT{}, h) : {W.W64.cmp.pick(_, al, bl) == GT{} : Cmp}
113      {==}
114
115def Laws.cmp_hi_eq(a, b, h):
116  match a b:
117    case W.W64{ah, +al} W.W64{bh, +bl}:
118      %Equal.sym(Cmp, U32.cmp(ah, bh), EQ{}, h) : {W.W64.cmp.pick(_, al, bl) == U32.cmp(al, bl) : Cmp}
119      {==}
120
121# Addition and subtraction: W64.add and W64.sub are proof_value.bend's
122# halves at width 32, with the carry or borrow between them
123
124def wp.add_split.fin(-ahw: Word(32n), -alw: Word(32n), -bhw: Word(32n), -blw: Word(32n), cb: Bool) -> {W.W64{U32.add(U32{Word.add(32n, ahw, bhw)}, W.W64.bit(cb)), U32{Word.add(32n, alw, blw)}} == W.W64{U32{Word.add(32n, Word.add(32n, ahw, bhw), P.wv.bitw(32n, cb))}, U32{Word.add(32n, alw, blw)}} : W.W64}:
125  match cb:
126    case True{}:
127      {==}
128    case False{}:
129      {==}
130
131def wp.add_split.go(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n), cb: Bool, e: {Cmp.is_lt(Word.cmp(32n, Word.add(32n, alw, blw), alw)) == cb : Bool}) -> {W.W64.add(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.addhi(32n, ahw, alw, bhw, blw)}, U32{Word.add(32n, alw, blw)}} : W.W64}:
132  %Equal.sym(Bool, Cmp.is_lt(Word.cmp(32n, Word.add(32n, alw, blw), alw)), cb, e) : {W.W64{U32.add(U32{Word.add(32n, ahw, bhw)}, W.W64.bit(_)), U32{Word.add(32n, alw, blw)}} == W.W64{U32{Word.add(32n, Word.add(32n, ahw, bhw), P.wv.bitw(32n, _))}, U32{Word.add(32n, alw, blw)}} : W.W64}
133  wp.add_split.fin(ahw, alw, bhw, blw, cb)
134
135def wp.add_split(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n)) -> {W.W64.add(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.addhi(32n, ahw, alw, bhw, blw)}, U32{Word.add(32n, alw, blw)}} : W.W64}:
136  wp.add_split.go(ahw, alw, bhw, blw, Cmp.is_lt(Word.cmp(32n, Word.add(32n, alw, blw), alw)), {==})
137
138def wp.sub_split.fin(-ahw: Word(32n), -alw: Word(32n), -bhw: Word(32n), -blw: Word(32n), cb: Bool) -> {W.W64{U32.sub(U32{Word.sub(32n, ahw, bhw)}, W.W64.bit(cb)), U32{Word.sub(32n, alw, blw)}} == W.W64{U32{Word.sub(32n, Word.sub(32n, ahw, bhw), P.wv.bitw(32n, cb))}, U32{Word.sub(32n, alw, blw)}} : W.W64}:
139  match cb:
140    case True{}:
141      {==}
142    case False{}:
143      {==}
144
145def wp.sub_split.go(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n), cb: Bool, e: {Cmp.is_lt(Word.cmp(32n, alw, blw)) == cb : Bool}) -> {W.W64.sub(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.subhi(32n, ahw, alw, bhw, blw)}, U32{Word.sub(32n, alw, blw)}} : W.W64}:
146  %Equal.sym(Bool, Cmp.is_lt(Word.cmp(32n, alw, blw)), cb, e) : {W.W64{U32.sub(U32{Word.sub(32n, ahw, bhw)}, W.W64.bit(_)), U32{Word.sub(32n, alw, blw)}} == W.W64{U32{Word.sub(32n, Word.sub(32n, ahw, bhw), P.wv.bitw(32n, _))}, U32{Word.sub(32n, alw, blw)}} : W.W64}
147  wp.sub_split.fin(ahw, alw, bhw, blw, cb)
148
149def wp.sub_split(+ahw: Word(32n), +alw: Word(32n), +bhw: Word(32n), +blw: Word(32n)) -> {W.W64.sub(W.W64{U32{ahw}, U32{alw}}, W.W64{U32{bhw}, U32{blw}}) == W.W64{U32{P.wv.subhi(32n, ahw, alw, bhw, blw)}, U32{Word.sub(32n, alw, blw)}} : W.W64}:
150  wp.sub_split.go(ahw, alw, bhw, blw, Cmp.is_lt(Word.cmp(32n, alw, blw)), {==})
151
152def Laws.add_wrap(a, b):
153  match a b:
154    case W.W64{U32{+ahw}, U32{+alw}} W.W64{U32{+bhw}, U32{+blw}}:
155      +x : W.W64 = W.W64{U32{ahw}, U32{alw}}
156      +y : W.W64 = W.W64{U32{bhw}, U32{blw}}
157      +r : W.W64 = W.W64{U32{P.wv.addhi(32n, ahw, alw, bhw, blw)}, U32{Word.add(32n, alw, blw)}}
158      %Equal.sym(W.W64, W.W64.add(x, y), r, wp.add_split(ahw, alw, bhw, blw)) : {Nat.add(W.W64.to_nat(_), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(_, x)))) == Nat.add(W.W64.to_nat(x), W.W64.to_nat(y)) : Nat}
159      %Equal.sym(Bool, W.W64.is_lt(r, x), Nat.is_lt(W.W64.to_nat(r), W.W64.to_nat(x)), Laws.lt_value(r, x)) : {Nat.add(W.W64.to_nat(r), U.U32Nat.dbl(64n, U.U32Nat.bit(_))) == Nat.add(W.W64.to_nat(x), W.W64.to_nat(y)) : Nat}
160      P.wv.gadd(32n, ahw, alw, bhw, blw)
161
162def Laws.add_value(a, b, c, h):
163  match a b c:
164    case W.W64{U32{+ahw}, U32{+alw}} W.W64{U32{+bhw}, U32{+blw}} W.W64{U32{+chw}, U32{+clw}}:
165      +x : W.W64 = W.W64{U32{ahw}, U32{alw}}
166      +y : W.W64 = W.W64{U32{bhw}, U32{blw}}
167      +r : W.W64 = W.W64{U32{P.wv.addhi(32n, ahw, alw, bhw, blw)}, U32{Word.add(32n, alw, blw)}}
168      %Equal.sym(W.W64, W.W64.add(x, y), r, wp.add_split(ahw, alw, bhw, blw)) : {W.W64.to_nat(_) == Nat.add(W.W64.to_nat(x), W.W64.to_nat(y)) : Nat}
169      P.wv.gadd_nowrap(32n, ahw, alw, bhw, blw, chw, clw, h)
170
171def Laws.sub_wrap(a, b):
172  match a b:
173    case W.W64{U32{+ahw}, U32{+alw}} W.W64{U32{+bhw}, U32{+blw}}:
174      +x : W.W64 = W.W64{U32{ahw}, U32{alw}}
175      +y : W.W64 = W.W64{U32{bhw}, U32{blw}}
176      +r : W.W64 = W.W64{U32{P.wv.subhi(32n, ahw, alw, bhw, blw)}, U32{Word.sub(32n, alw, blw)}}
177      %Equal.sym(W.W64, W.W64.sub(x, y), r, wp.sub_split(ahw, alw, bhw, blw)) : {Nat.add(W.W64.to_nat(_), W.W64.to_nat(y)) == Nat.add(W.W64.to_nat(x), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(x, y)))) : Nat}
178      %Equal.sym(Bool, W.W64.is_lt(x, y), Nat.is_lt(W.W64.to_nat(x), W.W64.to_nat(y)), Laws.lt_value(x, y)) : {Nat.add(W.W64.to_nat(r), W.W64.to_nat(y)) == Nat.add(W.W64.to_nat(x), U.U32Nat.dbl(64n, U.U32Nat.bit(_))) : Nat}
179      P.wv.gsub(32n, ahw, alw, bhw, blw)
180
181def Laws.sub_value(a, b, h):
182  +s = W.W64.to_nat(W.W64.sub(a, b))
183  +av = W.W64.to_nat(a)
184  +bv = W.W64.to_nat(b)
185  +el = Equal.trans(Bool, W.W64.is_lt(a, b), Nat.is_lt(av, bv), False{}, Laws.lt_value(a, b), P.wn.le_not_lt(bv, av, h))
186  +e1 = Equal.trans(Nat, Nat.add(s, bv), Nat.add(av, U.U32Nat.dbl(64n, U.U32Nat.bit(False{}))), av, Equal.trans(Nat, Nat.add(s, bv), Nat.add(av, U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(a, b)))), Nat.add(av, U.U32Nat.dbl(64n, U.U32Nat.bit(False{}))), Laws.sub_wrap(a, b), Equal.cong(Bool, Nat, x => Nat.add(av, U.U32Nat.dbl(64n, U.U32Nat.bit(x))), W.W64.is_lt(a, b), False{}, el)), UL.nat_add_zero(av))
187  %e1 : {s == Nat.sub(_, bv) : Nat}
188  Equal.sym(Nat, Nat.sub(Nat.add(s, bv), bv), s, P.wn.sub_add(s, bv))
189
190# Shifts: U32.shln and U32.shrn are proof_shift.bend's ws.shl and ws.shr at
191# width 32; W64.shl and W64.shr are its shifts across two halves
192
193def wq.shln(+w: Word(32n), k: Nat) -> {U32.shln(U32{w}, k) == U32{PS.ws.shl(32n, k, w)} : U32}:
194  match k:
195    case 0n:
196      {==}
197    case 1n+ +p:
198      %Equal.sym(U32, U32.shln(U32{w}, p), U32{PS.ws.shl(32n, p, w)}, wq.shln(w, p)) : {U32.shl(_) == U32{PS.ws.shl(32n, 1n+p, w)} : U32}
199      {==}
200
201def wq.shrn(+w: Word(32n), k: Nat) -> {U32.shrn(U32{w}, k) == U32{PS.ws.shr(32n, k, w)} : U32}:
202  match k:
203    case 0n:
204      {==}
205    case 1n+ +p:
206      %Equal.sym(U32, U32.shrn(U32{w}, p), U32{PS.ws.shr(32n, p, w)}, wq.shrn(w, p)) : {U32.shr(_) == U32{PS.ws.shr(32n, 1n+p, w)} : U32}
207      {==}
208
209def wq.shl.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), +chw: Word(32n), +clw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}, +h: {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{chw}, U32{clw}})) == True{} : Bool}) -> {W.W64.to_nat(W.W64.shl.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}})) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}:
210  match z l32 l64:
211    case True{} _ _:
212      Equal.sym(Nat, U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), Equal.cong(Nat, Nat, v => U.U32Nat.dbl(v, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), k, 0n, PS.ns.eq_zero(k, ez)))
213    case False{} True{} _:
214      %Equal.sym(U32, U32.shln(U32{hw}, k), U32{PS.ws.shl(32n, k, hw)}, wq.shln(hw, k)) : {W.W64.to_nat(W.W64{U32.or(_, U32.shrn(U32{lw}, Nat.sub(32n, k))), U32.shln(U32{lw}, k)}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
215      %Equal.sym(U32, U32.shrn(U32{lw}, Nat.sub(32n, k)), U32{PS.ws.shr(32n, Nat.sub(32n, k), lw)}, wq.shrn(lw, Nat.sub(32n, k))) : {W.W64.to_nat(W.W64{U32.or(U32{PS.ws.shl(32n, k, hw)}, _), U32.shln(U32{lw}, k)}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
216      %Equal.sym(U32, U32.shln(U32{lw}, k), U32{PS.ws.shl(32n, k, lw)}, wq.shln(lw, k)) : {W.W64.to_nat(W.W64{U32.or(U32{PS.ws.shl(32n, k, hw)}, U32{PS.ws.shr(32n, Nat.sub(32n, k), lw)}), _}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
217      PS.ws.gshl_lo(32n, k, hw, lw, chw, clw, e32, h)
218    case False{} False{} True{}:
219      %Equal.sym(U32, U32.shln(U32{lw}, Nat.sub(k, 32n)), U32{PS.ws.shl(32n, Nat.sub(k, 32n), lw)}, wq.shln(lw, Nat.sub(k, 32n))) : {W.W64.to_nat(W.W64{_, 0}) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}
220      PS.ws.gshl_hi(32n, k, hw, lw, chw, clw, PS.ns.le_of_not_lt(k, 32n, e32), h)
221    case False{} False{} False{}:
222      Empty.absurd({W.W64.to_nat(W.W64.shl.pick(False{}, False{}, False{}, k, W.W64{U32{hw}, U32{lw}})) == U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) : Nat}, P.wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 64n), True{}, Equal.sym(Bool, Nat.is_lt(k, 64n), False{}, e64), hk)))
223
224def Laws.shl_value(a, k, c, hk, h):
225  match a c:
226    case W.W64{U32{+hw}, U32{+lw}} W.W64{U32{+chw}, U32{+clw}}:
227      wq.shl.go(Nat.is_eq(k, 0n), Nat.is_lt(k, 32n), Nat.is_lt(k, 64n), k, hw, lw, chw, clw, {==}, {==}, {==}, hk, h)
228
229def wq.shr_le.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64.shr.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}}))), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}:
230  match z l32 l64:
231    case True{} _ _:
232      %Equal.sym(Nat, k, 0n, PS.ns.eq_zero(k, ez)) : {Nat.is_le(U.U32Nat.dbl(_, W.W64.to_nat(W.W64{U32{hw}, U32{lw}})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
233      UL.nat_le_refl(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}))
234    case False{} True{} _:
235      %Equal.sym(U32, U32.shrn(U32{hw}, k), U32{PS.ws.shr(32n, k, hw)}, wq.shrn(hw, k)) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{_, U32.or(U32.shrn(U32{lw}, k), U32.shln(U32{hw}, Nat.sub(32n, k)))})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
236      %Equal.sym(U32, U32.shrn(U32{lw}, k), U32{PS.ws.shr(32n, k, lw)}, wq.shrn(lw, k)) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{PS.ws.shr(32n, k, hw)}, U32.or(_, U32.shln(U32{hw}, Nat.sub(32n, k)))})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
237      %Equal.sym(U32, U32.shln(U32{hw}, Nat.sub(32n, k)), U32{PS.ws.shl(32n, Nat.sub(32n, k), hw)}, wq.shln(hw, Nat.sub(32n, k))) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{U32{PS.ws.shr(32n, k, hw)}, U32.or(U32{PS.ws.shr(32n, k, lw)}, _)})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
238      PS.ws.gshr_lo_le(32n, k, hw, lw, e32)
239    case False{} False{} True{}:
240      %Equal.sym(U32, U32.shrn(U32{hw}, Nat.sub(k, 32n)), U32{PS.ws.shr(32n, Nat.sub(k, 32n), hw)}, wq.shrn(hw, Nat.sub(k, 32n))) : {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64{0, _})), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}
241      PS.ws.gshr_hi_le(32n, k, hw, lw, PS.ns.le_of_not_lt(k, 32n, e32))
242    case False{} False{} False{}:
243      Empty.absurd({Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(W.W64.shr.pick(False{}, False{}, False{}, k, W.W64{U32{hw}, U32{lw}}))), W.W64.to_nat(W.W64{U32{hw}, U32{lw}})) == True{} : Bool}, P.wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 64n), True{}, Equal.sym(Bool, Nat.is_lt(k, 64n), False{}, e64), hk)))
244
245def Laws.shr_value_le(a, k, hk):
246  match a:
247    case W.W64{U32{+hw}, U32{+lw}}:
248      wq.shr_le.go(Nat.is_eq(k, 0n), Nat.is_lt(k, 32n), Nat.is_lt(k, 64n), k, hw, lw, {==}, {==}, {==}, hk)
249
250def wq.shr_lt.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, +hw: Word(32n), +lw: Word(32n), ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64.shr.pick(z, l32, l64, k, W.W64{U32{hw}, U32{lw}})))) == True{} : Bool}:
251  match z l32 l64:
252    case True{} _ _:
253      %Equal.sym(Nat, k, 0n, PS.ns.eq_zero(k, ez)) : {Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(_, 1n+W.W64.to_nat(W.W64{U32{hw}, U32{lw}}))) == True{} : Bool}
254      PS.ns.lt_succ_self(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}))
255    case False{} True{} _:
256      %Equal.sym(U32, U32.shrn(U32{hw}, k), U32{PS.ws.shr(32n, k, hw)}, wq.shrn(hw, k)) : {Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64{_, U32.or(U32.shrn(U32{lw}, k), U32.shln(U32{hw}, Nat.sub(32n, k)))}))) == True{} : Bool}
257      %Equal.sym(U32, U32.shrn(U32{lw}, k), U32{PS.ws.shr(32n, k, lw)}, wq.shrn(lw, k)) : {Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64{U32{PS.ws.shr(32n, k, hw)}, U32.or(_, U32.shln(U32{hw}, Nat.sub(32n, k)))}))) == True{} : Bool}
258      %Equal.sym(U32, U32.shln(U32{hw}, Nat.sub(32n, k)), U32{PS.ws.shl(32n, Nat.sub(32n, k), hw)}, wq.shln(hw, Nat.sub(32n, k))) : {Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64{U32{PS.ws.shr(32n, k, hw)}, U32.or(U32{PS.ws.shr(32n, k, lw)}, _)}))) == True{} : Bool}
259      PS.ws.gshr_lo_lt(32n, k, hw, lw, e32)
260    case False{} False{} True{}:
261      %Equal.sym(U32, U32.shrn(U32{hw}, Nat.sub(k, 32n)), U32{PS.ws.shr(32n, Nat.sub(k, 32n), hw)}, wq.shrn(hw, Nat.sub(k, 32n))) : {Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64{0, _}))) == True{} : Bool}
262      PS.ws.gshr_hi_lt(32n, k, hw, lw, PS.ns.le_of_not_lt(k, 32n, e32))
263    case False{} False{} False{}:
264      Empty.absurd({Nat.is_lt(W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), U.U32Nat.dbl(k, 1n+W.W64.to_nat(W.W64.shr.pick(False{}, False{}, False{}, k, W.W64{U32{hw}, U32{lw}})))) == True{} : Bool}, P.wn.ft(Equal.trans(Bool, False{}, Nat.is_lt(k, 64n), True{}, Equal.sym(Bool, Nat.is_lt(k, 64n), False{}, e64), hk)))
265
266def Laws.shr_value_lt(a, k, hk):
267  match a:
268    case W.W64{U32{+hw}, U32{+lw}}:
269      wq.shr_lt.go(Nat.is_eq(k, 0n), Nat.is_lt(k, 32n), Nat.is_lt(k, 64n), k, hw, lw, {==}, {==}, {==}, hk)
270
271def wq.shlbig.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, -a: W.W64, ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, +h: {Nat.is_le(64n, k) == True{} : Bool}) -> {W.W64.shl.pick(z, l32, l64, k, a) == W.W64.zero() : W.W64}:
272  match z l32 l64:
273    case True{} _ _:
274      Empty.absurd({a == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 64n), False{}, Equal.sym(Bool, Nat.is_lt(k, 64n), Nat.is_lt(0n, 64n), Equal.cong(Nat, Bool, v => Nat.is_lt(v, 64n), k, 0n, PS.ns.eq_zero(k, ez))), P.wn.le_not_lt(64n, k, h))))
275    case False{} True{} _:
276      Empty.absurd({W.W64.shl.pick(False{}, True{}, l64, k, a) == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 32n), False{}, Equal.sym(Bool, Nat.is_lt(k, 32n), True{}, e32), P.wn.le_not_lt(32n, k, UO.nat_le_trans(32n, 64n, k, {==}, h)))))
277    case False{} False{} True{}:
278      Empty.absurd({W.W64.shl.pick(False{}, False{}, True{}, k, a) == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 64n), False{}, Equal.sym(Bool, Nat.is_lt(k, 64n), True{}, e64), P.wn.le_not_lt(64n, k, h))))
279    case False{} False{} False{}:
280      {==}
281
282def Laws.shl_big(a, k, h):
283  wq.shlbig.go(Nat.is_eq(k, 0n), Nat.is_lt(k, 32n), Nat.is_lt(k, 64n), k, a, {==}, {==}, {==}, h)
284
285def wq.shrbig.go(z: Bool, l32: Bool, l64: Bool, +k: Nat, -a: W.W64, ez: {Nat.is_eq(k, 0n) == z : Bool}, e32: {Nat.is_lt(k, 32n) == l32 : Bool}, e64: {Nat.is_lt(k, 64n) == l64 : Bool}, +h: {Nat.is_le(64n, k) == True{} : Bool}) -> {W.W64.shr.pick(z, l32, l64, k, a) == W.W64.zero() : W.W64}:
286  match z l32 l64:
287    case True{} _ _:
288      Empty.absurd({a == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 64n), False{}, Equal.sym(Bool, Nat.is_lt(k, 64n), Nat.is_lt(0n, 64n), Equal.cong(Nat, Bool, v => Nat.is_lt(v, 64n), k, 0n, PS.ns.eq_zero(k, ez))), P.wn.le_not_lt(64n, k, h))))
289    case False{} True{} _:
290      Empty.absurd({W.W64.shr.pick(False{}, True{}, l64, k, a) == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 32n), False{}, Equal.sym(Bool, Nat.is_lt(k, 32n), True{}, e32), P.wn.le_not_lt(32n, k, UO.nat_le_trans(32n, 64n, k, {==}, h)))))
291    case False{} False{} True{}:
292      Empty.absurd({W.W64.shr.pick(False{}, False{}, True{}, k, a) == W.W64.zero() : W.W64}, PS.ns.tf(Equal.trans(Bool, True{}, Nat.is_lt(k, 64n), False{}, Equal.sym(Bool, Nat.is_lt(k, 64n), True{}, e64), P.wn.le_not_lt(64n, k, h))))
293    case False{} False{} False{}:
294      {==}
295
296def Laws.shr_big(a, k, h):
297  wq.shrbig.go(Nat.is_eq(k, 0n), Nat.is_lt(k, 32n), Nat.is_lt(k, 64n), k, a, {==}, {==}, {==}, h)