proof: generated-body execution summaries to auto-discharge discipline axioms

Problem

#1968 (closed) made ECM/interface proof obligations explicit; nothing tracks auto-discharging them. Morpho Blue's refinement/property theorems (Th0rgal/morpho-verity, Blue/Proofs/Disciplines.lean) still rest on typed local axioms about generated bodies:

• MonotoneDiscipline / GuardedDiscipline — which storage fields each entrypoint can move, and under which guards;
• AccrueInterestIdentityFor — the accrual identity;
• ExecutableMarketIdReadAligned / ExecutableOraclePriceReadAligned — ECM alignment facts;
• LocalNoOverflowFor (4 fields) — see the companion checked-arithmetic issue.

The repo's own docs acknowledge discharging these from generated bodies as future work. Until then, Blue's Property 1/2 are axiom-backed rather than proved end-to-end.

Goal

Per-entrypoint execution summaries generated alongside the compiled body:

1. Field-movement summary: for each entrypoint, a proven theorem of the form "execution preserves all storage locations except {…}, and field X only increases / only moves under guard G" — i.e. machine-derived MonotoneDiscipline/GuardedDiscipline instances.
2. Identity/alignment summaries: derive accrual-style identities and ECM read-alignment facts from the body + ECM contracts instead of asserting them.
3. A bridge so downstream proofs consume the generated summaries by name, with the local-axiom fallback kept only behind an explicit assumed trust-report entry.

Building blocks

• Compiler/Proofs/Frames.lean (#1983, merged): PreservesBindingsExcept / PreservesSelectorCalldata combinators are the right starting shape.
• #1990 (frame rule + footprint computation) is the general mechanism; this issue is its first concrete acceptance test: Blue Disciplines.lean local-axiom count → 0.
• #1895 (effects → execution frame theorems) covers the annotation-to-theorem half.

Start by reading Blue/Proofs/Disciplines.lean and the interfaces in Compiler/Proofs/Frames.lean, then review #1990 and #1895 for the frame and effects mechanisms. Done means generated per-entrypoint summaries feed the downstream proofs, with the local-axiom count in Blue/Proofs/Disciplines.lean reduced to zero and any fallback recorded as an explicit assumed trust entry.