law unpack_set_i

lawful-bytes@0.1.1.0 · proof_core.bend:425

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

425# The same for a U32 index.
426law unpack_set_i:
427  for +ws: List<&2, U32>
428  for +i: U32
429  for +w: U32
430  for +v: U32
431  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
432  for +hw: {List.get(&2, U32, ws, U32.to_nat((i >> 2n : U32))) == Some{w} : Maybe<&2, U32>}
433  {D.unpack(List.set(&2, U32, ws, U32.to_nat((i >> 2n : U32)), W.put_byte(w, U32.to_nat((i .&. 3 : U32)), v))) == List.set(&2, U32, D.unpack(ws), U32.to_nat(i), v) : List<&2, U32>}