[lmalloc]

Summary

This small PR aligns the handling of regimes within DEEP-ALI circuits to soundcalc, allowing for an optional explicitRegime override to be specified. If the override is specified, the circuit will only support that regime (either UDR or JBR). Otherwise, the circuit will support both regimes (our previous handling).

This PR also polishes stale docstrings, refining some of the TODOs present in the codebase:

• "Soundcalc TODOs" may be addressed from advances to soundcalc itself;
• "Feat TODOs" may be addressed from enhancements of our codebase.

[nadimkobeissi]

Please drop the private from getFRIProofSizeBits (Soundcalc/PCS/FRI.lean) and from gkrErrorUB and columnAggregFactor (Soundcalc/Lookup.lean). The monotonicity theorems now in main reference those three 45 times, so the branch cannot build once merged.

And while you're in there, replace the 0-as-"regime not applicable" sentinel in Circuit.totalSecBitsUDR/totalSecBitsJBR with an Option ℕ so an inapplicable regime stops being indistinguishable from zero security.

Also, makegetOptRegime reject an unrecognized key as loudly as it already rejects an unrecognized value, and add a fixture under SoundcalcIO/ZkVM/Ref/ that actually exercises explicit_regime, since nothing in CI currently does.

[lmalloc]

Fixed the first two items as suggested. For the second item, calling methods handle defaults in a semantically-consistent fashion (a missing value defaults to 0 in the context of a max argument). Further polishing is expected upon generalizing regimes.

For the third item, the first-line getOptString within getOptRegime should already handle the concern (if the key exists but is not a String, it rejects loudly). The CI behaviour related to explicit_regime should already be implicit in the parsing step plus a correct reproduction of the .md reports.