Write footprint computation + soundness (#1990 part 2/3)

[Th0rgal]

Summary

• Adds a computable write footprint for IR statements in Compiler/Proofs/Frames.lean: Expr.staticValue, Stmt.writeFootprint, Stmt.writeFootprintList. The footprint returns some for analyzable statements (letVar, assignVar, literal-offset mstore, tstore, require, return, stop, ite, statement lists) and none for dynamic shapes.
• Proves soundness: stmtWritesOnly_writeFootprint / stmtListWritesOnly_writeFootprint, and derives execStmt_frame_rule_writeFootprint / execStmts_frame_rule_writeFootprint so the frame rule applies automatically from syntax.
• Registers the new theorems in PrintAxioms.lean (zero new axioms).

Stacked on #2005 (part 1/3). Part 3 (coupling invariants / SegmentSim / composition rules) follows. Toward #1990.

Test plan

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

---

Note

Medium Risk
Touches validation traversal, external-call/trust reporting, and whole-contract correctness theorems; changes are mostly proof-facing and tested via smoke/compile-driver checks, but errors in footprint or dispatch bridges could affect proof claims.

Overview
Adds computable IR write footprints in Compiler/Proofs/Frames.lean (Expr.staticValue, Stmt.writeFootprint / writeFootprintList) with soundness theorems linking footprints to StmtWritesOnly and automatic frame-rule lemmas (execStmt_frame_rule_writeFootprint, etc.), registered in PrintAxioms.lean.

Beyond the footprint slice, the diff widens compiler proof and product surfaces: a whole-contract scalar-events theorem (compile_preserves_semantics_with_scalar_events) plus ScalarEventSmoke in ContractFeatureTest.lean; a public CEI proof bridge (CEISafety.lean); contract-level scalar-event documentation updates in AUDIT.md.

Trust and externals: ECM modules gain stateful external summaries (StatefulExternal in ECM.lean, externalSummary on modules); trust/assumption JSON adds externalSummaries, mutability, and selectors; oracleSummary / typedReadWordSummaryModule refactors oracle lowering with source-shaped assumption names.

Macro / DSL: roles blocks on verity_contract, explicit access-control theorems, callResult lowering to tryExternalCallBind, view interface calls via oracle summary (reject multi-word view returns); cei_safe smoke showing it does not bypass CEI without trust exits; dynamic bytes/string args for linked externals and helper calls.

Infrastructure: validation passes switch to Stmt.checkRec / Expr.foldBool with _viaFold rfl lemmas; mapping-slot non-alias certificates; new Verity/Core/Model/CodeData.lean (SSTORE2 layouts, CREATE2 preimage); executable Call.Result stub; compile-driver trust tests updated for new JSON shapes.

^{Reviewed by Cursor Bugbot for commit 64c3949. 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 16, 2026 9:12am

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 64c3949. Configure here.}

[cursor]

Unused _viaFold duplicate definitions and trivial theorems

Low Severity

Each of the four validator families (validateStmtParamReferences, validateReturnShapes, validateNoUnsupportedAdtConstruct, validateNoRuntimeReturnsInConstructor) plus exprContainsAdtConstruct gains a _viaFold function clone and _eq_viaFold theorem — totalling ~15 new definitions and ~15 trivial rfl theorems. Every _viaFold function is definitionally identical to its original (e.g., stmt.checkRec f vs Stmt.checkRec f stmt), and a grep confirms none of the _viaFold names are referenced anywhere outside their own _eq_viaFold theorems. This is dead code that adds maintenance burden.

Additional Locations (2)

• Compiler/CompilationModel/Validation.lean#L243-L280
• Compiler/CompilationModel/Validation.lean#L1179-L1206

 

^{Reviewed by Cursor Bugbot for commit 64c3949. Configure here.}