Challenge 12 (NonZero): known verification gaps from tool limits (follow-up to #637)

[feliperodri]

Follow-up from #637 (Challenge 12: safety and correctness of NonZero, tracking #71).

PR #637 verifies all of Part 1 and every Part 2 function, but two known gaps remain that stem from underlying tool (CBMC) limitations rather than missing harnesses. Filing this so they are tracked and can be revisited as the tooling improves.

1. Full-width 64/128-bit multiplication is not solvable

Affects checked_mul, saturating_mul, unchecked_mul, and isqrt.

CBMC cannot handle full-width multiplication at 64/128 bits within reasonable time. As a result, those widths are verified over value-range inputs rather than all possible inputs (smaller widths, up to 32 bits, are verified exhaustively). For isqrt, the unverified middle range is explicitly flagged as a known gap in-code.

2. checked_pow / saturating_pow: exact result not provable after loop abstraction

The strengthened loop invariant (self == 0 || (acc != 0 && base != 0), > 0 for unsigned) makes checked_pow/saturating_pow verifiable with no exponent bound. In return, after loop abstraction the exact result value is no longer provable, so the contracts state only that the result is nonzero, not its exact value.

Follow-up

• Revisit both once CBMC's handling of wide multiplication improves, or with an alternative encoding, to close the isqrt/mul input-range gap.
• Explore whether a stronger loop contract can recover the exact-value property for checked_pow/saturating_pow.