fix(circuit): strict bit-decomposition for path indices (#46)

[adamkrellenstein]

Closes #46.

The Merkle path-selection indices were derived with the non-strict to_bits_le, which only enforces Σ bitᵢ·2ⁱ ≡ x (mod p) — not canonicity. Because the Pallas scalar modulus sits just above 2²⁵⁴ while NUM_BITS = 255 (and p ≡ 1 mod 2³²), nearly every value admits a second valid 255-bit decomposition x + p whose low bits encode index + 1. A malicious prover could witness that to open leaf idx+1 instead of the challenged idx (file tree), or steer the aggregation path to index+1 while the public scalar stays index.

Fix: the two index-derivation sites in the production circuit (synth.rs — challenge_with_idx and ledger_index_public) now use to_bits_le_strict, which enforces the canonical in-field representation. Completeness is preserved (honest values are canonical); the idx+1 opening is closed.

The non-index depth_public decomposition is intentionally left as to_bits_le — it feeds active-flag/depth gating, not a path index, so it is not exploitable (per the audit).

Verified: build + api_functionality, circuit_wiring, depth_zero_cheat_regression, and security_{malicious_prover,challenge_distribution,ledger,negative_cases} all pass.

The constant-size circuit variant (formal_components.rs) has the same pattern; the matching fix is pushed to the #44 branch.

🤖 Generated with Claude Code

---

Note

High Risk
Directly patches a malicious-prover soundness issue in proof-of-retrievability path verification; incorrect constraints would break cryptographic guarantees.

Overview
Closes a soundness gap in the production Nova PoR circuit (synth.rs) where Merkle path-selection bits were derived with non-strict little-endian decomposition.

challenge_with_idx (file-tree path) and ledger_index_public (aggregation path) now use to_bits_le_strict, so the low bits used as indices are the canonical in-field representation. Non-strict decomposition only enforces congruence mod p; with a 255-bit width and modulus just above 2²⁵⁴, a prover could witness an alternate decomposition whose low bits encode index+1, opening the wrong file leaf or steering the aggregation path while public scalars still match the challenged index.

depth_public remains on to_bits_le because it drives depth gating, not path indices (not treated as exploitable here). Comments reference issue #46.

^{Reviewed by Cursor Bugbot for commit 41d7dea. Bugbot is set up for automated code reviews on this repo. Configure here.}

[codspeed-hq]

Merging this PR will not alter performance

✅ 13 untouched benchmarks
⏩ 13 skipped benchmarks¹

---

_{Comparing fix/strict-index-decomposition (41d7dea) with main (fe9f977)}

Footnotes

1. 13 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩

[adamkrellenstein]

Superseded by #50: the strict bit-decomposition fix for #46 is included there (on both index-derivation sites). Closing as redundant.