~/jendhub

proofs/math/typed/w64clz.bend

bend-collections-laws-crypto@1.0.0.0 · 208 lines · 34 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
5import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as BT
13import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend as NF
14import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
15import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
16import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
17import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as SR
18import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
19import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW
20
21# Leading zeros: bitlen(x) on a word is M.bit_length(x) (a binary search on
22# the top bit, each step halving the width: 16, 8, 4, 2, 1), and clz(a) is
23# 64 - bit_length(a) (Mathlib Nat.size / Nat.log2 characterisation
24# 2^(L - 1) <= n < 2^L, via bit_length(n) == k + bit_length(n / 2^k)).
25
26def v(+x: U32) -> Nat:
27  U32.to_nat(x)
28
29def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
30  LW.true_ne_false(h)
31
32# bit_length(1 + np) == 1 + bit_length(half(1 + np))
33def bl_succ(+np: Nat) -> {M.bit_length(1n+np) == 1n+M.bit_length(C.half(1n+np)) : Nat}:
34  +d = Nat.div(1n+np, 2n)
35  +hd = NF.half_le(np)
36  +e1 = Equal.trans(Nat, M.bit_length_go(np, d, 1n), 1n+M.bit_length_go(np, d, 0n), 1n+M.bit_length_go(d, d, 0n), BT.go_acc(np, d, 0n), Equal.cong(Nat, Nat, z => 1n+z, M.bit_length_go(np, d, 0n), M.bit_length_go(d, d, 0n), NF.bl_fuel(np, d, d, 0n, NF.bends_self(np, d, hd), NF.bends_self(d, d, N.le_refl(d)))))
37  Equal.trans(Nat, M.bit_length(1n+np), 1n+M.bit_length(d), 1n+M.bit_length(C.half(1n+np)), e1, Equal.cong(Nat, Nat, z => 1n+M.bit_length(z), d, C.half(1n+np), Equal.sym(Nat, C.half(1n+np), d, WA.half_div(1n+np))))
38
39def high0(+p: Nat) -> {C.high(p, 0n) == 0n : Nat}:
40  match p:
41    case 0n:
42      {==}
43    case 1n+ +q:
44      high0(q)
45
46# high(k, n) >= 1: bit_length(n) == k + bit_length(high(k, n))
47def bl_high(+k: Nat, +n: Nat, +h: {Nat.is_le(1n, C.high(k, n)) == True{} : Bool}) -> {M.bit_length(n) == Nat.add(k, M.bit_length(C.high(k, n))) : Nat}:
48  match k n:
49    case 0n _:
50      {==}
51    case 1n+ +p 0n:
52      Empty.absurd({M.bit_length(0n) == Nat.add(1n+p, M.bit_length(C.high(1n+p, 0n))) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, C.high(p, 0n), 0n, high0(p), h))))
53    case 1n+ +p 1n+ +np:
54      Equal.trans(Nat, M.bit_length(1n+np), 1n+M.bit_length(C.half(1n+np)), 1n+Nat.add(p, M.bit_length(C.high(p, C.half(1n+np)))), bl_succ(np), Equal.cong(Nat, Nat, z => 1n+z, M.bit_length(C.half(1n+np)), Nat.add(p, M.bit_length(C.high(p, C.half(1n+np)))), bl_high(p, C.half(1n+np), h)))
55
56def hp_c(+k: Nat, +y: Nat, +h: {Nat.is_le(C.pow2(k), y) == True{} : Bool}, +q: Nat, +hq: {C.high(k, y) == q : Nat}) -> {Nat.is_le(1n, q) == True{} : Bool}:
57  match q:
58    case 0n:
59      +e = Equal.trans(Nat, y, Nat.add(C.low(k, y), C.shift(k, C.high(k, y))), C.low(k, y), WW.low_high(k, y), Equal.trans(Nat, Nat.add(C.low(k, y), C.shift(k, C.high(k, y))), Nat.add(C.low(k, y), C.shift(k, 0n)), C.low(k, y), Equal.cong(Nat, Nat, z => Nat.add(C.low(k, y), C.shift(k, z)), C.high(k, y), 0n, hq), Equal.trans(Nat, Nat.add(C.low(k, y), C.shift(k, 0n)), Nat.add(C.low(k, y), 0n), C.low(k, y), Equal.cong(Nat, Nat, z => Nat.add(C.low(k, y), z), C.shift(k, 0n), 0n, WW.shift_zero(k)), N.add_zero(C.low(k, y)))))
60      +hl = L.subst(Nat, z => {Nat.is_lt(z, C.pow2(k)) == True{} : Bool}, C.low(k, y), y, Equal.sym(Nat, y, C.low(k, y), e), WW.low_lt(k, y))
61      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(y, C.pow2(k)), False{}, Equal.sym(Bool, Nat.is_lt(y, C.pow2(k)), True{}, hl), N.le_not_lt(y, C.pow2(k), h))))
62    case 1n+r:
63      N.zero_le(r)
64
65# 2^k <= y: high(k, y) >= 1
66def high_pos(+k: Nat, +y: Nat, +h: {Nat.is_le(C.pow2(k), y) == True{} : Bool}) -> {Nat.is_le(1n, C.high(k, y)) == True{} : Bool}:
67  hp_c(k, y, h, C.high(k, y), {==})
68
69# ---- the binary search of bitlen ----
70
71def P1(st: Nat & U32) -> Nat:
72  (+b, +y) = st
73  b
74
75def P2(st: Nat & U32) -> U32:
76  (+b, +y) = st
77  y
78
79def INV(+k: Nat, +n: Nat, st: Nat & U32) -> Type:
80  {M.bit_length(n) == Nat.add(P1(st), M.bit_length(v(P2(st)))) : Nat} & {C.fits(k, v(P2(st))) == True{} : Bool}
81
82def eta_step(+k: Nat, st: Nat & U32) -> {X.bl_step(k, st) == X.bl_step(k, (P1(st), P2(st))) : Nat & U32}:
83  match st:
84    case Tuple{+b, +y}:
85      {==}
86
87def eta_fin(st: Nat & U32) -> {X.bl_fin(st) == X.bl_fin((P1(st), P2(st))) : Nat}:
88  match st:
89    case Tuple{+b, +y}:
90      {==}
91
92def blstep_c(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}, +n: Nat, +base: Nat, +y: U32, +hy: {C.fits(Nat.add(k, k), v(y)) == True{} : Bool}, +inv: {M.bit_length(n) == Nat.add(base, M.bit_length(v(y))) : Nat}, +c: Bool, +hc: {U32.is_le(X.pow2(k), y) == c : Bool}) -> INV(k, n, X.bl_pick(y, X.pow2(k), k, base, c)):
93  match c:
94    case True{}:
95      +hle = L.subst(Nat, z => {Nat.is_le(z, v(y)) == True{} : Bool}, v(X.pow2(k)), C.pow2(k), SH.p2v(k, hk), Equal.trans(Bool, Nat.is_le(v(X.pow2(k)), v(y)), U32.is_le(X.pow2(k), y), True{}, Equal.sym(Bool, U32.is_le(X.pow2(k), y), Nat.is_le(v(X.pow2(k)), v(y)), W64S.is_le_nat(X.pow2(k), y)), hc))
96      +hh = C.high(k, v(y))
97      +ed = SR.shrn_high(y, k)
98      +eb = bl_high(k, v(y), high_pos(k, v(y), hle))
99      +e1 = Equal.trans(Nat, M.bit_length(n), Nat.add(base, Nat.add(k, M.bit_length(hh))), Nat.add(Nat.add(base, k), M.bit_length(v(U32.shrn(y, k)))), Equal.trans(Nat, M.bit_length(n), Nat.add(base, M.bit_length(v(y))), Nat.add(base, Nat.add(k, M.bit_length(hh))), inv, Equal.cong(Nat, Nat, z => Nat.add(base, z), M.bit_length(v(y)), Nat.add(k, M.bit_length(hh)), eb)), Equal.trans(Nat, Nat.add(base, Nat.add(k, M.bit_length(hh))), Nat.add(Nat.add(base, k), M.bit_length(hh)), Nat.add(Nat.add(base, k), M.bit_length(v(U32.shrn(y, k)))), Equal.sym(Nat, Nat.add(Nat.add(base, k), M.bit_length(hh)), Nat.add(base, Nat.add(k, M.bit_length(hh))), NA.add_assoc(base, k, M.bit_length(hh))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(base, k), M.bit_length(z)), hh, v(U32.shrn(y, k)), Equal.sym(Nat, v(U32.shrn(y, k)), hh, ed))))
100      +f1 = L.subst(Nat, z => {C.fits(k, z) == True{} : Bool}, hh, v(U32.shrn(y, k)), Equal.sym(Nat, v(U32.shrn(y, k)), hh, ed), SH.fits_high(k, k, v(y), hy))
101      (e1, f1)
102    case False{}:
103      +nl = Equal.trans(Bool, Nat.is_le(C.pow2(k), v(y)), Nat.is_le(v(X.pow2(k)), v(y)), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, v(y)), C.pow2(k), v(X.pow2(k)), Equal.sym(Nat, v(X.pow2(k)), C.pow2(k), SH.p2v(k, hk))), Equal.trans(Bool, Nat.is_le(v(X.pow2(k)), v(y)), U32.is_le(X.pow2(k), y), False{}, Equal.sym(Bool, U32.is_le(X.pow2(k), y), Nat.is_le(v(X.pow2(k)), v(y)), W64S.is_le_nat(X.pow2(k), y)), hc))
104      (inv, WW.fits_of_lt(k, v(y), N.not_le_lt(C.pow2(k), v(y), nl)))
105
106def blstep(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}, +n: Nat, +b: Nat, +y: U32, +hi: {M.bit_length(n) == Nat.add(b, M.bit_length(v(y))) : Nat}, +hy: {C.fits(Nat.add(k, k), v(y)) == True{} : Bool}) -> INV(k, n, X.bl_step(k, (b, y))):
107  blstep_c(k, hk, n, b, y, hy, hi, U32.is_le(X.pow2(k), y), {==})
108
109def small_c(+y: U32, +c: Bool, +hc: {U32.is_lt(y, 1) == c : Bool}, +nv: Nat, +hnv: {v(y) == nv : Nat}, +hy: {C.fits(1n, v(y)) == True{} : Bool}) -> {v(Bool.pick(U32, c, y, 1)) == M.bit_length(v(y)) : Nat}:
110  match c nv:
111    case True{} 0n:
112      Equal.trans(Nat, v(y), 0n, M.bit_length(v(y)), hnv, Equal.cong(Nat, Nat, z => M.bit_length(z), 0n, v(y), Equal.sym(Nat, v(y), 0n, hnv)))
113    case False{} 1n:
114      Equal.cong(Nat, Nat, z => M.bit_length(z), 1n, v(y), Equal.sym(Nat, v(y), 1n, hnv))
115    case True{} 1n+m:
116      +h0 = Equal.trans(Bool, Nat.is_lt(1n+m, 1n), Nat.is_lt(v(y), v(1)), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, 1n), 1n+m, v(y), Equal.sym(Nat, v(y), 1n+m, hnv)), Equal.trans(Bool, Nat.is_lt(v(y), v(1)), U32.is_lt(y, 1), True{}, Equal.sym(Bool, U32.is_lt(y, 1), Nat.is_lt(v(y), v(1)), U.is_lt_nat(y, 1)), hc))
117      Empty.absurd({v(Bool.pick(U32, True{}, y, 1)) == M.bit_length(v(y)) : Nat}, N.lt_zero_absurd(m, h0))
118    case False{} 0n:
119      +h0 = Equal.trans(Bool, Nat.is_lt(0n, 1n), Nat.is_lt(v(y), v(1)), False{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, 1n), 0n, v(y), Equal.sym(Nat, v(y), 0n, hnv)), Equal.trans(Bool, Nat.is_lt(v(y), v(1)), U32.is_lt(y, 1), False{}, Equal.sym(Bool, U32.is_lt(y, 1), Nat.is_lt(v(y), v(1)), U.is_lt_nat(y, 1)), hc))
120      Empty.absurd({v(Bool.pick(U32, False{}, y, 1)) == M.bit_length(v(y)) : Nat}, true_ne_false(h0))
121    case False{} 2n+m:
122      +h0 = L.subst(Nat, z => {C.fits(1n, z) == True{} : Bool}, v(y), 2n+m, hnv, hy)
123      Empty.absurd({v(Bool.pick(U32, False{}, y, 1)) == M.bit_length(v(y)) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, h0)))
124
125
126
127def S0(+x: U32) -> Nat & U32:
128  (0n, x)
129def S1(+x: U32) -> Nat & U32:
130  X.bl_step(16n, (P1(S0(x)), P2(S0(x))))
131def S2(+x: U32) -> Nat & U32:
132  X.bl_step(8n, (P1(S1(x)), P2(S1(x))))
133def S3(+x: U32) -> Nat & U32:
134  X.bl_step(4n, (P1(S2(x)), P2(S2(x))))
135def S4(+x: U32) -> Nat & U32:
136  X.bl_step(2n, (P1(S3(x)), P2(S3(x))))
137def S5(+x: U32) -> Nat & U32:
138  X.bl_step(1n, (P1(S4(x)), P2(S4(x))))
139
140def bl_fin_v(+x: U32, p: INV(1n, v(x), S5(x))) -> {X.bl_fin(S5(x)) == M.bit_length(v(x)) : Nat}:
141  (a, b) = p
142  +em0 = small_c(P2(S5(x)), U32.is_lt(P2(S5(x)), 1), {==}, v(P2(S5(x))), {==}, b)
143  +em = L.subst(U32, w => {v(w) == M.bit_length(v(P2(S5(x)))) : Nat}, Bool.pick(U32, U32.is_lt(P2(S5(x)), 1), P2(S5(x)), 1), U32.min(P2(S5(x)), 1), Equal.sym(U32, U32.min(P2(S5(x)), 1), Bool.pick(U32, U32.is_lt(P2(S5(x)), 1), P2(S5(x)), 1), W64S.min_pick(P2(S5(x)), 1)), em0)
144  Equal.trans(Nat, X.bl_fin(S5(x)), X.bl_fin((P1(S5(x)), P2(S5(x)))), M.bit_length(v(x)), eta_fin(S5(x)), Equal.trans(Nat, Nat.add(P1(S5(x)), v(U32.min(P2(S5(x)), 1))), Nat.add(P1(S5(x)), M.bit_length(v(P2(S5(x))))), M.bit_length(v(x)), Equal.cong(Nat, Nat, z => Nat.add(P1(S5(x)), z), v(U32.min(P2(S5(x)), 1)), M.bit_length(v(P2(S5(x)))), em), Equal.sym(Nat, M.bit_length(v(x)), Nat.add(P1(S5(x)), M.bit_length(v(P2(S5(x))))), a)))
145
146def bstep2(+k: Nat, +hk: {Nat.is_lt(k, 32n) == True{} : Bool}, +n: Nat, +b: Nat, +y: U32, p: {M.bit_length(n) == Nat.add(b, M.bit_length(v(y))) : Nat} & {C.fits(Nat.add(k, k), v(y)) == True{} : Bool}) -> INV(k, n, X.bl_step(k, (b, y))):
147  (a, c) = p
148  blstep(k, hk, n, b, y, a, c)
149
150def Q1(+x: U32) -> INV(16n, v(x), S1(x)):
151  blstep(16n, {==}, v(x), 0n, x, {==}, LW.vb(x))
152
153def Q2(+x: U32) -> INV(8n, v(x), S2(x)):
154  bstep2(8n, {==}, v(x), P1(S1(x)), P2(S1(x)), Q1(x))
155
156def Q3(+x: U32) -> INV(4n, v(x), S3(x)):
157  bstep2(4n, {==}, v(x), P1(S2(x)), P2(S2(x)), Q2(x))
158
159def Q4(+x: U32) -> INV(2n, v(x), S4(x)):
160  bstep2(2n, {==}, v(x), P1(S3(x)), P2(S3(x)), Q3(x))
161
162def Q5(+x: U32) -> INV(1n, v(x), S5(x)):
163  bstep2(1n, {==}, v(x), P1(S4(x)), P2(S4(x)), Q4(x))
164
165def eta_chain(+x: U32) -> {X.bitlen(x) == X.bl_fin(S5(x)) : Nat}:
166  +e1 = {{==} : {X.bl_step(16n, (0n, x)) == S1(x) : Nat & U32}}
167  +e2 = Equal.trans(Nat & U32, X.bl_step(8n, X.bl_step(16n, (0n, x))), X.bl_step(8n, S1(x)), S2(x), Equal.cong(Nat & U32, Nat & U32, z => X.bl_step(8n, z), X.bl_step(16n, (0n, x)), S1(x), e1), eta_step(8n, S1(x)))
168  +e3 = Equal.trans(Nat & U32, X.bl_step(4n, X.bl_step(8n, X.bl_step(16n, (0n, x)))), X.bl_step(4n, S2(x)), S3(x), Equal.cong(Nat & U32, Nat & U32, z => X.bl_step(4n, z), X.bl_step(8n, X.bl_step(16n, (0n, x))), S2(x), e2), eta_step(4n, S2(x)))
169  +e4 = Equal.trans(Nat & U32, X.bl_step(2n, X.bl_step(4n, X.bl_step(8n, X.bl_step(16n, (0n, x))))), X.bl_step(2n, S3(x)), S4(x), Equal.cong(Nat & U32, Nat & U32, z => X.bl_step(2n, z), X.bl_step(4n, X.bl_step(8n, X.bl_step(16n, (0n, x)))), S3(x), e3), eta_step(2n, S3(x)))
170  +e5 = Equal.trans(Nat & U32, X.bl_step(1n, X.bl_step(2n, X.bl_step(4n, X.bl_step(8n, X.bl_step(16n, (0n, x)))))), X.bl_step(1n, S4(x)), S5(x), Equal.cong(Nat & U32, Nat & U32, z => X.bl_step(1n, z), X.bl_step(2n, X.bl_step(4n, X.bl_step(8n, X.bl_step(16n, (0n, x))))), S4(x), e4), eta_step(1n, S4(x)))
171  Equal.cong(Nat & U32, Nat, z => X.bl_fin(z), X.bl_step(1n, X.bl_step(2n, X.bl_step(4n, X.bl_step(8n, X.bl_step(16n, (0n, x)))))), S5(x), e5)
172
173def bitlen_v(+x: U32) -> {X.bitlen(x) == M.bit_length(v(x)) : Nat}:
174  Equal.trans(Nat, X.bitlen(x), X.bl_fin(S5(x)), M.bit_length(v(x)), eta_chain(x), bl_fin_v(x, Q5(x)))
175
176# ---- clz ----
177
178def not_t(+x: Bool, +h: {Bool.not(x) == True{} : Bool}) -> {x == False{} : Bool}:
179  match x:
180    case True{}:
181      Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
182    case False{}:
183      {==}
184
185def not_f(+x: Bool, +h: {Bool.not(x) == False{} : Bool}) -> {x == True{} : Bool}:
186  match x:
187    case True{}:
188      {==}
189    case False{}:
190      Empty.absurd({False{} == True{} : Bool}, true_ne_false(h))
191
192def clz_c(+l: U32, +h: U32, +c: Bool, +hc: {Bool.not(U32.is_zero(h)) == c : Bool}) -> {X.clz_pick(WU.U64{l, h}, c) == Nat.sub(64n, M.bit_length(SW.value(WU.U64{l, h}))) : Nat}:
193  match c:
194    case True{}:
195      +hz = Equal.trans(Bool, Nat.is_eq(v(h), 0n), U32.is_zero(h), False{}, Equal.sym(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), LW.zero_nat(h)), not_t(U32.is_zero(h), hc))
196      +eh = WW.high_u(32n, v(l), v(h), LW.vb(l))
197      +h1 = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, v(h), C.high(32n, SW.value(WU.U64{l, h})), Equal.sym(Nat, C.high(32n, SW.value(WU.U64{l, h})), v(h), eh), WA.pos_ne(v(h), hz))
198      +eb = Equal.trans(Nat, M.bit_length(SW.value(WU.U64{l, h})), Nat.add(32n, M.bit_length(C.high(32n, SW.value(WU.U64{l, h})))), Nat.add(32n, M.bit_length(v(h))), bl_high(32n, SW.value(WU.U64{l, h}), h1), Equal.cong(Nat, Nat, z => Nat.add(32n, M.bit_length(z)), C.high(32n, SW.value(WU.U64{l, h})), v(h), eh))
199      Equal.trans(Nat, Nat.sub(32n, X.bitlen(h)), Nat.sub(32n, M.bit_length(v(h))), Nat.sub(64n, M.bit_length(SW.value(WU.U64{l, h}))), Equal.cong(Nat, Nat, z => Nat.sub(32n, z), X.bitlen(h), M.bit_length(v(h)), bitlen_v(h)), Equal.trans(Nat, Nat.sub(32n, M.bit_length(v(h))), Nat.sub(64n, Nat.add(32n, M.bit_length(v(h)))), Nat.sub(64n, M.bit_length(SW.value(WU.U64{l, h}))), Equal.sym(Nat, Nat.sub(64n, Nat.add(32n, M.bit_length(v(h)))), Nat.sub(32n, M.bit_length(v(h))), NR.sub_cancel_l(32n, 32n, M.bit_length(v(h)))), Equal.cong(Nat, Nat, z => Nat.sub(64n, z), Nat.add(32n, M.bit_length(v(h))), M.bit_length(SW.value(WU.U64{l, h})), Equal.sym(Nat, M.bit_length(SW.value(WU.U64{l, h})), Nat.add(32n, M.bit_length(v(h))), eb))))
200    case False{}:
201      +hz = Equal.trans(Bool, Nat.is_eq(v(h), 0n), U32.is_zero(h), True{}, Equal.sym(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), LW.zero_nat(h)), not_f(U32.is_zero(h), hc))
202      +ev = Equal.trans(Nat, SW.value(WU.U64{l, h}), Nat.add(v(l), C.shift(32n, 0n)), v(l), Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), v(h), 0n, N.eq_from_is_eq(v(h), 0n, hz)), Equal.trans(Nat, Nat.add(v(l), C.shift(32n, 0n)), Nat.add(v(l), 0n), v(l), Equal.cong(Nat, Nat, z => Nat.add(v(l), z), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(l))))
203      Equal.trans(Nat, Nat.sub(64n, X.bitlen(l)), Nat.sub(64n, M.bit_length(v(l))), Nat.sub(64n, M.bit_length(SW.value(WU.U64{l, h}))), Equal.cong(Nat, Nat, z => Nat.sub(64n, z), X.bitlen(l), M.bit_length(v(l)), bitlen_v(l)), Equal.cong(Nat, Nat, z => Nat.sub(64n, M.bit_length(z)), v(l), SW.value(WU.U64{l, h}), Equal.sym(Nat, SW.value(WU.U64{l, h}), v(l), ev)))
204
205def clz_value(+a: WU.U64) -> SW.Clz.value(a):
206  match a:
207    case WU.U64{+l, +h}:
208      clz_c(l, h, Bool.not(U32.is_zero(h)), {==})