[Infrastructure] Proof automation library expansion and optimization

[Th0rgal]

Summary

Expand and optimize the proof automation library (Automation.lean) to accelerate proof development and reduce boilerplate across all contracts.

Motivation

Current State (DumbContracts/Proofs/Stdlib/Automation.lean):

• ~15 core lemmas
• Safe arithmetic (safeAdd, safeSub)
• Storage operations
• Contract result helpers

Gaps:

• No mapping operation lemmas
• Limited control flow lemmas
• No authorization pattern lemmas
• No event emission helpers
• No composition lemmas for complex operations

Impact of Gaps:

• Repeated proof patterns across contracts
• Slower proof development
• Copy-paste errors
• Maintenance burden

Proposed Enhancements

Category 1: Mapping Operations (NEW)

-- File: DumbContracts/Proofs/Stdlib/MappingAutomation.lean

/-- Getting from mapping preserves state -/
@[simp] theorem getMapping_runState (slot : Nat) (key : Address) :
    (getMapping slot key).runState s = s

/-- Setting mapping updates only that key -/
theorem setMapping_updates_key (slot : Nat) (key : Address) (value : Uint256) :
    let s' := (setMapping slot key value).runState s
    s'.mappings slot key = value

/-- Setting mapping preserves other keys -/
theorem setMapping_preserves_others (slot : Nat) (key key' : Address) (value : Uint256) :
    key ≠ key' →
    let s' := (setMapping slot key value).runState s
    s'.mappings slot key' = s.mappings slot key'

/-- Mapping operations preserve storage -/
@[simp] theorem setMapping_preserves_storage :
    (setMapping slot key value).runState s
    |>.storage = s.storage

Category 2: Control Flow (NEW)

-- File: DumbContracts/Proofs/Stdlib/ControlFlowAutomation.lean

/-- Successful if-branch execution -/
theorem if_true_branch (cond : Bool) (thenBranch elseBranch : Contract α) :
    cond = true →
    (if cond then thenBranch else elseBranch) = thenBranch

/-- Failed if-branch execution -/
theorem if_false_branch (cond : Bool) (thenBranch elseBranch : Contract α) :
    cond = false →
    (if cond then thenBranch else elseBranch) = elseBranch

/-- Switch statement exhaustiveness -/
theorem switch_exhaustive (value : Uint256) (cases : List (Uint256 × Contract α)) :
    (∃ case ∈ cases, case.1 = value) ∨ useDefault

/-- Loop invariant preservation -/
theorem for_loop_invariant (inv : ContractState → Prop) :
    (∀ i, inv (loopBody i).runState s) →
    inv (for_loop n loopBody).runState s

Category 3: Authorization Patterns (NEW)

-- File: DumbContracts/Proofs/Stdlib/AuthorizationAutomation.lean

/-- OnlyOwner succeeds when sender is owner -/
theorem onlyOwner_succeeds (h : s.owner = s.sender) :
    (onlyOwner >> action).isSuccess = action.isSuccess

/-- OnlyOwner fails when sender is not owner -/
theorem onlyOwner_fails (h : s.owner ≠ s.sender) :
    (onlyOwner >> action).isSuccess = false

/-- RequireAuth pattern -/
theorem requireAuth_succeeds (authorized : Address → Bool) :
    authorized s.sender = true →
    (requireAuth authorized >> action).isSuccess = action.isSuccess

/-- Multiple role authorization -/
theorem requireRole_succeeds (roles : Address → Set Role) (required : Role) :
    required ∈ roles s.sender →
    (requireRole required >> action).isSuccess = action.isSuccess

Category 4: Arithmetic Composition (ENHANCED)

-- Extend existing arithmetic automation

/-- SafeAdd associativity -/
theorem safeAdd_assoc (a b c : Uint256) :
    safeAdd a (safeAdd b c) = safeAdd (safeAdd a b) c

/-- SafeSub anti-monotonicity -/
theorem safeSub_antimonotone (a b c : Uint256) :
    b ≤ c → safeSub a c ≤ safeSub a b

/-- Arithmetic cancellation -/
theorem add_sub_cancel (a b : Uint256) :
    (a + b) - b = a  -- modulo overflow

/-- Bounded arithmetic -/
theorem safeAdd_bounded (a b : Uint256) (h : safeAdd a b = some c) :
    c ≤ MAX_UINT256

Category 5: Event Emission (NEW)

-- File: DumbContracts/Proofs/Stdlib/EventAutomation.lean

/-- Event emission preserves state -/
@[simp] theorem emitEvent_preserves_state (event : Event) :
    (emitEvent event).runState s = s

/-- Event emission succeeds -/
@[simp] theorem emitEvent_succeeds (event : Event) :
    (emitEvent event).isSuccess = true

/-- Multiple events accumulate -/
theorem emit_multiple_events (e1 e2 : Event) :
    (emitEvent e1 >> emitEvent e2).events = [e1, e2]

Category 6: State Composition (NEW)

-- File: DumbContracts/Proofs/Stdlib/CompositionAutomation.lean

/-- Sequential operations preserve properties -/
theorem seq_preserves_property (P : ContractState → Prop) :
    P s →
    (∀ s', P s' → P (op2.runState s')) →
    P ((op1 >> op2).runState s)

/-- Bind associativity -/
theorem bind_assoc (m1 : Contract α) (f : α → Contract β) (g : β → Contract γ) :
    (m1 >>= f >>= g) = (m1 >>= fun a => f a >>= g)

/-- State update idempotence -/
theorem update_idempotent (f : ContractState → ContractState) :
    f (f s) = f s →
    (updateState f >> updateState f) = updateState f

Category 7: Finite Set Reasoning (NEW)

-- File: DumbContracts/Proofs/Stdlib/FiniteSetAutomation.lean

/-- Insert preserves membership -/
theorem insert_preserves_member {a : α} {s : FiniteSet α} :
    a ∈ s.insert a

/-- Insert preserves others -/
theorem insert_preserves_others {a b : α} {s : FiniteSet α} :
    a ≠ b → (b ∈ s ↔ b ∈ s.insert a)

/-- Sum over finite set with update -/
theorem sum_update_existing {f : α → Nat} :
    a ∈ s →
    s.sum (fun x => if x = a then f a + 1 else f x) = s.sum f + 1

Optimization: Tactic Development

Create custom tactics for common patterns:

-- File: DumbContracts/Proofs/Stdlib/Tactics.lean

/-- Solve storage preservation goals automatically -/
syntax "solve_storage_preservation" : tactic

macro_rules
  | `(tactic| solve_storage_preservation) =>
    `(tactic| 
      unfold runState
      simp [setStorage, getStorage]
      ext slot
      by_cases h : slot = targetSlot
      · simp [h]
      · simp [h])

/-- Solve authorization goals -/
syntax "solve_authorization" : tactic

/-- Solve safe arithmetic goals -/
syntax "solve_safe_arithmetic" : tactic

Benefits

✅ Accelerates proof development (30-50% faster)
✅ Reduces boilerplate
✅ Consistent proof style
✅ Easier maintenance
✅ Reusable across contracts
✅ Enables rapid prototyping

Implementation Plan

Phase 1: Core Extensions (1 week)

• Mapping operations
• Control flow helpers
• Authorization patterns

Phase 2: Advanced Automation (1 week)

• Arithmetic composition
• Event emission
• State composition

Phase 3: Finite Set Reasoning (3 days)

• Set operations
• Sum properties
• Membership proofs

Phase 4: Custom Tactics (1 week)

• Storage preservation tactic
• Authorization tactic
• Arithmetic tactic

Phase 5: Documentation & Testing (2 days)

• Document all lemmas
• Add examples
• Performance benchmarks

Files Affected

Extend:

• DumbContracts/Proofs/Stdlib/Automation.lean

Create:

• DumbContracts/Proofs/Stdlib/MappingAutomation.lean
• DumbContracts/Proofs/Stdlib/ControlFlowAutomation.lean
• DumbContracts/Proofs/Stdlib/AuthorizationAutomation.lean
• DumbContracts/Proofs/Stdlib/EventAutomation.lean
• DumbContracts/Proofs/Stdlib/CompositionAutomation.lean
• DumbContracts/Proofs/Stdlib/FiniteSetAutomation.lean
• DumbContracts/Proofs/Stdlib/Tactics.lean

Estimated Effort

3-4 weeks

Success Criteria

• 50+ new automation lemmas
• Custom tactics working
• 30%+ proof development speedup
• All contracts use automation
• Documentation complete

Related Issues

• Accelerates [Proofs] Complete Ledger sum property helper lemmas #65, [Example Contract] Implement ERC20 standard token with full verification #69, [Example Contract] Implement ERC721 NFT contract with advanced state modeling #73, [Example Contract] Multi-signature wallet with governance patterns #78 (contract proofs)
• Complements [Documentation] Create proof debugging handbook #70 (proof debugging guide)
• Enables [Documentation] Create 'Adding Your First Contract' tutorial #66 (first contract tutorial)

Future Work

• Machine learning for tactic suggestion
• Proof search automation
• SMT solver integration

[Th0rgal]

Review Findings

1. Wrong File Paths

DumbContracts/Proofs/Stdlib/Automation.lean → Verity/Proofs/Stdlib/Automation.lean
All proposed new file paths under DumbContracts/ should use Verity/.

2. Current Automation Library is Larger Than Described

The issue says "approximately 15 core lemmas." The actual Verity/Proofs/Stdlib/Automation.lean contains the addressToNat_injective axiom plus extensive helper lemmas. The Verity/Proofs/Stdlib/Math.lean file has 25 proven theorems. Combined, the stdlib is more substantial than "~15 core lemmas."

3. The Issue is Otherwise Reasonable

The gap analysis (no mapping operation lemmas, no authorization pattern lemmas, no composition lemmas) is accurate and the proposed categories make sense for the codebase's evolution.

[Th0rgal]

Analysis Update (automated codebase review)

Significant progress has been made on proof automation since this issue was opened:

What exists now

• Verity/Proofs/Stdlib/Automation.lean — 609 lines of proof automation tactics and lemmas
• Verity/Proofs/Stdlib/Math.lean — 329 lines of mathematical automation (modular arithmetic, overflow/underflow)
• Verity/Proofs/Stdlib/State.lean — State manipulation lemmas and simplification rules
• Verity/Proofs/Stdlib/Blockchain.lean — Blockchain-specific automation
• Verity/Proofs/Stdlib/SpecInterpreter.lean — 632 lines including execStmtsFuel with fuel-based execution

Impact

The automation is actively used across all 7 contract proof files in Compiler/Proofs/SpecCorrectness/, enabling 305 fully proven theorems with 0 sorry.

Recommendation

This issue should be updated to reflect current status — the core automation library is substantial. Remaining work could focus on:

• Reducing proof verbosity for new contracts (current proofs can be lengthy)
• Automating the edslToSpecStorage bridge pattern
• Decision procedures for storage slot disjointness (relevant to [Architecture] Formalize storage layout specification to prevent slot collisions #84)

[Th0rgal]

Status Update (2026-02-18)

This issue has significant outdated content. Key updates:

Path Renames

All DumbContracts/ paths → Verity/. The project was renamed. Files are now at:

• Verity/Proofs/Stdlib/Automation.lean
• Verity/Proofs/Stdlib/MappingAutomation.lean (already exists!)
• Verity/Proofs/Stdlib/ListSum.lean (new, PR fix: deduplicate list-sum helpers into shared ListSum module #378)

Partially Implemented Categories

Category 1 (Mapping Operations) — DONE. MappingAutomation.lean exists with all proposed lemmas plus more (mapping preservation, sender preservation, etc.). 90 Stdlib theorems in the manifest.

Category 4 (Arithmetic) — MOSTLY DONE. safeAdd_comm, safeAdd_some, safeSub_some, safeSub_none_iff_lt, etc. are all in Automation.lean. ListSum.lean (PR #378) adds occurrence-counting and sum conservation lemmas.

Category 7 (Finite Set) — PARTIALLY DONE. FiniteSet has insert, sum, insert_of_not_mem, mem_elements_insert. PR #380 removed unused set operations. ListSum.lean provides the sum-over-list-with-update patterns.

Not Yet Implemented

• Category 2 (Control Flow) — if_true_branch/if_false_branch are trivial (Lean's if reduces by rfl). Loop invariants remain relevant if loops are added.
• Category 3 (Authorization) — Not implemented as generic automation. Each contract proves its own owner checks inline.
• Category 5 (Events) — No event automation. Events are handled by SpecInterpreter but no @[simp] lemmas.
• Category 6 (Composition) — bind_assoc is Lean's monad law. seq_preserves_property not implemented.
• Custom Tactics — Not implemented. simp with @[simp] lemmas covers most patterns.

Recommendation

This issue should either be:

1. Rewritten to focus on the remaining gaps (event lemmas, composition lemmas, custom tactics), or
2. Closed and replaced with targeted issues for specific missing automation