Surface checked arithmetic proof obligations (#1993)

[Th0rgal]

Summary

• Detects safeAdd/safeSub/safeMul and addPanic/subPanic/mulPanic in verified contract bodies and generates stable per-entrypoint localObligations (e.g. checked_arithmetic_increment_1_add_no_overflow), leaving checked-arithmetic codegen untouched.
• Adds proof-facing predicates CheckedArithmetic.AddNoOverflow/SubNoUnderflow/MulNoOverflow with bridging theorems safeAdd_isSome_iff_addNoOverflow, safeSub_isSome_iff_subNoUnderflow, safeMul_isSome_iff_mulNoOverflow (Verity/Proofs/Stdlib/Math.lean).
• Smoke checks that generated obligations appear for add/sub/mul; PrintAxioms.lean refreshed (zero new axioms).

Proof-obligation half of #1993. Downstream target: the 4 LocalNoOverflowFor local axioms in morpho-verity Proofs/Disciplines.lean become provable obligations. Stacked on #2009 (#1994 execution summaries); the emission half (#1993a) lands separately.

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

Medium Risk
Changes contract spec generation and obligation surfacing across all entrypoints; incorrect detection or naming could mislead proofs, though smoke tests and unchanged codegen limit runtime impact.

Overview
The Verity macro now scans function, constructor, and immutable-init bodies for safeAdd/safeSub/safeMul and panic variants, and merges auto-generated localObligations (stable names like checked_arithmetic_increment_1_add_no_overflow, .assumed status, text pointing at proof predicates) into compilation models without changing checked-arithmetic codegen.

Proof library: Verity/Proofs/Stdlib/Math.lean adds CheckedArithmetic.AddNoOverflow / SubNoUnderflow / MulNoOverflow and iff lemmas tying safeAdd/safeSub/safeMul .isSome to those props; PrintAxioms.lean lists the three new theorems.

Related macro work in the same diff: auto-generated _frame_holds and _view_frame execution theorems for eligible modifies / parameterless view functions (smoke examples in Effects.lean), and immutable initializers can lower through translateSafeRequireBind when init uses checked ops.

Tests: CheckedArithmeticObligationSmoke in SpecGenAndChecks.lean asserts add/sub/mul obligations on SafeCounter and SafeMulRequireSmoke.

^{Reviewed by Cursor Bugbot for commit 41c14e1. 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 18, 2026 7:31am

[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 4dbf7b7. Configure here.}