law mul_of_max_halves

bend-osdev-word64@0.1.1.0 · LAWS.bend:26

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

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