law from_parts_zero_hi

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

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

55# Interface laws: a word whose high half is 0 is the word of its low half,
56# and the word of halves 0 and 0 is zero.
57law from_parts_zero_hi:
58  for a: U32
59  {W.W64.from_parts(0, a) == W.W64.from_u32(a) : W.W64}