def um.go

bend-osdev-u32@0.1.0.0 · PROOF.bend:1438

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as Laws

1438def um.go(+n: Nat, m: Nat, a: Word(m), +b: Word(n), +acc: Word(n)) -> {Nat.add(Word.to_nat(n, Word.mul.go(n, m, a, b, acc)), U.U32Nat.dbl(n, um.k(n, m, a, b, acc))) == Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(m, a), Word.to_nat(n, b))) : Nat}:
1439  match m:
1440    case 0n:
1441      ur.r20(Word.to_nat(n, acc), n, Word.to_nat(n, b))
1442    case 1n+ +mp:
1443      match a:
1444        case WCon{False{}, +at}:
1445          Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), acc))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), Nat.add(Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), ur.r14(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), n, um.k(n, mp, at, Word.shl(n, b), acc), Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), acc))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), um.go(n, mp, at, Word.shl(n, b), acc))), ur.r15(Word.to_nat(n, acc), Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)), n, U.U32Nat.bit(un.top(n, b)))), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), zz)), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))), Nat.double(Word.to_nat(n, b)), un.shlv(n, b))), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(n, acc), zz), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b))), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)), ur.r16(Word.to_nat(mp, at), Word.to_nat(n, b))))
1446        case WCon{True{}, +at}:
1447          Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Nat.add(Word.to_nat(n, acc), Nat.mul(1n+Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))))), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))))), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), ur.r17(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), n, um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)))), Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), um.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)))), ur.r18(Word.to_nat(n, Word.add(n, acc, b)), Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)), n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), U.U32Nat.bit(un.top(n, b)))), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, Word.add(n, acc, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))))), Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Laws.word_add_wrap(n, acc, b))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), zz)), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))), Nat.double(Word.to_nat(n, b)), un.shlv(n, b))), ur.r19(Word.to_nat(n, acc), Word.to_nat(n, b), Word.to_nat(mp, at)))