proofs/math/typed/w64add.bend
bend-collections-laws-math@1.0.0.0 · 468 lines · 51 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
5import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
8import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
10import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U3
11import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
12import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
17import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
18import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
19import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
20import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
21import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR2
22
23
24
25
26
27
28
29
30
31def v(+x: U32) -> Nat:
32 U32.to_nat(x)
33
34def val(+l: U32, +h: U32) -> Nat:
35 Nat.add(v(l), C.shift(32n, v(h)))
36
37def bv(c: Bool) -> Nat:
38 S.bit_value(c)
39
40def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:
41 LW.vb(x)
42
43
44def acons(+x: U32, +y: U32) -> {Nat.add(v(U32.add(x, y)), C.shift(32n, bv(P64.carry32(x, y)))) == Nat.add(v(x), v(y)) : Nat}:
45 +c = bv(P64.carry32(x, y))
46 Equal.trans(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, c)), Nat.add(v(U32.add(x, y)), WD.sc(32n, c)), Nat.add(v(x), v(y)), Equal.cong(Nat, Nat, t => Nat.add(v(U32.add(x, y)), t), C.shift(32n, c), WD.sc(32n, c), W64M.shift_sc(32n, c)), P64.add_cons(x, y))
47
48
49def add_alg(+al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +l: Nat, +c1: Nat, +s: Nat, +c2: Nat, +h: Nat, +c3: Nat, +e1: {Nat.add(l, C.shift(32n, c1)) == Nat.add(al, bl) : Nat}, +e2: {Nat.add(s, C.shift(32n, c2)) == Nat.add(ah, bh) : Nat}, +e3: {Nat.add(h, C.shift(32n, c3)) == Nat.add(s, c1) : Nat}) -> {Nat.add(Nat.add(al, C.shift(32n, ah)), Nat.add(bl, C.shift(32n, bh))) == Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))) : Nat}:
50 Equal.trans(Nat, Nat.add(Nat.add(al, C.shift(32n, ah)), Nat.add(bl, C.shift(32n, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))), Equal.trans(Nat, Nat.add(Nat.add(al, C.shift(32n, ah)), Nat.add(bl, C.shift(32n, bh))), Nat.add(Nat.add(al, bl), Nat.add(C.shift(32n, ah), C.shift(32n, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), W64M.add4(al, C.shift(32n, ah), bl, C.shift(32n, bh)), Equal.trans(Nat, Nat.add(Nat.add(al, bl), Nat.add(C.shift(32n, ah), C.shift(32n, bh))), Nat.add(Nat.add(al, bl), C.shift(32n, Nat.add(ah, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(al, bl), t), Nat.add(C.shift(32n, ah), C.shift(32n, bh)), C.shift(32n, Nat.add(ah, bh)), Equal.sym(Nat, C.shift(32n, Nat.add(ah, bh)), Nat.add(C.shift(32n, ah), C.shift(32n, bh)), WW.shift_add(32n, ah, bh))), Equal.trans(Nat, Nat.add(Nat.add(al, bl), C.shift(32n, Nat.add(ah, bh))), Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(ah, bh))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, Nat.add(ah, bh))), Nat.add(al, bl), Nat.add(l, C.shift(32n, c1)), Equal.sym(Nat, Nat.add(l, C.shift(32n, c1)), Nat.add(al, bl), e1)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(ah, bh))), Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(s, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, t)), Nat.add(ah, bh), Nat.add(s, C.shift(32n, c2)), Equal.sym(Nat, Nat.add(s, C.shift(32n, c2)), Nat.add(ah, bh), e2)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, c1)), C.shift(32n, Nat.add(s, C.shift(32n, c2)))), Nat.add(Nat.add(l, C.shift(32n, c1)), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, c1)), t), C.shift(32n, Nat.add(s, C.shift(32n, c2))), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2))), WW.shift_add(32n, s, C.shift(32n, c2))), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, c1)), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, c1), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2))))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), NA.add_assoc(l, C.shift(32n, c1), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(32n, c1), Nat.add(C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))), Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2)))), NA.add_swap(C.shift(32n, c1), C.shift(32n, s), C.shift(32n, C.shift(32n, c2)))))))))), Equal.sym(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, C.shift(32n, Nat.add(c3, c2)))), Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, Nat.add(C.shift(32n, c3), C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, t)), C.shift(32n, Nat.add(c3, c2)), Nat.add(C.shift(32n, c3), C.shift(32n, c2)), WW.shift_add(32n, c3, c2)), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), C.shift(32n, Nat.add(C.shift(32n, c3), C.shift(32n, c2)))), Nat.add(Nat.add(l, C.shift(32n, h)), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(l, C.shift(32n, h)), t), C.shift(32n, Nat.add(C.shift(32n, c3), C.shift(32n, c2))), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))), WW.shift_add(32n, C.shift(32n, c3), C.shift(32n, c2))), Equal.trans(Nat, Nat.add(Nat.add(l, C.shift(32n, h)), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), NA.add_assoc(l, C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Equal.trans(Nat, Nat.add(l, Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))))), Nat.add(l, Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2))), Nat.add(C.shift(32n, h), Nat.add(C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2)))), NA.add_assoc(C.shift(32n, h), C.shift(32n, C.shift(32n, c3)), C.shift(32n, C.shift(32n, c2))))), Equal.trans(Nat, Nat.add(l, Nat.add(Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, Nat.add(h, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, Nat.add(t, C.shift(32n, C.shift(32n, c2)))), Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), C.shift(32n, Nat.add(h, C.shift(32n, c3))), Equal.sym(Nat, C.shift(32n, Nat.add(h, C.shift(32n, c3))), Nat.add(C.shift(32n, h), C.shift(32n, C.shift(32n, c3))), WW.shift_add(32n, h, C.shift(32n, c3)))), Equal.trans(Nat, Nat.add(l, Nat.add(C.shift(32n, Nat.add(h, C.shift(32n, c3))), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, Nat.add(s, c1)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, Nat.add(C.shift(32n, t), C.shift(32n, C.shift(32n, c2)))), Nat.add(h, C.shift(32n, c3)), Nat.add(s, c1), e3), Equal.trans(Nat, Nat.add(l, Nat.add(C.shift(32n, Nat.add(s, c1)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(Nat.add(C.shift(32n, s), C.shift(32n, c1)), C.shift(32n, C.shift(32n, c2)))), Nat.add(l, Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2))))), Equal.cong(Nat, Nat, t => Nat.add(l, Nat.add(t, C.shift(32n, C.shift(32n, c2)))), C.shift(32n, Nat.add(s, c1)), Nat.add(C.shift(32n, s), C.shift(32n, c1)), WW.shift_add(32n, s, c1)), Equal.cong(Nat, Nat, t => Nat.add(l, t), Nat.add(Nat.add(C.shift(32n, s), C.shift(32n, c1)), C.shift(32n, C.shift(32n, c2))), Nat.add(C.shift(32n, s), Nat.add(C.shift(32n, c1), C.shift(32n, C.shift(32n, c2)))), NA.add_assoc(C.shift(32n, s), C.shift(32n, c1), C.shift(32n, C.shift(32n, c2)))))))))))))
51
52def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
53 LW.true_ne_false(h)
54
55
56def add_eq(+al: U32, +ah: U32, +bl: U32, +bh: U32) -> {Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))) == Nat.add(Nat.add(v(U32.add(al, bl)), C.shift(32n, v(U32.add(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al)))))), C.shift(64n, Nat.add(bv(P64.carry32(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al)))), bv(P64.carry32(ah, bh))))) : Nat}:
57 +l = U32.add(al, bl)
58 +c1b = U32.is_lt(l, al)
59 +s = U32.add(ah, bh)
60 +cb = X.b32(c1b)
61 +h = U32.add(s, cb)
62 +q1 = P64.carry32(al, bl)
63 +q2 = P64.carry32(ah, bh)
64 +q3 = P64.carry32(s, cb)
65 +e1 = acons(al, bl)
66 +e2 = acons(ah, bh)
67 +ecb = Equal.trans(Nat, v(cb), bv(c1b), bv(q1), W64M.b32_v(c1b), Equal.cong(Bool, Nat, t => bv(t), c1b, q1, P64.add_lt(al, bl)))
68 +e3 = Equal.trans(Nat, Nat.add(v(h), C.shift(32n, bv(q3))), Nat.add(v(s), v(cb)), Nat.add(v(s), bv(q1)), acons(s, cb), Equal.cong(Nat, Nat, t => Nat.add(v(s), t), v(cb), bv(q1), ecb))
69 +q = Nat.add(bv(q3), bv(q2))
70 +eq = add_alg(v(al), v(ah), v(bl), v(bh), v(l), bv(q1), v(s), bv(q2), v(h), bv(q3), e1, e2, e3)
71 +e64 = WW.shift_comp(32n, 32n, q)
72 Equal.trans(Nat, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(Nat.add(v(l), C.shift(32n, v(h))), C.shift(32n, C.shift(32n, q))), Nat.add(Nat.add(v(l), C.shift(32n, v(h))), C.shift(64n, q)), eq, Equal.cong(Nat, Nat, t => Nat.add(Nat.add(v(l), C.shift(32n, v(h))), t), C.shift(32n, C.shift(32n, q)), C.shift(64n, q), Equal.sym(Nat, C.shift(64n, q), C.shift(32n, C.shift(32n, q)), e64)))
73
74def add_value(+a: WU.U64, +b: WU.U64) -> SW.Add.value(a, b):
75 match a b:
76 case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
77 +R = Nat.add(v(U32.add(al, bl)), C.shift(32n, v(U32.add(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al))))))
78 +q = Nat.add(bv(P64.carry32(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al)))), bv(P64.carry32(ah, bh)))
79 +hR = WW.limbs_fit(32n, 32n, v(U32.add(al, bl)), v(U32.add(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al)))), vb(U32.add(al, bl)), vb(U32.add(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al)))))
80 +lq = Equal.trans(Nat, C.low(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), C.low(64n, Nat.add(R, C.shift(64n, q))), R, Equal.cong(Nat, Nat, t => C.low(64n, t), Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(R, C.shift(64n, q)), add_eq(al, ah, bl, bh)), WW.low_u(64n, R, q, hR))
81 Equal.sym(Nat, C.low(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), R, lq)
82
83def plus1(+x: Nat) -> {Nat.add(x, 1n) == 1n+x : Nat}:
84 Equal.trans(Nat, Nat.add(x, 1n), 1n+Nat.add(x, 0n), 1n+x, NA.add_succ(x, 0n), Equal.cong(Nat, Nat, t => 1n+t, Nat.add(x, 0n), x, N.add_zero(x)))
85
86
87def acons_o(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32) -> {Nat.add(v(U32.add(x, y)), C.shift(32n, WD.bo(P64.carry32(x, y), one))) == Nat.add(v(x), v(y)) : Nat}:
88 +c = P64.carry32(x, y)
89 Equal.trans(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, WD.bo(c, one))), Nat.add(v(U32.add(x, y)), C.shift(32n, bv(c))), Nat.add(v(x), v(y)), Equal.cong(Nat, Nat, t => Nat.add(v(U32.add(x, y)), C.shift(32n, t)), WD.bo(c, one), bv(c), WD.bo_bit(c, one, h1)), acons(x, y))
90
91
92def no_carry(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +c: Bool, +t: Nat, +e: {Nat.add(r, C.shift(32n, WD.bo(c, one))) == t : Nat}, +ht: {C.fits(32n, t) == True{} : Bool}) -> {c == False{} : Bool}:
93 match c:
94 case False{}:
95 {==}
96 case True{}:
97 Empty.absurd({True{} == False{} : Bool}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, t), False{}, Equal.sym(Bool, C.fits(32n, t), True{}, ht), Equal.trans(Bool, C.fits(32n, t), C.fits(32n, Nat.add(r, C.shift(32n, one))), False{}, Equal.cong(Nat, Bool, z => C.fits(32n, z), t, Nat.add(r, C.shift(32n, one)), Equal.sym(Nat, Nat.add(r, C.shift(32n, one)), t, e)), WW.unfit_one(32n, one, h1, r)))))
98
99
100def c_one(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +vs: Nat, +vm: Nat, +cc: Bool, +e: {Nat.add(r, C.shift(32n, WD.bo(cc, one))) == Nat.add(vs, 1n) : Nat}, +em: {1n+vm == C.shift(32n, one) : Nat}, +hr: {C.fits(32n, r) == True{} : Bool}, +hs: {C.fits(32n, vs) == True{} : Bool}) -> {cc == Nat.is_eq(vs, vm) : Bool}:
101 match cc:
102 case True{}:
103 +hs1 = L.subst(Nat, z => {Nat.is_lt(vs, z) == True{} : Bool}, C.shift(32n, one), 1n+vm, Equal.sym(Nat, 1n+vm, C.shift(32n, one), em), WW.lt_one(32n, one, h1, vs, hs))
104 +hle = N.lt_succ_le(vs, vm, hs1)
105 +e2 = Equal.trans(Nat, Nat.add(r, 1n+vm), Nat.add(r, C.shift(32n, one)), 1n+vs, Equal.cong(Nat, Nat, z => Nat.add(r, z), 1n+vm, C.shift(32n, one), em), Equal.trans(Nat, Nat.add(r, C.shift(32n, one)), Nat.add(vs, 1n), 1n+vs, e, plus1(vs)))
106 +hge0 = L.subst(Nat, z => {Nat.is_le(1n+vm, z) == True{} : Bool}, Nat.add(r, 1n+vm), 1n+vs, e2, L.subst(Nat, z => {Nat.is_le(1n+vm, z) == True{} : Bool}, Nat.add(1n+vm, r), Nat.add(r, 1n+vm), N.add_comm(1n+vm, r), N.le_add_right(1n+vm, r)))
107 +eqv = N.le_antisym(vs, vm, hle, hge0)
108 Equal.sym(Bool, Nat.is_eq(vs, vm), True{}, L.subst(Nat, z => {Nat.is_eq(z, vm) == True{} : Bool}, vm, vs, Equal.sym(Nat, vs, vm, eqv), N.is_eq_refl(vm)))
109 case False{}:
110 +e0 = Equal.trans(Nat, r, Nat.add(r, 0n), 1n+vs, Equal.sym(Nat, Nat.add(r, 0n), r, N.add_zero(r)), Equal.trans(Nat, Nat.add(r, 0n), Nat.add(r, C.shift(32n, 0n)), 1n+vs, Equal.cong(Nat, Nat, z => Nat.add(r, z), 0n, C.shift(32n, 0n), Equal.sym(Nat, C.shift(32n, 0n), 0n, WW.shift_zero(32n))), Equal.trans(Nat, Nat.add(r, C.shift(32n, 0n)), Nat.add(vs, 1n), 1n+vs, e, plus1(vs))))
111 +hr1 = L.subst(Nat, z => {Nat.is_lt(r, z) == True{} : Bool}, C.shift(32n, one), 1n+vm, Equal.sym(Nat, 1n+vm, C.shift(32n, one), em), WW.lt_one(32n, one, h1, r, hr))
112 +hlt = L.subst(Nat, z => {Nat.is_lt(z, 1n+vm) == True{} : Bool}, r, 1n+vs, e0, hr1)
113 Equal.sym(Bool, Nat.is_eq(vs, vm), False{}, N.is_eq_lt(vs, vm, hlt))
114
115
116def c3_eq(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +c: Bool, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}) -> {P64.carry32(s, X.b32(c)) == Bool.and(c, U32.is_eq(s, m)) : Bool}:
117 match c:
118 case False{}:
119 +ht = L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, v(s), Nat.add(v(s), 0n), Equal.sym(Nat, Nat.add(v(s), 0n), v(s), N.add_zero(v(s))), vb(s))
120 no_carry(one, h1, v(U32.add(s, 0)), P64.carry32(s, 0), Nat.add(v(s), 0n), acons_o(one, h1, s, 0), ht)
121 case True{}:
122 +em = Equal.trans(Nat, 1n+v(m), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, m, pm), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))
123 +c1 = c_one(one, h1, v(U32.add(s, 1)), v(s), v(m), P64.carry32(s, 1), acons_o(one, h1, s, 1), em, vb(U32.add(s, 1)), vb(s))
124 Equal.trans(Bool, P64.carry32(s, 1), Nat.is_eq(v(s), v(m)), U32.is_eq(s, m), c1, Equal.sym(Bool, U32.is_eq(s, m), Nat.is_eq(v(s), v(m)), LW.eq_nat(s, m)))
125
126def aog(+s: U32, +ah: U32, c: Bool, +m: U32) -> Bool:
127 Bool.or(U32.is_lt(s, ah), Bool.and(c, U32.is_eq(s, m)))
128
129def or_bits(+c2: Bool, +c3: Bool) -> {Bool.or(c2, c3) == Bool.not(Nat.is_eq(Nat.add(bv(c3), bv(c2)), 0n)) : Bool}:
130 match c2 c3:
131 case True{} True{}:
132 {==}
133 case True{} False{}:
134 {==}
135 case False{} True{}:
136 {==}
137 case False{} False{}:
138 {==}
139
140def over_g(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}) -> {aog(U32.add(ah, bh), ah, U32.is_lt(U32.add(al, bl), al), m) == Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))) : Bool}:
141 +s = U32.add(ah, bh)
142 +c1b = U32.is_lt(U32.add(al, bl), al)
143 +q2 = P64.carry32(ah, bh)
144 +q3 = P64.carry32(s, X.b32(c1b))
145 +R = Nat.add(v(U32.add(al, bl)), C.shift(32n, v(U32.add(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al))))))
146 +q = Nat.add(bv(P64.carry32(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al)))), bv(P64.carry32(ah, bh)))
147 +hR = WW.limbs_fit(32n, 32n, v(U32.add(al, bl)), v(U32.add(s, X.b32(c1b))), vb(U32.add(al, bl)), vb(U32.add(s, X.b32(c1b))))
148 +ea = Equal.trans(Bool, aog(s, ah, c1b, m), Bool.or(q2, Bool.and(c1b, U32.is_eq(s, m))), Bool.or(q2, q3), Equal.cong(Bool, Bool, t => Bool.or(t, Bool.and(c1b, U32.is_eq(s, m))), U32.is_lt(s, ah), q2, P64.add_lt(ah, bh)), Equal.cong(Bool, Bool, t => Bool.or(q2, t), Bool.and(c1b, U32.is_eq(s, m)), q3, Equal.sym(Bool, q3, Bool.and(c1b, U32.is_eq(s, m)), c3_eq(one, h1, s, c1b, m, pm))))
149 +eb = Equal.trans(Nat, C.high(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), C.high(64n, Nat.add(R, C.shift(64n, q))), q, Equal.cong(Nat, Nat, t => C.high(64n, t), Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(R, C.shift(64n, q)), add_eq(al, ah, bl, bh)), WW.high_u(64n, R, q, hR))
150 +ec = Equal.cong(Nat, Bool, t => Bool.not(Nat.is_eq(t, 0n)), C.high(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), q, eb)
151 Equal.trans(Bool, aog(s, ah, c1b, m), Bool.or(q2, q3), Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))), ea, Equal.trans(Bool, Bool.or(q2, q3), Bool.not(Nat.is_eq(q, 0n)), Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))), or_bits(q2, q3), Equal.sym(Bool, Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))), Bool.not(Nat.is_eq(q, 0n)), ec)))
152
153def add_over_value(+a: WU.U64, +b: WU.U64) -> SW.AddOver.value(a, b):
154 match a b:
155 case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
156 over_g(1n, {==}, al, ah, bl, bh, 4294967295, {==})
157
158
159
160def iz_n(+x: Nat, +y: Nat) -> {Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(y, 0n)) == Nat.is_eq(Nat.add(x, C.shift(32n, y)), 0n) : Bool}:
161 match x:
162 case 0n:
163 Equal.sym(Bool, Nat.is_eq(C.shift(32n, y), 0n), Nat.is_eq(y, 0n), WW.shift_eq0(32n, y))
164 case 1n+xp:
165 {==}
166
167def is_zero_value(+a: WU.U64) -> SW.IsZero.value(a):
168 match a:
169 case WU.U64{+l, +h}:
170 Equal.trans(Bool, Bool.and(U32.is_zero(l), U32.is_zero(h)), Bool.and(Nat.is_eq(v(l), 0n), Nat.is_eq(v(h), 0n)), Nat.is_eq(val(l, h), 0n), Equal.trans(Bool, Bool.and(U32.is_zero(l), U32.is_zero(h)), Bool.and(Nat.is_eq(v(l), 0n), U32.is_zero(h)), Bool.and(Nat.is_eq(v(l), 0n), Nat.is_eq(v(h), 0n)), Equal.cong(Bool, Bool, t => Bool.and(t, U32.is_zero(h)), U32.is_zero(l), Nat.is_eq(v(l), 0n), LW.zero_nat(l)), Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(v(l), 0n), t), U32.is_zero(h), Nat.is_eq(v(h), 0n), LW.zero_nat(h))), iz_n(v(l), v(h)))
171
172
173
174def eq_value(+a: WU.U64, +b: WU.U64) -> SW.Eq.value(a, b):
175 match a b:
176 case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
177 +e1 = Equal.trans(Bool, Bool.and(U32.is_eq(al, bl), U32.is_eq(ah, bh)), Bool.and(Nat.is_eq(v(al), v(bl)), U32.is_eq(ah, bh)), Bool.and(Nat.is_eq(v(al), v(bl)), Nat.is_eq(v(ah), v(bh))), Equal.cong(Bool, Bool, t => Bool.and(t, U32.is_eq(ah, bh)), U32.is_eq(al, bl), Nat.is_eq(v(al), v(bl)), LW.eq_nat(al, bl)), Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(v(al), v(bl)), t), U32.is_eq(ah, bh), Nat.is_eq(v(ah), v(bh)), LW.eq_nat(ah, bh)))
178 Equal.trans(Bool, Bool.and(U32.is_eq(al, bl), U32.is_eq(ah, bh)), Bool.and(Nat.is_eq(v(al), v(bl)), Nat.is_eq(v(ah), v(bh))), Nat.is_eq(val(al, ah), val(bl, bh)), e1, WW.eq_limbs(32n, v(al), v(ah), v(bl), v(bh), vb(al), vb(bl)))
179
180def lt_value(+a: WU.U64, +b: WU.U64) -> SW.Lt.value(a, b):
181 match a b:
182 case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
183 +x = Bool.or(U32.is_lt(ah, bh), Bool.and(U32.is_eq(ah, bh), U32.is_lt(al, bl)))
184 +y1 = Bool.or(Nat.is_lt(v(ah), v(bh)), Bool.and(U32.is_eq(ah, bh), U32.is_lt(al, bl)))
185 +y2 = Bool.or(Nat.is_lt(v(ah), v(bh)), Bool.and(Nat.is_eq(v(ah), v(bh)), U32.is_lt(al, bl)))
186 +y3 = Bool.or(Nat.is_lt(v(ah), v(bh)), Bool.and(Nat.is_eq(v(ah), v(bh)), Nat.is_lt(v(al), v(bl))))
187 +e1 = Equal.cong(Bool, Bool, t => Bool.or(t, Bool.and(U32.is_eq(ah, bh), U32.is_lt(al, bl))), U32.is_lt(ah, bh), Nat.is_lt(v(ah), v(bh)), U3.is_lt_nat(ah, bh))
188 +e2 = Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(v(ah), v(bh)), Bool.and(t, U32.is_lt(al, bl))), U32.is_eq(ah, bh), Nat.is_eq(v(ah), v(bh)), LW.eq_nat(ah, bh))
189 +e3 = Equal.cong(Bool, Bool, t => Bool.or(Nat.is_lt(v(ah), v(bh)), Bool.and(Nat.is_eq(v(ah), v(bh)), t)), U32.is_lt(al, bl), Nat.is_lt(v(al), v(bl)), U3.is_lt_nat(al, bl))
190 Equal.trans(Bool, x, y1, Nat.is_lt(val(al, ah), val(bl, bh)), e1, Equal.trans(Bool, y1, y2, Nat.is_lt(val(al, ah), val(bl, bh)), e2, Equal.trans(Bool, y2, y3, Nat.is_lt(val(al, ah), val(bl, bh)), e3, WW.lt_limbs(32n, v(al), v(ah), v(bl), v(bh), vb(al), vb(bl)))))
191
192def nle(+a: Nat, +b: Nat, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {Bool.not(c) == Nat.is_le(b, a) : Bool}:
193 match c:
194 case True{}:
195 Equal.sym(Bool, Nat.is_le(b, a), False{}, N.lt_not_le(a, b, hc))
196 case False{}:
197 Equal.sym(Bool, Nat.is_le(b, a), True{}, N.not_lt_le(a, b, hc))
198
199def le_value(+a: WU.U64, +b: WU.U64) -> SW.Le.value(a, b):
200 Equal.trans(Bool, Bool.not(X.lt(b, a)), Bool.not(Nat.is_lt(SW.value(b), SW.value(a))), Nat.is_le(SW.value(a), SW.value(b)), Equal.cong(Bool, Bool, t => Bool.not(t), X.lt(b, a), Nat.is_lt(SW.value(b), SW.value(a)), lt_value(b, a)), nle(SW.value(b), SW.value(a), Nat.is_lt(SW.value(b), SW.value(a)), {==}))
201
202def odd_value(+a: WU.U64) -> SW.Odd.value(a):
203 match a:
204 case WU.U64{+l, +h}:
205 Equal.trans(Bool, U32.is_eq(U32.and(l, 1), 1), Nat.is_eq(Nat.mod(v(l), 2n), 1n), Nat.is_eq(Nat.mod(val(l, h), 2n), 1n), LW.tests_odd(l), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 1n), Nat.mod(v(l), 2n), Nat.mod(val(l, h), 2n), Equal.sym(Nat, Nat.mod(val(l, h), 2n), Nat.mod(v(l), 2n), WW.odd_limb(31n, v(l), v(h)))))
206
207
208
209def chh(+n: Nat) -> {C.half(n) == UH.hlf(n) : Nat}:
210 match n:
211 case 0n:
212 {==}
213 case 1n:
214 {==}
215 case 2n+ +q:
216 Equal.cong(Nat, Nat, t => 1n+t, C.half(q), UH.hlf(q), chh(q))
217
218def half_div(+n: Nat) -> {C.half(n) == Nat.div(n, 2n) : Nat}:
219 Equal.trans(Nat, C.half(n), UH.hlf(n), Nat.div(n, 2n), chh(n), LW.hlf_div2(n))
220
221
222def add_exact(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +hf: {C.fits(32n, Nat.add(v(x), v(y))) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}:
223 +cc = P64.carry32(x, y)
224 +e = acons_o(one, h1, x, y)
225 +nc = no_carry(one, h1, v(U32.add(x, y)), cc, Nat.add(v(x), v(y)), e, hf)
226 +e0 = L.subst(Bool, t => {Nat.add(v(U32.add(x, y)), C.shift(32n, WD.bo(t, one))) == Nat.add(v(x), v(y)) : Nat}, cc, False{}, nc, e)
227 Equal.trans(Nat, v(U32.add(x, y)), Nat.add(v(U32.add(x, y)), C.shift(32n, 0n)), Nat.add(v(x), v(y)), Equal.sym(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, 0n)), v(U32.add(x, y)), Equal.trans(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, 0n)), Nat.add(v(U32.add(x, y)), 0n), v(U32.add(x, y)), Equal.cong(Nat, Nat, t => Nat.add(v(U32.add(x, y)), t), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(U32.add(x, y))))), e0)
228
229def mul_le1(+b: Nat, +x: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {Nat.is_le(Nat.mul(b, x), x) == True{} : Bool}:
230 match b:
231 case 0n:
232 N.zero_le(x)
233 case 1n:
234 L.subst(Nat, z => {Nat.is_le(z, x) == True{} : Bool}, x, Nat.add(x, 0n), Equal.sym(Nat, Nat.add(x, 0n), x, N.add_zero(x)), N.le_refl(x))
235 case 2n+c:
236 Empty.absurd({Nat.is_le(Nat.mul(2n+c, x), x) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hb)))
237
238def half_g(+l: U32, +h: U32, +c: U32) -> WU.U64:
239 WU.U64{U32.add(U32.shr(l), U32.mul(U32.and(h, 1), c)), U32.shr(h)}
240
241def halfval(+one: Nat, +h1: {one == 1n : Nat}, +l: U32, +h: U32, +c: U32, +pc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {SW.value(half_g(l, h, c)) == Nat.div(val(l, h), 2n) : Nat}:
242 +b = U32.and(h, 1)
243 +s31 = C.shift(31n, one)
244 +bt = C.bit(v(h))
245 +evb = Equal.trans(Nat, v(b), Nat.mod(v(h), 2n), bt, LW.odd_val(h), Equal.sym(Nat, bt, Nat.mod(v(h), 2n), WW.bit_mod(v(h))))
246 +evc = Equal.trans(Nat, v(c), WD.sc(31n, one), s31, PD.pow32(31n, {==}, one, h1, c, pc), Equal.sym(Nat, s31, WD.sc(31n, one), W64M.shift_sc(31n, one)))
247 +hb1 = WW.bit_le1(v(h))
248 +epr = Equal.trans(Nat, Nat.mul(v(b), v(c)), Nat.mul(bt, v(c)), Nat.mul(bt, s31), Equal.cong(Nat, Nat, t => Nat.mul(t, v(c)), v(b), bt, evb), Equal.cong(Nat, Nat, t => Nat.mul(bt, t), v(c), s31, evc))
249 +hs1 = L.subst(Nat, z => {Nat.is_le(z, s31) == True{} : Bool}, one, 1n, h1, WW.shift_ge(31n, one))
250 +hsd = N.succ_le_lt(s31, Nat.double(s31), N.double_succ_le(s31, hs1))
251 +hple = L.subst(Nat, z => {Nat.is_le(z, s31) == True{} : Bool}, Nat.mul(bt, s31), Nat.mul(v(b), v(c)), Equal.sym(Nat, Nat.mul(v(b), v(c)), Nat.mul(bt, s31), epr), mul_le1(bt, s31, hb1))
252 +hplt = L.subst(Nat, z => {Nat.is_lt(Nat.mul(v(b), v(c)), z) == True{} : Bool}, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one), N.le_lt_trans(Nat.mul(v(b), v(c)), s31, Nat.double(s31), hple, hsd))
253 +m = U32.mul(b, c)
254 +evm = Equal.trans(Nat, v(m), Nat.mul(v(b), v(c)), Nat.mul(bt, s31), PD.mul32(one, h1, b, c, hplt), epr)
255 +hl = C.half(v(l))
256 +evs = Equal.trans(Nat, v(U32.shr(l)), Nat.div(v(l), 2n), hl, LW.ops_half(l), Equal.sym(Nat, hl, Nat.div(v(l), 2n), half_div(v(l))))
257 +hlt = Equal.trans(Bool, Nat.is_lt(hl, s31), Nat.is_lt(v(l), Nat.double(s31)), True{}, WW.lt_half(v(l), s31), WW.lt_one(32n, one, h1, v(l), vb(l)))
258 +hsum = N.lt_le_trans(Nat.add(hl, Nat.mul(bt, s31)), Nat.add(s31, Nat.mul(bt, s31)), Nat.double(s31), N.lt_add_r2(hl, s31, Nat.mul(bt, s31), hlt), L.subst(Nat, z => {Nat.is_le(Nat.add(s31, Nat.mul(bt, s31)), z) == True{} : Bool}, Nat.add(s31, s31), Nat.double(s31), Equal.sym(Nat, Nat.double(s31), Nat.add(s31, s31), NA.double_self(s31)), N.le_add_left(Nat.mul(bt, s31), s31, s31, mul_le1(bt, s31, hb1))))
259 +es = Equal.trans(Nat, Nat.add(v(U32.shr(l)), v(m)), Nat.add(hl, v(m)), Nat.add(hl, Nat.mul(bt, s31)), Equal.cong(Nat, Nat, t => Nat.add(t, v(m)), v(U32.shr(l)), hl, evs), Equal.cong(Nat, Nat, t => Nat.add(hl, t), v(m), Nat.mul(bt, s31), evm))
260 +hfit = WW.fits_one(32n, one, h1, Nat.add(v(U32.shr(l)), v(m)), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, Nat.add(hl, Nat.mul(bt, s31)), Nat.add(v(U32.shr(l)), v(m)), Equal.sym(Nat, Nat.add(v(U32.shr(l)), v(m)), Nat.add(hl, Nat.mul(bt, s31)), es), hsum))
261 +elo = Equal.trans(Nat, v(U32.add(U32.shr(l), m)), Nat.add(v(U32.shr(l)), v(m)), Nat.add(hl, Nat.mul(bt, s31)), add_exact(one, h1, U32.shr(l), m, hfit), es)
262 +ehi = Equal.trans(Nat, v(U32.shr(h)), Nat.div(v(h), 2n), C.half(v(h)), LW.ops_half(h), Equal.sym(Nat, C.half(v(h)), Nat.div(v(h), 2n), half_div(v(h))))
263 +ev = Equal.trans(Nat, Nat.add(v(U32.add(U32.shr(l), m)), C.shift(32n, v(U32.shr(h)))), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, v(U32.shr(h)))), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, C.half(v(h)))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, v(U32.shr(h)))), v(U32.add(U32.shr(l), m)), Nat.add(hl, Nat.mul(bt, s31)), elo), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, t)), v(U32.shr(h)), C.half(v(h)), ehi))
264 +eh = WW.half_limbs(31n, one, h1, v(l), v(h))
265 Equal.trans(Nat, Nat.add(v(U32.add(U32.shr(l), m)), C.shift(32n, v(U32.shr(h)))), C.half(val(l, h)), Nat.div(val(l, h), 2n), Equal.trans(Nat, Nat.add(v(U32.add(U32.shr(l), m)), C.shift(32n, v(U32.shr(h)))), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, C.half(v(h)))), C.half(val(l, h)), ev, Equal.sym(Nat, C.half(val(l, h)), Nat.add(Nat.add(hl, Nat.mul(bt, s31)), C.shift(32n, C.half(v(h)))), eh)), half_div(val(l, h)))
266
267def half_value(+a: WU.U64) -> SW.Half.value(a):
268 match a:
269 case WU.U64{+l, +h}:
270 halfval(1n, {==}, l, h, 2147483648, {==})
271
272
273
274
275def borrow_eq(+one: Nat, +h1: {one == 1n : Nat}, +vx: Nat, +vs: Nat, +vy: Nat, +cc: Bool, +e: {Nat.add(vx, C.shift(32n, WD.bo(cc, one))) == Nat.add(vs, vy) : Nat}, +hs: {C.fits(32n, vs) == True{} : Bool}) -> {cc == Nat.is_lt(vx, vy) : Bool}:
276 match cc:
277 case True{}:
278 +h1s = WW.lt_one(32n, one, h1, vs, hs)
279 +h2 = L.subst(Nat, z => {Nat.is_lt(Nat.add(vs, vy), z) == True{} : Bool}, Nat.add(C.shift(32n, one), vy), Nat.add(vy, C.shift(32n, one)), N.add_comm(C.shift(32n, one), vy), N.lt_add_r2(vs, C.shift(32n, one), vy, h1s))
280 +h3 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(vy, C.shift(32n, one))) == True{} : Bool}, Nat.add(vs, vy), Nat.add(vx, C.shift(32n, one)), Equal.sym(Nat, Nat.add(vx, C.shift(32n, one)), Nat.add(vs, vy), e), h2)
281 Equal.sym(Bool, Nat.is_lt(vx, vy), True{}, Equal.trans(Bool, Nat.is_lt(vx, vy), Nat.is_lt(Nat.add(vx, C.shift(32n, one)), Nat.add(vy, C.shift(32n, one))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(vx, C.shift(32n, one)), Nat.add(vy, C.shift(32n, one))), Nat.is_lt(vx, vy), WW.lt_cancel_r(vx, vy, C.shift(32n, one))), h3))
282 case False{}:
283 +e0 = Equal.trans(Nat, vx, Nat.add(vx, C.shift(32n, 0n)), Nat.add(vs, vy), Equal.sym(Nat, Nat.add(vx, C.shift(32n, 0n)), vx, Equal.trans(Nat, Nat.add(vx, C.shift(32n, 0n)), Nat.add(vx, 0n), vx, Equal.cong(Nat, Nat, t => Nat.add(vx, t), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(vx))), e)
284 +hle = L.subst(Nat, z => {Nat.is_le(vy, z) == True{} : Bool}, Nat.add(vy, vs), vx, Equal.trans(Nat, Nat.add(vy, vs), Nat.add(vs, vy), vx, N.add_comm(vy, vs), Equal.sym(Nat, vx, Nat.add(vs, vy), e0)), N.le_add_right(vy, vs))
285 Equal.sym(Bool, Nat.is_lt(vx, vy), False{}, N.le_not_lt(vx, vy, hle))
286
287def sub_cons(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32) -> {Nat.add(v(U32.sub(x, y)), v(y)) == Nat.add(v(x), C.shift(32n, WD.bo(U32.is_lt(x, y), one))) : Nat}:
288 +d = U32.sub(x, y)
289 +cc = P64.carry32(d, y)
290 +e0 = acons_o(one, h1, d, y)
291 +e1 = L.subst(U32, z => {Nat.add(v(z), C.shift(32n, WD.bo(cc, one))) == Nat.add(v(d), v(y)) : Nat}, U32.add(d, y), x, A.sub_add(x, y), e0)
292 +ec = Equal.trans(Bool, cc, Nat.is_lt(v(x), v(y)), U32.is_lt(x, y), borrow_eq(one, h1, v(x), v(d), v(y), cc, e1, vb(d)), Equal.sym(Bool, U32.is_lt(x, y), Nat.is_lt(v(x), v(y)), U3.is_lt_nat(x, y)))
293 +e2 = L.subst(Bool, t => {Nat.add(v(x), C.shift(32n, WD.bo(t, one))) == Nat.add(v(d), v(y)) : Nat}, cc, U32.is_lt(x, y), ec, e1)
294 Equal.sym(Nat, Nat.add(v(x), C.shift(32n, WD.bo(U32.is_lt(x, y), one))), Nat.add(v(d), v(y)), e2)
295
296def sub_alg(+lo: Nat, +hi: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +s: Nat, +b1: Nat, +b2: Nat, +b3: Nat, +e1: {Nat.add(lo, bl) == Nat.add(al, C.shift(32n, b1)) : Nat}, +e2: {Nat.add(s, bh) == Nat.add(ah, C.shift(32n, b2)) : Nat}, +e3: {Nat.add(hi, b1) == Nat.add(s, C.shift(32n, b3)) : Nat}) -> {Nat.add(Nat.add(lo, C.shift(32n, hi)), Nat.add(bl, C.shift(32n, bh))) == Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))) : Nat}:
297 Equal.trans(Nat, Nat.add(Nat.add(lo, C.shift(32n, hi)), Nat.add(bl, C.shift(32n, bh))), Nat.add(Nat.add(lo, bl), Nat.add(C.shift(32n, hi), C.shift(32n, bh))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), W64M.add4(lo, C.shift(32n, hi), bl, C.shift(32n, bh)), Equal.trans(Nat, Nat.add(Nat.add(lo, bl), Nat.add(C.shift(32n, hi), C.shift(32n, bh))), Nat.add(Nat.add(lo, bl), C.shift(32n, Nat.add(hi, bh))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(Nat.add(lo, bl), t), Nat.add(C.shift(32n, hi), C.shift(32n, bh)), C.shift(32n, Nat.add(hi, bh)), Equal.sym(Nat, C.shift(32n, Nat.add(hi, bh)), Nat.add(C.shift(32n, hi), C.shift(32n, bh)), WW.shift_add(32n, hi, bh))), Equal.trans(Nat, Nat.add(Nat.add(lo, bl), C.shift(32n, Nat.add(hi, bh))), Nat.add(Nat.add(al, C.shift(32n, b1)), C.shift(32n, Nat.add(hi, bh))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, Nat.add(hi, bh))), Nat.add(lo, bl), Nat.add(al, C.shift(32n, b1)), e1), Equal.trans(Nat, Nat.add(Nat.add(al, C.shift(32n, b1)), C.shift(32n, Nat.add(hi, bh))), Nat.add(al, Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh)))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), NA.add_assoc(al, C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh))), Equal.trans(Nat, Nat.add(al, Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh)))), Nat.add(al, C.shift(32n, Nat.add(b1, Nat.add(hi, bh)))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(al, t), Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh))), C.shift(32n, Nat.add(b1, Nat.add(hi, bh))), Equal.sym(Nat, C.shift(32n, Nat.add(b1, Nat.add(hi, bh))), Nat.add(C.shift(32n, b1), C.shift(32n, Nat.add(hi, bh))), WW.shift_add(32n, b1, Nat.add(hi, bh)))), Equal.trans(Nat, Nat.add(al, C.shift(32n, Nat.add(b1, Nat.add(hi, bh)))), Nat.add(al, C.shift(32n, Nat.add(ah, C.shift(32n, Nat.add(b2, b3))))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(al, C.shift(32n, t)), Nat.add(b1, Nat.add(hi, bh)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.trans(Nat, Nat.add(b1, Nat.add(hi, bh)), Nat.add(hi, Nat.add(b1, bh)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), NA.add_swap(b1, hi, bh), Equal.trans(Nat, Nat.add(hi, Nat.add(b1, bh)), Nat.add(Nat.add(hi, b1), bh), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.sym(Nat, Nat.add(Nat.add(hi, b1), bh), Nat.add(hi, Nat.add(b1, bh)), NA.add_assoc(hi, b1, bh)), Equal.trans(Nat, Nat.add(Nat.add(hi, b1), bh), Nat.add(Nat.add(s, C.shift(32n, b3)), bh), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.cong(Nat, Nat, t => Nat.add(t, bh), Nat.add(hi, b1), Nat.add(s, C.shift(32n, b3)), e3), Equal.trans(Nat, Nat.add(Nat.add(s, C.shift(32n, b3)), bh), Nat.add(s, Nat.add(C.shift(32n, b3), bh)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), NA.add_assoc(s, C.shift(32n, b3), bh), Equal.trans(Nat, Nat.add(s, Nat.add(C.shift(32n, b3), bh)), Nat.add(s, Nat.add(bh, C.shift(32n, b3))), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.cong(Nat, Nat, t => Nat.add(s, t), Nat.add(C.shift(32n, b3), bh), Nat.add(bh, C.shift(32n, b3)), N.add_comm(C.shift(32n, b3), bh)), Equal.trans(Nat, Nat.add(s, Nat.add(bh, C.shift(32n, b3))), Nat.add(Nat.add(s, bh), C.shift(32n, b3)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.sym(Nat, Nat.add(Nat.add(s, bh), C.shift(32n, b3)), Nat.add(s, Nat.add(bh, C.shift(32n, b3))), NA.add_assoc(s, bh, C.shift(32n, b3))), Equal.trans(Nat, Nat.add(Nat.add(s, bh), C.shift(32n, b3)), Nat.add(Nat.add(ah, C.shift(32n, b2)), C.shift(32n, b3)), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(32n, b3)), Nat.add(s, bh), Nat.add(ah, C.shift(32n, b2)), e2), Equal.trans(Nat, Nat.add(Nat.add(ah, C.shift(32n, b2)), C.shift(32n, b3)), Nat.add(ah, Nat.add(C.shift(32n, b2), C.shift(32n, b3))), Nat.add(ah, C.shift(32n, Nat.add(b2, b3))), NA.add_assoc(ah, C.shift(32n, b2), C.shift(32n, b3)), Equal.cong(Nat, Nat, t => Nat.add(ah, t), Nat.add(C.shift(32n, b2), C.shift(32n, b3)), C.shift(32n, Nat.add(b2, b3)), Equal.sym(Nat, C.shift(32n, Nat.add(b2, b3)), Nat.add(C.shift(32n, b2), C.shift(32n, b3)), WW.shift_add(32n, b2, b3)))))))))))), Equal.trans(Nat, Nat.add(al, C.shift(32n, Nat.add(ah, C.shift(32n, Nat.add(b2, b3))))), Nat.add(al, Nat.add(C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3))))), Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Equal.cong(Nat, Nat, t => Nat.add(al, t), C.shift(32n, Nat.add(ah, C.shift(32n, Nat.add(b2, b3)))), Nat.add(C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), WW.shift_add(32n, ah, C.shift(32n, Nat.add(b2, b3)))), Equal.sym(Nat, Nat.add(Nat.add(al, C.shift(32n, ah)), C.shift(32n, C.shift(32n, Nat.add(b2, b3)))), Nat.add(al, Nat.add(C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3))))), NA.add_assoc(al, C.shift(32n, ah), C.shift(32n, C.shift(32n, Nat.add(b2, b3))))))))))))
298
299def sub_fin(+vs: Nat, +d: Nat, +q: Nat, +e: {vs == Nat.add(d, C.shift(64n, q)) : Nat}, +hf: {C.fits(64n, vs) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(q, 0n) == c : Bool}) -> {vs == d : Nat}:
300 match c:
301 case True{}:
302 +eq = N.eq_from_is_eq(q, 0n, hc)
303 Equal.trans(Nat, vs, Nat.add(d, C.shift(64n, q)), d, e, Equal.trans(Nat, Nat.add(d, C.shift(64n, q)), Nat.add(d, 0n), d, Equal.cong(Nat, Nat, t => Nat.add(d, t), C.shift(64n, q), 0n, Equal.trans(Nat, C.shift(64n, q), C.shift(64n, 0n), 0n, Equal.cong(Nat, Nat, t => C.shift(64n, t), q, 0n, eq), WW.shift_zero(64n))), N.add_zero(d)))
304 case False{}:
305 Empty.absurd({vs == d : Nat}, true_ne_false(Equal.trans(Bool, True{}, C.fits(64n, vs), False{}, Equal.sym(Bool, C.fits(64n, vs), True{}, hf), Equal.trans(Bool, C.fits(64n, vs), C.fits(64n, Nat.add(d, C.shift(64n, q))), False{}, Equal.cong(Nat, Bool, t => C.fits(64n, t), vs, Nat.add(d, C.shift(64n, q)), e), WW.unfit_nz(64n, d, q, hc)))))
306
307def subval(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +hle: {Nat.is_le(val(bl, bh), val(al, ah)) == True{} : Bool}) -> {SW.value(X.sub(WU.U64{al, ah}, WU.U64{bl, bh})) == Nat.sub(val(al, ah), val(bl, bh)) : Nat}:
308 +lo = U32.sub(al, bl)
309 +c1 = U32.is_lt(al, bl)
310 +s = U32.sub(ah, bh)
311 +cb = X.b32(c1)
312 +hi = U32.sub(s, cb)
313 +b1 = WD.bo(c1, one)
314 +b2 = WD.bo(U32.is_lt(ah, bh), one)
315 +b3 = WD.bo(U32.is_lt(s, cb), one)
316 +ecb = Equal.trans(Nat, v(cb), S.bit_value(c1), b1, W64M.b32_v(c1), Equal.sym(Nat, b1, S.bit_value(c1), WD.bo_bit(c1, one, h1)))
317 +e3 = Equal.trans(Nat, Nat.add(v(hi), b1), Nat.add(v(hi), v(cb)), Nat.add(v(s), C.shift(32n, b3)), Equal.cong(Nat, Nat, t => Nat.add(v(hi), t), b1, v(cb), Equal.sym(Nat, v(cb), b1, ecb)), sub_cons(one, h1, s, cb))
318 +eq = sub_alg(v(lo), v(hi), v(al), v(ah), v(bl), v(bh), v(s), b1, b2, b3, sub_cons(one, h1, al, bl), sub_cons(one, h1, ah, bh), e3)
319 +q = Nat.add(b2, b3)
320 +va = val(al, ah)
321 +vbb = val(bl, bh)
322 +vs = val(lo, hi)
323 +T = C.shift(64n, q)
324 +eq2 = Equal.trans(Nat, Nat.add(vs, vbb), Nat.add(va, C.shift(32n, C.shift(32n, q))), Nat.add(va, T), eq, Equal.cong(Nat, Nat, t => Nat.add(va, t), C.shift(32n, C.shift(32n, q)), T, Equal.sym(Nat, T, C.shift(32n, C.shift(32n, q)), WW.shift_comp(32n, 32n, q))))
325 +dd = Nat.sub(va, vbb)
326 +ea = Equal.sym(Nat, Nat.add(vbb, dd), va, N.sub_add(va, vbb, hle))
327 +e4 = Equal.trans(Nat, Nat.add(vbb, vs), Nat.add(vs, vbb), Nat.add(vbb, Nat.add(dd, T)), N.add_comm(vbb, vs), Equal.trans(Nat, Nat.add(vs, vbb), Nat.add(va, T), Nat.add(vbb, Nat.add(dd, T)), eq2, Equal.trans(Nat, Nat.add(va, T), Nat.add(Nat.add(vbb, dd), T), Nat.add(vbb, Nat.add(dd, T)), Equal.cong(Nat, Nat, t => Nat.add(t, T), va, Nat.add(vbb, dd), ea), NA.add_assoc(vbb, dd, T))))
328 +e5 = NR.add_cancel(vbb, vs, Nat.add(dd, T), e4)
329 +hf = WW.limbs_fit(32n, 32n, v(lo), v(hi), vb(lo), vb(hi))
330 sub_fin(vs, dd, q, e5, hf, Nat.is_eq(q, 0n), {==})
331
332def sub_value(+a: WU.U64, +b: WU.U64, +h: {Nat.is_le(SW.value(b), SW.value(a)) == True{} : Bool}) -> SW.Sub.value(a, b, h):
333 match a b:
334 case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
335 subval(1n, {==}, al, ah, bl, bh, h)
336
337
338
339def mcons(+x: U32, +y: U32) -> {Nat.add(v(U32.mul(x, y)), C.shift(32n, W64M.mex(x, y))) == Nat.mul(v(x), v(y)) : Nat}:
340 Equal.trans(Nat, Nat.add(v(U32.mul(x, y)), C.shift(32n, W64M.mex(x, y))), Nat.add(v(U32.mul(x, y)), WD.sc(32n, W64M.mex(x, y))), Nat.mul(v(x), v(y)), Equal.cong(Nat, Nat, z => Nat.add(v(U32.mul(x, y)), z), C.shift(32n, W64M.mex(x, y)), WD.sc(32n, W64M.mex(x, y)), W64M.shift_sc(32n, W64M.mex(x, y))), W64M.mul_cons(x, y))
341
342
343def cross_eq(+al: U32, +ah: U32, +bl: U32, +bh: U32) -> {Nat.add(v(U32.add(U32.mul(al, bh), U32.mul(ah, bl))), C.shift(32n, Nat.add(bv(P64.carry32(U32.mul(al, bh), U32.mul(ah, bl))), Nat.add(W64M.mex(al, bh), W64M.mex(ah, bl))))) == Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))) : Nat}:
344 +m1 = U32.mul(al, bh)
345 +m2 = U32.mul(ah, bl)
346 +t = U32.add(m1, m2)
347 +c = P64.carry32(m1, m2)
348 +x1 = W64M.mex(al, bh)
349 +x2 = W64M.mex(ah, bl)
350 +e1 = mcons(al, bh)
351 +e2 = mcons(ah, bl)
352 +et = acons(m1, m2)
353 Equal.sym(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.add(v(m2), C.shift(32n, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.trans(Nat, Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))), Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.mul(v(ah), v(bl))), Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.add(v(m2), C.shift(32n, x2))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mul(v(ah), v(bl))), Nat.mul(v(al), v(bh)), Nat.add(v(m1), C.shift(32n, x1)), Equal.sym(Nat, Nat.add(v(m1), C.shift(32n, x1)), Nat.mul(v(al), v(bh)), e1)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(m1), C.shift(32n, x1)), z), Nat.mul(v(ah), v(bl)), Nat.add(v(m2), C.shift(32n, x2)), Equal.sym(Nat, Nat.add(v(m2), C.shift(32n, x2)), Nat.mul(v(ah), v(bl)), e2))), Equal.trans(Nat, Nat.add(Nat.add(v(m1), C.shift(32n, x1)), Nat.add(v(m2), C.shift(32n, x2))), Nat.add(Nat.add(v(m1), v(m2)), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), W64M.add4(v(m1), C.shift(32n, x1), v(m2), C.shift(32n, x2)), Equal.trans(Nat, Nat.add(Nat.add(v(m1), v(m2)), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(v(m1), v(m2)), Nat.add(v(t), C.shift(32n, bv(c))), Equal.sym(Nat, Nat.add(v(t), C.shift(32n, bv(c))), Nat.add(v(m1), v(m2)), et)), Equal.trans(Nat, Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), Nat.add(C.shift(32n, x1), C.shift(32n, x2))), Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), C.shift(32n, Nat.add(x1, x2))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), z), Nat.add(C.shift(32n, x1), C.shift(32n, x2)), C.shift(32n, Nat.add(x1, x2)), Equal.sym(Nat, C.shift(32n, Nat.add(x1, x2)), Nat.add(C.shift(32n, x1), C.shift(32n, x2)), WW.shift_add(32n, x1, x2))), Equal.trans(Nat, Nat.add(Nat.add(v(t), C.shift(32n, bv(c))), C.shift(32n, Nat.add(x1, x2))), Nat.add(v(t), Nat.add(C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2)))), Nat.add(v(t), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2)))), NA.add_assoc(v(t), C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2))), Equal.cong(Nat, Nat, z => Nat.add(v(t), z), Nat.add(C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2))), C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2))), Equal.sym(Nat, C.shift(32n, Nat.add(bv(c), Nat.add(x1, x2))), Nat.add(C.shift(32n, bv(c)), C.shift(32n, Nat.add(x1, x2))), WW.shift_add(32n, bv(c), Nat.add(x1, x2))))))))))
354
355def mul_value(+a: WU.U64, +b: WU.U64) -> SW.Mul.value(a, b):
356 match a b:
357 case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
358 +m1 = U32.mul(al, bh)
359 +m2 = U32.mul(ah, bl)
360 +t = U32.add(m1, m2)
361 +kc = Nat.add(bv(P64.carry32(m1, m2)), Nat.add(W64M.mex(al, bh), W64M.mex(ah, bl)))
362 +A = Nat.mul(v(al), v(bl))
363 +H = Nat.mul(v(ah), v(bh))
364 +mk = WW.mul_k(32n, v(al), v(ah), v(bl), v(bh), v(t), kc, cross_eq(al, ah, bl, bh))
365 +Y = Nat.add(kc, H)
366 +p = X.mul32(al, bl)
367 +q = {WU.U64{0, t} : WU.U64}
368 av = add_value(p, q)
369 +elp = Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(z, C.shift(32n, v(t)))), SW.value(p), A, W64M.mul32_value(al, bl))
370 +em = Equal.trans(Nat, Nat.mul(val(al, ah), val(bl, bh)), Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(32n, C.shift(32n, Y))), Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(64n, Y)), mk, Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(32n, v(t))), z), C.shift(32n, C.shift(32n, Y)), C.shift(64n, Y), Equal.sym(Nat, C.shift(64n, Y), C.shift(32n, C.shift(32n, Y)), WW.shift_comp(32n, 32n, Y))))
371 +elm = Equal.trans(Nat, C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), C.low(64n, Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(64n, Y))), C.low(64n, Nat.add(A, C.shift(32n, v(t)))), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.mul(val(al, ah), val(bl, bh)), Nat.add(Nat.add(A, C.shift(32n, v(t))), C.shift(64n, Y)), em), WW.low_add_shift(64n, Nat.add(A, C.shift(32n, v(t))), Y))
372 Equal.trans(Nat, SW.value(X.add(p, q)), C.low(64n, Nat.add(SW.value(p), C.shift(32n, v(t)))), C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), av, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(p), C.shift(32n, v(t)))), C.low(64n, Nat.add(A, C.shift(32n, v(t)))), C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), elp, Equal.sym(Nat, C.low(64n, Nat.mul(val(al, ah), val(bl, bh))), C.low(64n, Nat.add(A, C.shift(32n, v(t)))), elm)))
373
374
375
376def mo_alg(+k: Nat, +A: Nat, +t1: Nat, +t2: Nat, +hh: Nat, +pl: Nat, +ph: Nat, +cl: Nat, +ch: Nat, +s: Nat, +cr: Nat, +ea: {A == Nat.add(pl, C.shift(k, ph)) : Nat}, +ec: {Nat.add(t2, t1) == Nat.add(cl, C.shift(k, ch)) : Nat}, +es: {Nat.add(s, C.shift(k, cr)) == Nat.add(ph, cl) : Nat}, +eh: {hh == 0n : Nat}) -> {Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, hh)))) == Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))) : Nat}:
377 Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, hh)))), Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, 0n)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, z)))), hh, 0n, eh), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), C.shift(k, C.shift(k, 0n)))), Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), 0n)), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), z)), C.shift(k, C.shift(k, 0n)), 0n, Equal.trans(Nat, C.shift(k, C.shift(k, 0n)), C.shift(k, 0n), 0n, Equal.cong(Nat, Nat, z => C.shift(k, z), C.shift(k, 0n), 0n, WW.shift_zero(k)), WW.shift_zero(k))), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), Nat.add(C.shift(k, t2), 0n)), Nat.add(Nat.add(A, C.shift(k, t1)), C.shift(k, t2)), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(A, C.shift(k, t1)), z), Nat.add(C.shift(k, t2), 0n), C.shift(k, t2), N.add_zero(C.shift(k, t2))), Equal.trans(Nat, Nat.add(Nat.add(A, C.shift(k, t1)), C.shift(k, t2)), Nat.add(A, Nat.add(C.shift(k, t1), C.shift(k, t2))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), NA.add_assoc(A, C.shift(k, t1), C.shift(k, t2)), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(k, t1), C.shift(k, t2))), Nat.add(A, Nat.add(C.shift(k, t2), C.shift(k, t1))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(C.shift(k, t1), C.shift(k, t2)), Nat.add(C.shift(k, t2), C.shift(k, t1)), N.add_comm(C.shift(k, t1), C.shift(k, t2))), Equal.trans(Nat, Nat.add(A, Nat.add(C.shift(k, t2), C.shift(k, t1))), Nat.add(A, C.shift(k, Nat.add(t2, t1))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(C.shift(k, t2), C.shift(k, t1)), C.shift(k, Nat.add(t2, t1)), Equal.sym(Nat, C.shift(k, Nat.add(t2, t1)), Nat.add(C.shift(k, t2), C.shift(k, t1)), WW.shift_add(k, t2, t1))), Equal.trans(Nat, Nat.add(A, C.shift(k, Nat.add(t2, t1))), Nat.add(A, C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(A, C.shift(k, z)), Nat.add(t2, t1), Nat.add(cl, C.shift(k, ch)), ec), Equal.trans(Nat, Nat.add(A, C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, ph)), C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, Nat.add(cl, C.shift(k, ch)))), A, Nat.add(pl, C.shift(k, ph)), ea), Equal.trans(Nat, Nat.add(Nat.add(pl, C.shift(k, ph)), C.shift(k, Nat.add(cl, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, ph)), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(pl, C.shift(k, ph)), z), C.shift(k, Nat.add(cl, C.shift(k, ch))), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch))), WW.shift_add(k, cl, C.shift(k, ch))), Equal.trans(Nat, Nat.add(Nat.add(pl, C.shift(k, ph)), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), NA.add_assoc(pl, C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch))))), Nat.add(pl, Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, z), Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch))), Equal.sym(Nat, Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch))), Nat.add(C.shift(k, ph), Nat.add(C.shift(k, cl), C.shift(k, C.shift(k, ch)))), NA.add_assoc(C.shift(k, ph), C.shift(k, cl), C.shift(k, C.shift(k, ch))))), Equal.trans(Nat, Nat.add(pl, Nat.add(Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, Nat.add(ph, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(z, C.shift(k, C.shift(k, ch)))), Nat.add(C.shift(k, ph), C.shift(k, cl)), C.shift(k, Nat.add(ph, cl)), Equal.sym(Nat, C.shift(k, Nat.add(ph, cl)), Nat.add(C.shift(k, ph), C.shift(k, cl)), WW.shift_add(k, ph, cl))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, Nat.add(ph, cl)), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, Nat.add(s, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(C.shift(k, z), C.shift(k, C.shift(k, ch)))), Nat.add(ph, cl), Nat.add(s, C.shift(k, cr)), Equal.sym(Nat, Nat.add(s, C.shift(k, cr)), Nat.add(ph, cl), es)), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, Nat.add(s, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(z, C.shift(k, C.shift(k, ch)))), C.shift(k, Nat.add(s, C.shift(k, cr))), Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), WW.shift_add(k, s, C.shift(k, cr))), Equal.trans(Nat, Nat.add(pl, Nat.add(Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), C.shift(k, C.shift(k, ch)))), Nat.add(pl, Nat.add(C.shift(k, s), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, z), Nat.add(Nat.add(C.shift(k, s), C.shift(k, C.shift(k, cr))), C.shift(k, C.shift(k, ch))), Nat.add(C.shift(k, s), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch)))), NA.add_assoc(C.shift(k, s), C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch)))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, s), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))))), Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(C.shift(k, s), z)), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))), C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))), Equal.sym(Nat, C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))), Nat.add(C.shift(k, C.shift(k, cr)), C.shift(k, C.shift(k, ch))), WW.shift_add(k, C.shift(k, cr), C.shift(k, ch)))), Equal.trans(Nat, Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, Nat.add(C.shift(k, cr), C.shift(k, ch))))), Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, C.shift(k, Nat.add(cr, ch))))), Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Equal.cong(Nat, Nat, z => Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, z))), Nat.add(C.shift(k, cr), C.shift(k, ch)), C.shift(k, Nat.add(cr, ch)), Equal.sym(Nat, C.shift(k, Nat.add(cr, ch)), Nat.add(C.shift(k, cr), C.shift(k, ch)), WW.shift_add(k, cr, ch))), Equal.sym(Nat, Nat.add(Nat.add(pl, C.shift(k, s)), C.shift(k, C.shift(k, Nat.add(cr, ch)))), Nat.add(pl, Nat.add(C.shift(k, s), C.shift(k, C.shift(k, Nat.add(cr, ch))))), NA.add_assoc(pl, C.shift(k, s), C.shift(k, C.shift(k, Nat.add(cr, ch))))))))))))))))))))))
378
379def val_eta(+p: WU.U64) -> {SW.value(p) == Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) : Nat}:
380 match p:
381 case WU.U64{+l, +h}:
382 {==}
383
384def prod_fits(+k: Nat, +x: Nat, +y: Nat, +hx: {C.fits(k, x) == True{} : Bool}, +hy: {C.fits(k, y) == True{} : Bool}) -> {C.fits(Nat.add(k, k), Nat.mul(x, y)) == True{} : Bool}:
385 +h = W64M.mul_lt_sq(x, y, C.pow2(k), WW.lt_of_fits(k, x, hx), WW.lt_of_fits(k, y, hy))
386 WW.fits_of_lt(Nat.add(k, k), Nat.mul(x, y), L.subst(Nat, z => {Nat.is_lt(Nat.mul(x, y), z) == True{} : Bool}, Nat.mul(C.pow2(k), C.pow2(k)), C.pow2(Nat.add(k, k)), WW.pow2_sq(k), h))
387
388def le_hi(+k: Nat, +x: Nat, +y: Nat, +hy: {Nat.is_le(1n, y) == True{} : Bool}) -> {Nat.is_le(C.pow2(k), Nat.add(x, C.shift(k, y))) == True{} : Bool}:
389 +h1 = L.subst(Nat, z => {Nat.is_le(z, C.shift(k, y)) == True{} : Bool}, C.shift(k, 1n), C.pow2(k), WW.shift_one(k), WW.shift_mono(k, 1n, y, hy))
390 N.le_trans(C.pow2(k), C.shift(k, y), Nat.add(x, C.shift(k, y)), h1, L.subst(Nat, z => {Nat.is_le(C.shift(k, y), z) == True{} : Bool}, Nat.add(C.shift(k, y), x), Nat.add(x, C.shift(k, y)), N.add_comm(C.shift(k, y), x), N.le_add_right(C.shift(k, y), x)))
391
392def both_hi(+k: Nat, +x1: Nat, +y1: Nat, +x2: Nat, +y2: Nat, +hy1: {Nat.is_le(1n, y1) == True{} : Bool}, +hy2: {Nat.is_le(1n, y2) == True{} : Bool}) -> {C.fits(Nat.add(k, k), Nat.mul(Nat.add(x1, C.shift(k, y1)), Nat.add(x2, C.shift(k, y2)))) == False{} : Bool}:
393 +a = Nat.add(x1, C.shift(k, y1))
394 +b = Nat.add(x2, C.shift(k, y2))
395 +P = C.pow2(k)
396 +h1 = N.le_trans(Nat.mul(P, P), Nat.mul(a, P), Nat.mul(a, b), AR2.mul_le(P, a, P, le_hi(k, x1, y1, hy1)), W64M.le_mul_r(a, P, b, le_hi(k, x2, y2, hy2)))
397 +h2 = L.subst(Nat, z => {Nat.is_le(z, Nat.mul(a, b)) == True{} : Bool}, Nat.mul(P, P), C.pow2(Nat.add(k, k)), WW.pow2_sq(k), h1)
398 Equal.trans(Bool, C.fits(Nat.add(k, k), Nat.mul(a, b)), Nat.is_lt(Nat.mul(a, b), C.pow2(Nat.add(k, k))), False{}, WW.fits_lt(Nat.add(k, k), Nat.mul(a, b)), N.le_not_lt(Nat.mul(a, b), C.pow2(Nat.add(k, k)), h2))
399
400def pos_ne(+n: Nat, +h: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
401 match n:
402 case 0n:
403 Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, true_ne_false(h))
404 case 1n+m:
405 N.zero_le(m)
406
407def or_cr(+x: Nat, +c: Bool) -> {Bool.or(Bool.not(Nat.is_eq(x, 0n)), c) == Bool.not(Nat.is_eq(Nat.add(bv(c), x), 0n)) : Bool}:
408 match x c:
409 case 0n True{}:
410 {==}
411 case 1n+y True{}:
412 {==}
413 case 0n False{}:
414 {==}
415 case 1n+y False{}:
416 {==}
417
418
419def mo_core(+al: U32, +ah: U32, +bl: U32, +bh: U32, +eh: {Nat.mul(v(ah), v(bh)) == 0n : Nat}, +hT: {C.fits(64n, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), v(bh)))) == True{} : Bool}) -> {X.mul_over_one(X.mul32(al, bl), X.add(X.mul32(ah, bl), X.mul32(al, bh))) == Bool.not(C.fits(64n, Nat.mul(val(al, ah), val(bl, bh)))) : Bool}:
420 +p = X.mul32(al, bl)
421 +c = X.add(X.mul32(ah, bl), X.mul32(al, bh))
422 +pl = X.lo(p)
423 +ph = X.hi(p)
424 +cl = X.lo(c)
425 +ch = X.hi(c)
426 +s = U32.add(ph, cl)
427 +cr = P64.carry32(ph, cl)
428 +A = Nat.mul(v(al), v(bl))
429 +t1 = Nat.mul(v(al), v(bh))
430 +t2 = Nat.mul(v(ah), v(bl))
431 +ea = Equal.trans(Nat, A, SW.value(p), Nat.add(v(pl), C.shift(32n, v(ph))), Equal.sym(Nat, SW.value(p), A, W64M.mul32_value(al, bl)), val_eta(p))
432 av = add_value(X.mul32(ah, bl), X.mul32(al, bh))
433 +ecv = Equal.trans(Nat, SW.value(c), C.low(64n, Nat.add(SW.value(X.mul32(ah, bl)), SW.value(X.mul32(al, bh)))), Nat.add(t2, t1), av, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(X.mul32(ah, bl)), SW.value(X.mul32(al, bh)))), C.low(64n, Nat.add(t2, t1)), Nat.add(t2, t1), Equal.trans(Nat, C.low(64n, Nat.add(SW.value(X.mul32(ah, bl)), SW.value(X.mul32(al, bh)))), C.low(64n, Nat.add(t2, SW.value(X.mul32(al, bh)))), C.low(64n, Nat.add(t2, t1)), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(z, SW.value(X.mul32(al, bh)))), SW.value(X.mul32(ah, bl)), t2, W64M.mul32_value(ah, bl)), Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(t2, z)), SW.value(X.mul32(al, bh)), t1, W64M.mul32_value(al, bh))), WW.low_fit(64n, Nat.add(t2, t1), hT)))
434 +ec = Equal.trans(Nat, Nat.add(t2, t1), SW.value(c), Nat.add(v(cl), C.shift(32n, v(ch))), Equal.sym(Nat, SW.value(c), Nat.add(t2, t1), ecv), val_eta(c))
435 +es = acons(ph, cl)
436 +ealg = mo_alg(32n, A, t1, t2, Nat.mul(v(ah), v(bh)), v(pl), v(ph), v(cl), v(ch), v(s), bv(cr), ea, ec, es, eh)
437 +pr = Nat.mul(val(al, ah), val(bl, bh))
438 +q = Nat.add(bv(cr), v(ch))
439 +R = Nat.add(v(pl), C.shift(32n, v(s)))
440 +e1 = Equal.trans(Nat, pr, Nat.add(Nat.add(Nat.mul(v(al), v(bl)), C.shift(32n, Nat.mul(v(al), v(bh)))), Nat.add(C.shift(32n, Nat.mul(v(ah), v(bl))), C.shift(32n, C.shift(32n, Nat.mul(v(ah), v(bh)))))), Nat.add(R, C.shift(64n, q)), WW.expand_k(32n, v(al), v(ah), v(bl), v(bh)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(v(al), v(bl)), C.shift(32n, Nat.mul(v(al), v(bh)))), Nat.add(C.shift(32n, Nat.mul(v(ah), v(bl))), C.shift(32n, C.shift(32n, Nat.mul(v(ah), v(bh)))))), Nat.add(R, C.shift(32n, C.shift(32n, q))), Nat.add(R, C.shift(64n, q)), ealg, Equal.cong(Nat, Nat, z => Nat.add(R, z), C.shift(32n, C.shift(32n, q)), C.shift(64n, q), Equal.sym(Nat, C.shift(64n, q), C.shift(32n, C.shift(32n, q)), WW.shift_comp(32n, 32n, q)))))
441 +eh2 = Equal.trans(Nat, C.high(64n, pr), C.high(64n, Nat.add(R, C.shift(64n, q))), q, Equal.cong(Nat, Nat, z => C.high(64n, z), pr, Nat.add(R, C.shift(64n, q)), e1), WW.high_u(64n, R, q, WW.limbs_fit(32n, 32n, v(pl), v(s), vb(pl), vb(s))))
442 +em1 = Equal.trans(Bool, Bool.or(Bool.not(U32.is_zero(ch)), U32.is_lt(s, ph)), Bool.or(Bool.not(Nat.is_eq(v(ch), 0n)), U32.is_lt(s, ph)), Bool.or(Bool.not(Nat.is_eq(v(ch), 0n)), cr), Equal.cong(Bool, Bool, z => Bool.or(Bool.not(z), U32.is_lt(s, ph)), U32.is_zero(ch), Nat.is_eq(v(ch), 0n), LW.zero_nat(ch)), Equal.cong(Bool, Bool, z => Bool.or(Bool.not(Nat.is_eq(v(ch), 0n)), z), U32.is_lt(s, ph), cr, P64.add_lt(ph, cl)))
443 Equal.trans(Bool, Bool.or(Bool.not(U32.is_zero(ch)), U32.is_lt(s, ph)), Bool.not(Nat.is_eq(q, 0n)), Bool.not(C.fits(64n, pr)), Equal.trans(Bool, Bool.or(Bool.not(U32.is_zero(ch)), U32.is_lt(s, ph)), Bool.or(Bool.not(Nat.is_eq(v(ch), 0n)), cr), Bool.not(Nat.is_eq(q, 0n)), em1, or_cr(v(ch), cr)), Equal.sym(Bool, Bool.not(C.fits(64n, pr)), Bool.not(Nat.is_eq(q, 0n)), Equal.cong(Nat, Bool, z => Bool.not(Nat.is_eq(z, 0n)), C.high(64n, pr), q, eh2)))
444
445def mo_top(+al: U32, +ah: U32, +bl: U32, +bh: U32, +z1: Bool, +z2: Bool, +hz1: {U32.is_zero(ah) == z1 : Bool}, +hz2: {U32.is_zero(bh) == z2 : Bool}) -> {Bool.or(Bool.and(Bool.not(z1), Bool.not(z2)), X.mul_over_one(X.mul32(al, bl), X.add(X.mul32(ah, bl), X.mul32(al, bh)))) == Bool.not(C.fits(64n, Nat.mul(val(al, ah), val(bl, bh)))) : Bool}:
446 match z1 z2:
447 case False{} False{}:
448 +h1 = pos_ne(v(ah), Equal.trans(Bool, Nat.is_eq(v(ah), 0n), U32.is_zero(ah), False{}, Equal.sym(Bool, U32.is_zero(ah), Nat.is_eq(v(ah), 0n), LW.zero_nat(ah)), hz1))
449 +h2 = pos_ne(v(bh), Equal.trans(Bool, Nat.is_eq(v(bh), 0n), U32.is_zero(bh), False{}, Equal.sym(Bool, U32.is_zero(bh), Nat.is_eq(v(bh), 0n), LW.zero_nat(bh)), hz2))
450 +hb = both_hi(32n, v(al), v(ah), v(bl), v(bh), h1, h2)
451 Equal.sym(Bool, Bool.not(C.fits(64n, Nat.mul(val(al, ah), val(bl, bh)))), True{}, Equal.cong(Bool, Bool, t => Bool.not(t), C.fits(64n, Nat.mul(val(al, ah), val(bl, bh))), False{}, hb))
452 case True{} _:
453 +eah = N.eq_from_is_eq(v(ah), 0n, Equal.trans(Bool, Nat.is_eq(v(ah), 0n), U32.is_zero(ah), True{}, Equal.sym(Bool, U32.is_zero(ah), Nat.is_eq(v(ah), 0n), LW.zero_nat(ah)), hz1))
454 +eh = L.subst(Nat, z => {Nat.mul(z, v(bh)) == 0n : Nat}, 0n, v(ah), Equal.sym(Nat, v(ah), 0n, eah), {==})
455 +hT = L.subst(Nat, z => {C.fits(64n, Nat.add(Nat.mul(z, v(bl)), Nat.mul(v(al), v(bh)))) == True{} : Bool}, 0n, v(ah), Equal.sym(Nat, v(ah), 0n, eah), prod_fits(32n, v(al), v(bh), vb(al), vb(bh)))
456 mo_core(al, ah, bl, bh, eh, hT)
457 case False{} True{}:
458 +ebh = N.eq_from_is_eq(v(bh), 0n, Equal.trans(Bool, Nat.is_eq(v(bh), 0n), U32.is_zero(bh), True{}, Equal.sym(Bool, U32.is_zero(bh), Nat.is_eq(v(bh), 0n), LW.zero_nat(bh)), hz2))
459 +eh = L.subst(Nat, z => {Nat.mul(v(ah), z) == 0n : Nat}, 0n, v(bh), Equal.sym(Nat, v(bh), 0n, ebh), NA.mul_zero(v(ah)))
460 +e0 = Equal.trans(Nat, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), 0n)), Nat.add(Nat.mul(v(ah), v(bl)), 0n), Nat.mul(v(ah), v(bl)), Equal.cong(Nat, Nat, t => Nat.add(Nat.mul(v(ah), v(bl)), t), Nat.mul(v(al), 0n), 0n, NA.mul_zero(v(al))), N.add_zero(Nat.mul(v(ah), v(bl))))
461 +hT0 = L.subst(Nat, z => {C.fits(64n, z) == True{} : Bool}, Nat.mul(v(ah), v(bl)), Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), 0n)), Equal.sym(Nat, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), 0n)), Nat.mul(v(ah), v(bl)), e0), prod_fits(32n, v(ah), v(bl), vb(ah), vb(bl)))
462 +hT = L.subst(Nat, z => {C.fits(64n, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), z))) == True{} : Bool}, 0n, v(bh), Equal.sym(Nat, v(bh), 0n, ebh), hT0)
463 mo_core(al, ah, bl, bh, eh, hT)
464
465def mul_over_value(+a: WU.U64, +b: WU.U64) -> SW.MulOver.value(a, b):
466 match a b:
467 case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
468 mo_top(al, ah, bl, bh, U32.is_zero(ah), U32.is_zero(bh), {==}, {==})