[opt] Add AND subset (absorption) rewrite

[cdleary]

This is also useful as an optimization because it reduces the use count for the absorbed operand and we have a bunch of things that trigger off of single-use.

From the block comment:

  // Pattern: AND subset check (mask subset).
  //
  // This is also commonly described as an AND "absorption" rewrite: if y has no
  // bits set outside x, then `y & x == y`. The rewritten form makes that "no
  // bits set outside x" condition explicit as `(y & ~x) == 0`.
  //
  // Why "subset":
  // Think of a bitvector as the set of positions where it has a 1-bit.
  // Then eq(and(x, y), y) holds when that set for y is a subset of the
  // set for x. y has no bits set outside the 1-bits of x.
  //
  // For same-width bitvectors, the following are equivalent:
  // - `eq(and(x, y), y)` means: every 1-bit in y is also a 1-bit in x
  //
  // - `eq(and(not(x), y), 0)` means: y has no 1-bits in positions where x has a
  //   0-bit (equivalently, and(not(x), y) has no 1-bits at all).
  //
  // So we can rewrite:
  // `eq(and(x, y), y)` <=> `eq(and(not(x), y), 0)`
  // `eq(and(x, y), x)` <=> `eq(and(not(y), x), 0)`
  //
  // This generalizes to n-ary and:
  //
  // `eq(and(a, b, ..., t), t)` <=> `eq(and(not(and(a, b, ...)), t), 0)`
  //
  // And similarly for `ne`.