law byte_merge_lo

lawful-words@0.1.0.0 · LAWS.bend:437

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

437# A word read r bytes into the pair (lo, hi): bytes r.. of lo, then bytes of hi.
438law byte_merge_lo:
439  for lo: U32
440  for hi: U32
441  for r: Nat
442  for j: Nat
443  for h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}
444  {D.byte(D.merge(lo, hi, r), j) == D.byte(lo, Nat.add(j, r)) : U32}