Execution summary frame theorems (#1994)

[Th0rgal]

Summary

• Adds ExecutionSummary machinery to Compiler/Proofs/Frames.lean for summarizing generated function bodies: storage/address/array frame predicates (PreservesStorageExcept, PreservesAddressStorageExcept, PreservesStorageArraysExcept).
• Composition theorems (ExecutionSummary.refl/weaken/trans) and generated-body bridge theorems (execStmt_setStorage_execution_summary, execStmt_setStorageAddr_execution_summary, execStmtList_execution_summary_cons).
• Storage helper frame theorems for writeUintSlots, writeStorageWordSlots, writeAddressSlots, writeStorageArray.
• Registers new theorems in PrintAxioms.lean (zero new axioms).

Toward #1994; downstream consumer is Morpho Blue Proofs/Disciplines.lean local-axiom discharge. Complements the #1990 stack (#2005/#2007/#2008) — based on main, may need a trivial rebase after that stack lands since both extend Frames.lean.

Test plan

• lake build Verity Contracts Compiler PrintAxioms → "Build completed successfully."
• refresh_verification_artifacts.sh → [refresh] PASS
• make check → "All checks passed."
• CI green

---

Note

Low Risk
Proof-only additions in Frames.lean and PrintAxioms registration; no runtime or auth behavior changes.

Overview
Adds ExecutionSummary in Compiler/Proofs/Frames.lean: a bundled record of “what changed” across bindings, storage slots, address storage, storage arrays, and selector/calldata, with refl, weaken, and trans for composing summaries along successful runs.

New “except written slots” lemmas for writeUintSlots, writeStorageWordSlots, writeAddressSlots, and writeStorageArray, plus bridge theorems that setStorage / setStorageAddr successful execStmt steps yield an ExecutionSummary, and execStmtList_execution_summary_cons chains stmt + rest via ExecutionSummary.trans. PreservesSelectorCalldata is hoisted next to the other preservation abbreviations.

Compiler.lean imports Compiler.Proofs.Frames; PrintAxioms.lean registers the new public theorems (theorem count 5227 → 5240, no new axioms).

^{Reviewed by Cursor Bugbot for commit 52c3ff7. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jun 17, 2026 12:49pm

[github-actions]

\n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n```

[Th0rgal]

bugbot run

[cursor]

✅ Bugbot reviewed your changes and found no new issues!

Comment @cursor review or bugbot run to trigger another review on this PR

^{Reviewed by Cursor Bugbot for commit 5b3c464. Configure here.}