law shl_value

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

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

154# Shifts, as Nat facts. A shift left by k < 64 multiplies the value by 2^k
155# when the result is no more than a word's value; a shift right by k < 64
156# is the floor of the value divided by 2^k (2^k times it is at most the
157# value, and 2^k times one more is above it); by 64 or more, both give 0.
158law shl_value:
159  for +a: W.W64
160  for +k: Nat
161  for +c: W.W64
162  for hk: {Nat.is_lt(k, 64n) == True{} : Bool}
163  for +h: {Nat.is_le(U.U32Nat.dbl(k, W.W64.to_nat(a)), W.W64.to_nat(c)) == True{} : Bool}
164  {W.W64.to_nat(W.W64.shl(a, k)) == U.U32Nat.dbl(k, W.W64.to_nat(a)) : Nat}