Vmac.cr.vm.mul: def of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/vmac.bend as Vmac
Lines 60-72 of bend-osdev-crypto@0.1.0.0/vmac.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/vmac.bend&start_line=60&end_line=72

import Base
import bend-osdev-word64@0.1.0.0/word64.bend as W

# the 128-bit product of two 64-bit words
def cr.vm.mul(+a: W.W64, +b: W.W64) -> CrU128:
  +al = W.W64.lo(a)
  +ah = W.W64.hi(a)
  +bl = W.W64.lo(b)
  +bh = W.W64.hi(b)
  +p0 = W.W64.mul(cr.vm.w(al), cr.vm.w(bl))
  +p1 = W.W64.mul(cr.vm.w(al), cr.vm.w(bh))
  +p2 = W.W64.mul(cr.vm.w(ah), cr.vm.w(bl))
  +p3 = W.W64.mul(cr.vm.w(ah), cr.vm.w(bh))
  +mid = W.W64.add(p1, p2)
  +lo = W.W64.add(p0, W.W64.shl(mid, 32n))
  CrU128{W.W64.add(W.W64.add(p3, W.W64.shr(mid, 32n)), W.W64.add(W.W64.shl(cr.vm.carry(W.W64.is_lt(mid, p1)), 32n), cr.vm.carry(W.W64.is_lt(lo, p0)))), lo}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/vmac.bend&name=CrU128
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/vmac.bend&name=cr.vm.carry
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/vmac.bend&name=cr.vm.w
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.hi
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.lo
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.mul
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.shl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.shr