law hi_from_parts

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

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

44# For every pair of halves: splitting the joined word gives them back.
45law hi_from_parts:
46  for h: U32
47  for l: U32
48  {W.W64.hi(W.W64.from_parts(h, l)) == h : U32}