law shift_ok

lawful-bytes@0.1.1.0 · LAWS.bend:267

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B

267law shift_ok:
268  for b: D.Bytes
269  for d: Nat
270  for k: U32
271  for h: {D.ok(b, d) == True{} : Bool}
272  for hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}
273  {D.ok(B.shift(b, k), d) == True{} : Bool}