law byte_pack4

lawful-words@0.1.0.0 · LAWS.bend:360

import Base
import lawful-words@0.1.0.0/defs.bend as D

360# Unpacking a packed word gives its bytes back. j is any index below 4 (in
361# code it is i & 3, not a literal).
362law byte_pack4:
363  for b0: U32
364  for b1: U32
365  for b2: U32
366  for b3: U32
367  for j: Nat
368  for h0: {U32.is_lt(b0, 256) == True{} : Bool}
369  for h1: {U32.is_lt(b1, 256) == True{} : Bool}
370  for h2: {U32.is_lt(b2, 256) == True{} : Bool}
371  for h3: {U32.is_lt(b3, 256) == True{} : Bool}
372  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
373  {D.byte(D.pack4(b0, b1, b2, b3), j) == D.nth4(j, b0, b1, b2, b3) : U32}