feat(Codegen,Proofs): automatic checked-arithmetic obligations (solc 0.8 overflow semantics)

Problem

Two related gaps, revealed by the Morpho Blue/Midnight ports (Th0rgal/morpho-verity):

1. Yul drift: solc 0.8 generates checked_add_* / checked_sub_* / checked_mul_* helpers by default. Verity does not emit shape-matched equivalents, so these helpers account for a large share of the 75 solc-only vs 214 verity-only functions accepted by Midnight's Yul identity gate.
2. Hand-stated overflow axioms: Blue's Proofs/Disciplines.lean carries 4 manually asserted LocalNoOverflowFor axioms (totalBorrowAssets+1, totalBorrowShares+1e6, collateral*price, collateral*price*lltv). These should be derived side conditions, not assumptions.

Note: #1752 (closed) added explicit safeAdd-style builtins only — it did not address default checked semantics or auto-derived obligations.

Scope sketch

1. Emission: an opt-in (later default) mode where source arithmetic lowers to solc-shaped checked_* Yul helpers with panic(0x11) revert paths, closing that Yul-identity-drift category.
2. Obligation generation: for each checked operation in a generated body, derive a NoOverflow side condition as a proof obligation attached to the entrypoint summary, replacing hand-stated LocalNoOverflowFor axioms.
3. Discharge support: tactic/lemma support to discharge the generated conditions from contract invariants (e.g. supply caps), or leave them as explicit assumed trust-report entries when not dischargeable.

Relations

• Pairs with the dynamic ABI codec work (#1982 P0-1) as the other big Yul-drift category.
• Obligation discharge composes with generated-body execution summaries (see companion issue) and #1990.

Start with the checked arithmetic and Yul behavior described in the issue, then inspect Proofs/Disciplines.lean and the related work in #1990 and #1982. Done means checked operations emit solc-shaped helpers, generated NoOverflow obligations replace the listed hand-stated axioms, and discharge or trust-report behavior is covered.