law unpack_get

lawful-bytes@0.1.1.0 · proof_core.bend:99

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

99# Byte r of word q is byte 4q + r.
100law unpack_get:
101  for +ws: List<&2, U32>
102  for +q: Nat
103  for +r: Nat
104  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
105  {List.get(&2, U32, D.unpack(ws), Nat.add(Nat.mul(q, 4n), r)) == mb(List.get(&2, U32, ws, q), r) : Maybe<&2, U32>}