feat: NORM_BV_MUL_POW2_REV Bitvector rewrite

[bollu]

This PR adds a rewrite rule NORM_BV_MUL_POW2_REV,
which we suspect will improve bv_decide's performance on
problems from nötzli.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d29407b4814a2bceae1f1e41aec1ea0d0f144a1f --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-12 15:43:23)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d29407b4814a2bceae1f1e41aec1ea0d0f144a1f --onto 6ca23a7b8bee57152110ce500ce795148707d4ed. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-13 15:57:40)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d29407b4814a2bceae1f1e41aec1ea0d0f144a1f --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-12 15:43:26)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase d29407b4814a2bceae1f1e41aec1ea0d0f144a1f --onto 9da8f5dce42832b8411d58446653f3640a94a6e3. You can force reference manual CI using the force-manual-ci label. (2026-02-13 15:57:41)

[bollu]

/--
info: BitVec.extractLsb'_append_zero_eq_mul_shiftLeft {n m : Nat} (x : BitVec n) (tz : Nat) (hm : n = m + tz) :
  BitVec.extractLsb' 0 m x ++ 0#tz = BitVec.cast hm (x * 1#n <<< tz)
-/
#guard_msgs in #check BitVec.extractLsb'_append_zero_eq_mul_shiftLeft

/--
info: BitVec.shiftLeft_eq_concat_of_lt {w : Nat} {x : BitVec w} {n : Nat} (hn : n < w) :
  x <<< n = BitVec.cast ⋯ (BitVec.extractLsb' 0 (w - n) x ++ 0#n)
-/
#guard_msgs in #check BitVec.shiftLeft_eq_concat_of_lt

the new rewrite BitVec.extractLsb'_append_zero_eq_mul_shiftLeft creates a loop with `BitVec.shiftLeft_eq_concat_of_lt.

[bollu]

// https://github.com/bitwuzla/bitwuzla/blob/main/src/rewrite/rewriter.cpp#L83C1-L84C1
d_arithmetic(level == LEVEL_ARITHMETIC),
...
//https://github.com/bitwuzla/bitwuzla/blob/main/src/rewrite/rewriter.cpp#L1251-L1254
  if (d_arithmetic)
  {
    BZLA_APPLY_RW_RULE(NORM_BV_MUL_POW2_REV);
  }
...
// https://github.com/bitwuzla/bitwuzla/blob/main/src/rewrite/rewriter.cpp#L1251-L1254
    if (!d_arithmetic)
    {
      BZLA_APPLY_RW_RULE(BV_MUL_POW2);
    }

Bitwuzla has three sets of normalization rules: the default set that's always run, the arithmetic set, and the "anti-arithmetic" set which breaks arithmetic down into bitwise rewrites.

The arithmetic level is not accessible from userspace:

// https://github.com/bitwuzla/bitwuzla/blob/8f28c2e8d465576e91931787a9062f2a93d072f1/src/rewrite/rewriter.h#L60-L61
  /**
   * The level of speculative rewrites. This level can not be configured
   * from the outside and rewrites of this level are only applied specifically
   * for normalization.
   */
  inline static constexpr uint8_t LEVEL_ARITHMETIC = LEVEL_MAX + 1;

and is specially initialized by the PassNormalizer:

// https://github.dev/bitwuzla/bitwuzla/blob/8f28c2e8d465576e91931787a9062f2a93d072f1/src/preprocess/pass/normalize.cpp#L248-L255
PassNormalize::PassNormalize(Env& env,
                             backtrack::BacktrackManager* backtrack_mgr)
    : PreprocessingPass(env, backtrack_mgr, "no", "normalize"),
      d_rewriter(env, Rewriter::LEVEL_ARITHMETIC, "normalize"),
      d_stats(env.statistics(), "preprocess::" + name() + "::")
{
}

I suggest that we mimic this, and maintain three different simproc sets, called bv_normalize_common, bv_normalize_arithmetic, and bv_normalize_antiarithmetic? In the first pass, we run bv_normalize+bv_normalize_arithmetic. in the fixpoint, we run bv_normalize+bv_normalize_antiarithmetic, which should mimic the Bitwuzla behaviour.