law wbp0

lawful-bytes@0.1.1.0 · proof_core.bend:297

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

297# The four bytes of a word with byte k set to v (k a literal).
298law wbp0:
299  for +w: U32
300  for +v: U32
301  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
302  {L4(W.put_byte(w, 0n, v)) == List.set(&2, U32, L4(w), 0n, v) : List<&2, U32>}