law bit_merge

lawful-words@0.1.0.0 · proof_bytes.bend:745

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

745# The bits of a merged word, at byte j, bit k.
746law bit_merge:
747  for +lo: U32
748  for +hi: U32
749  for +r: Nat
750  for +j: Nat
751  for +k: Nat
752  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == Bool.and(Nat.is_lt(k, 8n), Bool.or(D.bit(lo, Nat.add(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, r))),
753    Bool.and(Nat.is_le(Nat.mul(8n, Nat.sub(4n, r)), Nat.add(Nat.mul(8n, j), k)), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n),
754      D.bit(hi, Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, Nat.sub(4n, r)))))))) : Bool}