feat: parallel-prefix-sum circuit

[luisacicolini]

This PR introduces a new operation BitVec.hAdd, which recursively adds l-long words in a (flattened) w-long bitvector, similarly to the vectorized add operation we find e.g. in LLVM and in assembly intrinsics. We equip this operation with a bitblastable circuit and operation (parPreSum) implementing the operation via parallel-prefix-sum circuit for efficiency.

This circuit is the base to construct an efficient bitblasting circuit for BitVec.cpop, and part of our effort to make the RISC-V ISA bitblastable.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e6d021967eee968e05aa9e953c63bd962a44b8be --onto d92cdae8e901d3d9686f8c0e88a0371379c49dff. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-09 16:55:32)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e6d021967eee968e05aa9e953c63bd962a44b8be --onto 470498cc061e40ae5fb8312fb7e7939a0f0d0f6f. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-11 11:46:38)

[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 e6d021967eee968e05aa9e953c63bd962a44b8be --onto d92cdae8e901d3d9686f8c0e88a0371379c49dff. You can force reference manual CI using the force-manual-ci label. (2026-01-09 16:55:34)