dev: leverage non-determinism in extract_limb_bits

[enitrat]

Move extract_limb_bits to maths.cairo in cairo_core. Rename it to felt252_to_bits.

Using a hint, we can ask the prover to directly provide the bit decomposition of limb as an array of bits. The Cairo code then only needs to:

-Verify that the provided bit array is valid (i.e., contains only 0s and 1s).
-Reconstruct the original limb from the bit array and ensure it matches the input.

This approach eliminates the recursive calls and reduces the operation to a single pass for verification, significantly lowering the number of steps.

How It Works

Non-Deterministic Hint:
Inside the %{%} block, the prover computes the binary representation of limb and writes the bits directly into bits_ptr. It also sets len to the number of bits.
This is done efficiently in Python & Rust.

Verification:
The Cairo code:

• iterates over the provided bits, verifying each is either 0 or 1 using range checks.
• reconstructs the original limb by computing sum(bit[i] * 2^i) and checks that it equals the input limb.

The optimized version is still an O(n) verification steps (iteration on all bits), but these are simpler operations (multiplications and additions) and avoid recursion and heavy function calls. The heavy lifting is offloaded to the prover.

The logic is very similar to felt252_to_bytes_be