law bit_byte

lawful-words@0.1.0.0 · proof_bytes.bend:268

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

268# Bit k of byte j of w is bit 8j + k of w (and 0 from k = 8 up).
269law bit_byte:
270  for +w: U32
271  for +j: Nat
272  for +k: Nat
273  {D.bit(D.byte(w, j), k) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(Nat.mul(8n, j), k))) : Bool}