[Property Coverage] Add finite address set modeling for sum properties

[Th0rgal]

Overview

Enable proving sum properties ("total supply = sum of all balances") by adding finite address set abstraction.

Status: Design clear, well-understood problem
Effort: 1-2 weeks
Difficulty: Medium (requires modeling changes)
Priority: Low (polish, not blocking core verification)
Impact: Completes Ledger contract verification to 100%

Current State

Property Coverage: 70% (203/292)

• ✅ All testable properties are covered!
• ❌ 7 sum properties cannot be proven

The 7 Blocked Properties:

1. mint_sum_equation - Minting increases total by amount
2. burn_sum_equation - Burning decreases total by amount
3. transfer_sum_preservation - Transfers preserve total
4. totalSupply_equals_sum - Total supply equals sum of all balances
5. mint_increases_supply - Minting increases total supply
6. burn_decreases_supply - Burning decreases total supply
7. transfer_preserves_supply - Transfers don't change total supply

The Problem

Current model: Addresses are unbounded (Nat, representing uint160)

structure State where
  balances : Nat → Nat  -- Address → Balance (unbounded)
  totalSupply : Nat

Issue: Cannot sum over infinite domain

• Cannot express "sum of all balances"
• Properties like totalSupply = Σ balances are unprovable

Proposed Solution

Add Finite Address Set Abstraction

-- Finite set of addresses with bound
structure FiniteAddressSet where
  addresses : Finset Address
  maxSize : addresses.card ≤ 2^160  -- Bound by uint160 max

-- State with tracked addresses  
structure StateWithAddresses where
  balances : Nat → Nat
  totalSupply : Nat
  knownAddresses : FiniteAddressSet
  -- Invariant: only knownAddresses have non-zero balances
  balances_finite : ∀ addr ∉ knownAddresses.addresses, balances addr = 0

Prove Sum Properties

-- Helper: sum balances over finite set
def sum_balances (addrs : Finset Address) (balances : Address → Nat) : Nat :=
  addrs.sum (fun addr => balances addr)

-- Main invariant
theorem totalSupply_equals_sum (s : StateWithAddresses) :
    s.totalSupply = sum_balances s.knownAddresses.addresses s.balances := by
  -- Proof by induction on operations (mint, burn, transfer)
  sorry

-- Now we can prove the 7 properties!
theorem mint_preserves_supply_sum (s : StateWithAddresses) (to : Address) (amount : Nat) :
    let s' := mint s to amount
    sum_balances s'.knownAddresses.addresses s'.balances = 
      sum_balances s.knownAddresses.addresses s.balances + amount := by
  sorry

Implementation Plan

Phase 1: Modeling (Week 1)

Files to modify:

• DumbContracts/Core.lean - Add FiniteAddressSet
• Contract state definitions - Add knownAddresses tracking

Changes:

1. Define FiniteAddressSet structure
2. Add to contract states
3. Update operations to maintain knownAddresses
4. Prove finiteness invariant

Phase 2: Sum Properties (Week 2)

Files to modify:

• DumbContracts/Specs/Ledger.lean - Add sum property definitions
• DumbContracts/Specs/Ledger/Proofs.lean - Prove the 7 properties

Proofs:

1. totalSupply_equals_sum - Base invariant
2. mint_preserves_supply_sum - Minting adds to both
3. burn_preserves_supply_sum - Burning subtracts from both
4. transfer_preserves_supply_sum - Transfer doesn't change sum
5. Derive the other 4 from these

Acceptance Criteria

• FiniteAddressSet structure defined
• Contract states track knownAddresses
• All operations maintain knownAddresses invariant
• 7 sum properties proven (no sorries)
• Property coverage increases to ~72%+ (206/292)
• Ledger contract at 100% completeness
• CI passes (all tests)

Impact

Before: 70% property coverage, 7 sum properties unprovable

After: ~72% property coverage, Ledger contract 100% verified

• ✅ All invariants provable
• ✅ Complete verification of supply properties
• ✅ Stronger correctness guarantees

Alternative Approaches

Option B: Bounded Address Space

Use Fin (2^160) instead of Nat for addresses.

Pros: More accurate model
Cons: More complex, may require extensive refactoring

Option C: Ghost State

Add specification-only activeAddresses that tracks non-zero balances.

Pros: Minimal changes to existing code
Cons: Less explicit, harder to reason about

Recommendation: Option A (FiniteAddressSet) - clear, explicit, maintainable

References

• Current properties: DumbContracts/Specs/Ledger.lean
• Property extraction: docs/ROADMAP.md - Property Extraction section
• Finset docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Basic.html

Questions?

This is a well-understood problem with a clear solution. The main work is updating the model and proving the properties - no research needed!

[Th0rgal]

Phase 1 Complete ✅

PR #47 has been merged, completing Phase 1 of this issue:

✅ Completed (Phase 1)

• ✅ FiniteAddressSet structure defined
• ✅ Contract states track knownAddresses
• ✅ All operations maintain knownAddresses invariant
• ✅ Sum property specifications defined (7 specs in Ledger/Spec.lean)
• ✅ CI passes (all tests)

📋 Remaining Work (Phase 2)

• Prove the 7 sum properties in Ledger/Proofs.lean:
  1. Spec_deposit_sum_equation
  2. Spec_withdraw_sum_equation
  3. Spec_transfer_sum_preservation
  4. Spec_deposit_sum_singleton_sender
  5. Spec_withdraw_sum_singleton_sender
  6. Spec_deposit_withdraw_sum_cancel
  7. Spec_transfer_sum_preserved_unique
• Complete sorry placeholder in Sum.lean (helper theorem for sumBalances_insert_new)
• Property coverage increases to ~72%+ (206/292)
• Ledger contract reaches 100% completeness (32/32 properties)

The foundation is now in place for Phase 2 work. The finite address set infrastructure is fully integrated and all existing functionality continues to work.

[Th0rgal]

Phase 2 Implementation Guide

Phase 1 has been successfully merged in PR #47. This comment provides technical guidance for implementing Phase 2.

Current State

✅ Infrastructure Complete:

• FiniteAddressSet structure defined in Core/FiniteSet.lean
• sumBalances helper function in Specs/Common/Sum.lean
• Spec_* property definitions in Specs/Ledger/Spec.lean
• All contract states track knownAddresses
• All operations maintain the knownAddresses invariant

⚠️ Remaining Work:

• 1 helper theorem with sorry placeholder: sumBalances_insert_new
• 7 sum property specifications need proofs

Technical Approach

1. Helper Lemma: sumBalances_insert_new

Location: DumbContracts/Specs/Common/Sum.lean:34-43

Challenge: Proving properties about List.foldl with Uint256 modular arithmetic

Required Lemmas:

• Prove that foldl (fun acc x => acc + f x) 0 distributes over list concatenation
• Handle Uint256's add_comm and add_assoc properties
• Account for the fact that Uint256 doesn't have AddCommGroup (it's modular arithmetic)

Approach:

-- Need lemmas like:
theorem foldl_add_comm (f : α → Uint256) (a : α) (rest : List α) (acc : Uint256) :
  rest.foldl (fun acc' x => acc' + f x) (acc + f a) =
  (rest.foldl (fun acc' x => acc' x) acc) + f a := by
  -- Induction on rest, using Uint256.add_comm and add_assoc

2. Sum Property Proofs

Required Proofs (in order of dependency):

1. Spec_deposit_sum_equation - Foundation for deposit proofs

   • Show that deposit increases totalBalance by exactly amount
   • Uses: sumBalances_insert_new (if new address) or existing address logic
   • Key: Show that setMapping correctly updates the sum

2. Spec_withdraw_sum_equation - Foundation for withdraw proofs

   • Show that withdraw decreases totalBalance by exactly amount
   • Similar structure to deposit but with subtraction

3. Spec_transfer_sum_preservation - Core conservation property

   • Show that transfer doesn't change totalBalance
   • Two cases: sender == recipient (no-op), sender ≠ recipient (one decreases, one increases)

4. Spec_deposit_sum_singleton_sender - Derived property

   • Special case when only sender has non-zero balance
   • Can be derived from Spec_deposit_sum_equation

5. Spec_withdraw_sum_singleton_sender - Derived property

   • Special case when only sender has non-zero balance
   • Can be derived from Spec_withdraw_sum_equation

6. Spec_deposit_withdraw_sum_cancel - Composition property

   • This is trivially derivable from equations 1 & 2
   • Already documented as derived in the docstring

7. Spec_transfer_sum_preserved_unique - Special case of Minimal EDSL: 7 Iterations of Pattern Development (82-line core) #3

   • Can be derived from Spec_transfer_sum_preservation

Implementation Strategy

Step 1: Complete sumBalances_insert_new helper

# Work in DumbContracts/Specs/Common/Sum.lean
# Add necessary foldl lemmas to DumbContracts/Core/FiniteSet.lean if needed

Step 2: Prove core properties (1-3)

# Create DumbContracts/Proofs/Ledger/SumProperties.lean
# Import necessary modules
# Prove the 3 foundational theorems

Step 3: Derive special cases (4-7)

# These should be much easier given the foundational proofs

Step 4: Update property tracking

# Remove from property_exclusions.json once proven
# Verify property coverage improves

Resources

• Existing sum proofs: DumbContracts/Proofs/Ledger/Conservation.lean has List-based sum proofs that can guide the approach
• Uint256 properties: DumbContracts/Core/Uint256.lean has add_comm, add_assoc, sub_add_cancel, etc.
• Ledger operations: DumbContracts/Examples/Ledger.lean shows the operations being verified

Expected Effort

• Helper lemma: 2-4 hours (requires understanding Lean's foldl)
• Core proofs (1-3): 1-2 days each (requires careful handling of cases)
• Derived proofs (4-7): 2-4 hours total
• Testing & cleanup: 0.5 day

Total: ~1 week of focused Lean development work

Success Criteria

• All 8 theorems proven (no sorry placeholders)
• CI passes
• Property coverage increases from 70% to ~72%
• Ledger contract reaches 100% property completeness (32/32)

This guide should help future implementers tackle Phase 2 systematically! 🚀

[Th0rgal]

Phase 2 Implementation Analysis

I've conducted a thorough analysis of the remaining Phase 2 work for sum properties. Here's what I found:

Current State

✅ Phase 1 Complete (merged in #47)

• FiniteSet and FiniteAddressSet infrastructure
• sumBalances helper function
• All 7 Spec_* property definitions
• Property exclusions tracking

⏳ Phase 2 Remaining

• Complete sumBalances_insert_new helper theorem (has sorry)
• Prove 7 sum property specifications
• Update property_exclusions.json

Key Technical Challenges

1. List.foldl Reasoning - The FiniteSet.sum uses foldl, requiring lemmas about accumulator-based list operations

2. Uint256 Modular Arithmetic - Must relate Uint256 operations to natural number operations while handling overflow

3. FiniteAddressSet Tracking - Proofs must account for how knownAddresses evolves across operations

Critical Blocker: sumBalances_insert_new

This theorem is the foundation for all sum properties. It requires:

• Developing foldl extensionality lemmas
• Handling Uint256 arithmetic integration
• Proving function equality over list elements

Estimated effort: 3-4 days of focused Lean development.

Proof Development Roadmap

Step 1: Complete sumBalances_insert_new (3-4 days)
Step 2: Prove singleton properties (1-2 days)

• Spec_deposit_sum_singleton_sender
• Spec_withdraw_sum_singleton_sender

Step 3: Prove equation properties (2-3 days)

• Spec_deposit_sum_equation
• Spec_withdraw_sum_equation

Step 4: Prove transfer properties (2-3 days)

• Spec_transfer_sum_preservation
• Spec_transfer_sum_preserved_unique

Step 5: Prove cancellation (1 day)

• Spec_deposit_withdraw_sum_cancel

Step 6: Integration and testing (1 day)

Total Estimated Timeline: 10-14 days of focused Lean expertise

Detailed Analysis

I've created a comprehensive analysis document: /output/Phase2_Implementation_Analysis.md with:

• Full proof sketches for each property
• Required helper lemmas
• Proof patterns from existing codebase
• Step-by-step roadmap

Recommendation

Phase 2 requires advanced Lean theorem proving expertise, particularly around:

• List.foldl operations and accumulator reasoning
• Uint256 modular arithmetic
• Proof by cases with finite set tracking

The work is well-defined and ready for a Lean expert to tackle. The analysis document provides comprehensive guidance to accelerate the implementation.