law shl_one_wrap

bend-osdev-word64@0.1.1.0 · LAWS_bits.bend:45

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

45# A shift left by one bit: twice the value, less 2^64 for the top bit (bit
46# 31 of the high half) going out.
47law shl_one_wrap:
48  for +a: W.W64
49  {Nat.add(W.W64.to_nat(W.W64.shl(a, 1n)), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(W.W64.hi(a), 31n)))) == Nat.double(W.W64.to_nat(a)) : Nat}