LAWS.mul_of_max_halves: law of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/LAWS.bend as LAWS
Lines 26-28 of bend-osdev-word64@0.1.1.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/LAWS.bend&start_line=26&end_line=28

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

# (2^32 - 1)^2 = 2^64 - 2^33 + 1
law mul_of_max_halves:
  {W.W64.mul(W.W64.from_u32(4294967295), W.W64.from_u32(4294967295)) == W.W64.from_parts(4294967294, 1) : W.W64}

Uses (4):
  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.from_parts
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.from_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.mul