law vec64_halves

bend-osdev-algo@0.1.0.0 · LAWS.bend:333

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

333law vec64_halves:
334  {(A.bits64.ctz(W.W64.from_parts(1, 0)), A.bits64.clz(W.W64.from_parts(0, 1)), A.bits64.popcount(W.W64.max())) == (32n, 63n, 64n) : Nat & Nat & Nat}