def native_multiply

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:138

import Base
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic

138def native_multiply(+a: U32,+b: U32) -> {U32.mul(a,b) == U32.from_nat(Nat.mul(U32.to_nat(a),U32.to_nat(b))) : U32}:
139  match a b:
140    case U32{+x} U32{+y}:
141      %Equal.sym(U32,U32.from_nat(Nat.mul(Word.to_nat(32n,x),Word.to_nat(32n,y))),U32{WordArithmetic.encode(Nat.mul(Word.to_nat(32n,x),
142              Word.to_nat(32n,y)),32n)},WordArithmetic.native_encoding(Nat.mul(Word.to_nat(32n,x),Word.to_nat(32n,y)))) : {U32{Word.mul(32n,x,
143            y)} == _ : U32}
144      %multiply(32n,x,y) : {U32{Word.mul(32n,x,y)} == U32{_} : U32}
145      {==}