law unpack_set

lawful-bytes@0.1.1.0 · proof_core.bend:394

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

394# Byte 4q + r of the word list after word q is written with its byte r set.
395law unpack_set:
396  for +ws: List<&2, U32>
397  for +q: Nat
398  for +r: Nat
399  for +w: U32
400  for +v: U32
401  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
402  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
403  for +hw: {List.get(&2, U32, ws, q) == Some{w} : Maybe<&2, U32>}
404  {D.unpack(List.set(&2, U32, ws, q, W.put_byte(w, r, v))) == List.set(&2, U32, D.unpack(ws), Nat.add(Nat.mul(q, 4n), r), v) : List<&2, U32>}