[Integration] Integrate EVMYulLean UInt256 arithmetic library

[Th0rgal]

Summary

Replace/enhance current Uint256 implementation with the comprehensive, well-tested UInt256 library from EVMYulLean.

Motivation

• EVMYulLean has mature UInt256 library with proven properties
• DumbContracts has basic Uint256 (DumbContracts/EVM/Uint256.lean)
• Code reuse opportunity for better-tested arithmetic
• Cross-project validation reduces verification burden

Current State

DumbContracts Uint256:

• Basic operations (add, sub, mul, div, mod)
• Limited lemmas
• ~200 LOC

EVMYulLean Uint256:

• Comprehensive modular arithmetic
• Overflow/underflow semantics
• Well-tested properties
• ~500 LOC + lemmas

Implementation Plan

Phase 1: Extract (1 day)

cp EVMYulLean/EvmYul/UInt256.lean DumbContracts/EVM/Uint256Verified.lean
# Review and adapt to DumbContracts naming conventions

Phase 2: Integration (1 day)

Integrate verified lemmas:

-- EVMYulLean provides:
theorem add_mod : (a + b) % 2^256 = ...
theorem sub_underflow : a < b → (a - b) % 2^256 = 2^256 - (b - a)
theorem mul_overflow : ...
theorem div_by_zero : ...

Phase 3: Update Automation (1 day)

-- Update Automation.lean to use verified arithmetic
theorem safeAdd_some_iff_le (a b : Uint256Verified) :
    (safeAdd a b).isSome ↔ (a : Nat) + (b : Nat) ≤ MAX_UINT256 := by
  -- Now proven using EVMYulLean lemmas

Benefits

✅ Reduces verification burden (arithmetic proven once)
✅ Catches edge cases in modular arithmetic
✅ Improves trust in numeric operations
✅ Cross-project validation
✅ Leverages EVMYulLean's extensive testing

Risks & Mitigation

• Risk: API differences between implementations

• Mitigation: Adapter layer if needed, gradual migration

• Risk: Increased dependencies

• Mitigation: Vendor the code (copy, don't link)

Files Affected

• Extract: EVMYulLean/EvmYul/UInt256.lean
• Create: DumbContracts/EVM/Uint256Verified.lean
• Update: DumbContracts/EVM/Uint256.lean (compatibility layer)
• Update: DumbContracts/Proofs/Stdlib/Automation.lean

Estimated Effort

3 days

Dependencies

• Access to EVMYulLean repository (already cloned)
• None blocking

Success Criteria

• ✅ lake build passes with new Uint256
• ✅ All existing proofs still work
• ✅ New arithmetic lemmas available in Automation.lean
• ✅ Documentation updated

Related

• Part of EVMYulLean integration strategy
• Enables more robust arithmetic-heavy contracts (ERC20, ERC721)

[Th0rgal]

Review Findings

1. Wrong File Paths

All paths use DumbContracts/ which has been renamed to Verity/:

• DumbContracts/EVM/Uint256.lean → Verity/EVM/Uint256.lean (re-export) / Verity/Core/Uint256.lean (actual impl)
• DumbContracts/EVM/Uint256Verified.lean → Would be Verity/EVM/Uint256Verified.lean
• DumbContracts/Proofs/Stdlib/Automation.lean → Verity/Proofs/Stdlib/Automation.lean

2. "EVMYulLean already cloned" — Not True

The issue states "Access to EVMYulLean repository (already cloned)" under Dependencies. EVMYulLean is not present in the repository. The only git submodule is lib/forge-std. This dependency needs to be fetched/vendored before any integration work can begin.

3. Current Uint256 is More Substantial Than Described

The issue says "Basic operations (add, sub, mul, div, mod), Limited lemmas, ~200 LOC". In reality, Verity/Core/Uint256.lean is 550 lines with substantial lemma coverage including:

• add_comm, add_assoc, add_left_comm
• sub_add_cancel, sub_add_cancel_of_lt (important — 130+ line proof)
• add_right_cancel, add_mul, sub_add_cancel_left
• zero_add, add_zero, sub_zero, sub_self, div_one, etc.

This is not "limited lemmas" — it's a reasonably complete library. The effort to integrate EVMYulLean may not be as beneficial as described, especially given the API adaptation overhead.

3-day estimate seems reasonable if EVMYulLean is actually accessible and compatible.