Correct generated msat postconditions

[JasonGross]

Summary

• specify msat as the saturated (n+1)-limb representation whose two’s-complement value is exactly the modulus
• retain its per-limb machine-word bounds without claiming that its unsigned value is less than the modulus
• regenerate the 94 affected C, Rust, Go, Zig, and Java files

Rationale

msat returns the modulus itself. Its old contract reused the ordinary field-element valid predicate, producing contradictory postconditions: twos_complement_eval out1 = m and 0 ≤ eval out1 < m. The corrected contract preserves the exact-value and limb-bound guarantees while removing the false < m claim. This fixes Scrutineer finding #2524.

All generated changes are comment-only: each affected file only loses the false postcondition line.

Testing

• focused Rocq proof compilation
• regenerated exactly the 94 affected artifacts
• GCC, Cargo, and Zig backend builds
• git diff --check

Go and Java compilers were unavailable locally; their generated diffs were verified to be comment-only.

Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.