law unpack_get_n

lawful-bytes@0.1.1.0 · proof_core.bend:116

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

116# Byte n of the word list: byte n % 4 of word n / 4.
117law unpack_get_n:
118  for +ws: List<&2, U32>
119  for +n: Nat
120  {List.get(&2, U32, D.unpack(ws), n) == mb(List.get(&2, U32, ws, Nat.div(n, 4n)), Nat.mod(n, 4n)) : Maybe<&2, U32>}