def add_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:55

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

55# the full sum: the two limbs of the wrapped sum plus 2^64 (c3 + c2)
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)))