law wbp

lawful-bytes@0.1.1.0 · proof_core.bend:366

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

366law wbp:
367  for +w: U32
368  for +r: Nat
369  for +v: U32
370  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
371  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
372  {L4(W.put_byte(w, r, v)) == List.set(&2, U32, L4(w), r, v) : List<&2, U32>}