law to_nat_parts

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

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

70# The value of a word (for every word): lo + hi * 2^32, the weight 2^32 being
71# 32 doublings (U32Nat.dbl, from bend-osdev-u32).
72law to_nat_parts:
73  for +h: U32
74  for +l: U32
75  {W.W64.to_nat(W.W64.from_parts(h, l)) == Nat.add(U32.to_nat(l), U.U32Nat.dbl(32n, U32.to_nat(h))) : Nat}