def mul_cons

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:207

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as WM
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

207# a wrapping product and its lost high part
208def mul_cons(+x: U32, +y: U32) -> {Nat.add(v(U32.mul(x, y)), WD.sc(32n, mex(x, y))) == Nat.mul(v(x), v(y)) : Nat}:
209  match x y:
210    case U32{+a} U32{+b}:
211      +p = Nat.mul(S.unsigned(32n, a), S.unsigned(32n, b))
212      +lhs = Nat.add(S.unsigned(32n, Word.mul.go(32n, 32n, a, b, Word.zero(32n))), S.scale_binary(32n, WM.excess(32n, 32n, a, b, Word.zero(32n))))
213      %Equal.sym(Nat, UD.v(U32{Word.mul(32n, a, b)}), WD.uw(32n, Word.mul(32n, a, b)), UD.vw(Word.mul(32n, a, b))) : {Nat.add(_, WD.sc(32n, WM.excess(32n, 32n, a, b, Word.zero(32n)))) == Nat.mul(UD.v(U32{a}), UD.v(U32{b})) : Nat}
214      %Equal.sym(Nat, UD.v(U32{a}), WD.uw(32n, a), UD.vw(a)) : {Nat.add(WD.uw(32n, Word.mul(32n, a, b)), WD.sc(32n, WM.excess(32n, 32n, a, b, Word.zero(32n)))) == Nat.mul(_, UD.v(U32{b})) : Nat}
215      %Equal.sym(Nat, UD.v(U32{b}), WD.uw(32n, b), UD.vw(b)) : {Nat.add(WD.uw(32n, Word.mul(32n, a, b)), WD.sc(32n, WM.excess(32n, 32n, a, b, Word.zero(32n)))) == Nat.mul(WD.uw(32n, a), _) : Nat}
216      Equal.trans(Nat, lhs, Nat.add(S.unsigned(32n, Word.zero(32n)), p), p, WM.conservation(32n, 32n, a, b, Word.zero(32n)), cong_l(S.unsigned(32n, Word.zero(32n)), 0n, p, WM.zero_unsigned(32n)))