[Example Contract] Implement ERC721 NFT contract with advanced state modeling

[Th0rgal]

Summary

Implement a fully-compliant ERC721 (NFT) contract with complete formal verification, demonstrating DumbContracts' capability for complex state models and ownership tracking.

Motivation

• Current examples: Simple state (single/few storage slots)
• ERC721 complexity: Token IDs, ownership tracking, approvals
• Market relevance: Second most important standard after ERC20
• Technical challenge: Tests finite set reasoning and complex mappings
• Proof of capability: Shows scalability to NFT platforms

Current State

All existing examples have simple state:

• SimpleStorage: Single value
• Counter: Single counter
• Ledger: Address → balance mapping
• SimpleToken: Similar to Ledger

ERC721 needs:

• Multiple interrelated mappings
• Token ID tracking
• Ownership transfers
• Approval system (token-level + operator-level)

Proposed Implementation

State Model

structure ERC721State where
  -- Core mappings
  owners : Nat → Address                   -- tokenId → owner
  balances : Address → Nat                 -- owner → token count
  tokenApprovals : Nat → Address           -- tokenId → approved address
  operatorApprovals : (Address × Address) → Bool  -- (owner, operator) → approved
  
  -- Tracking
  knownTokenIds : FiniteNatSet             -- All minted tokens
  knownOwners : FiniteAddressSet           -- All addresses with tokens
  
  -- Metadata
  totalSupply : Nat
  nextTokenId : Nat                        -- For sequential minting

ERC721 Interface

structure ERC721Spec where
  -- Views
  balanceOf : Address → ContractState → Nat
  ownerOf : Nat → ContractState → Option Address
  getApproved : Nat → ContractState → Option Address
  isApprovedForAll : Address → Address → ContractState → Bool
  
  -- Mutations
  mint : Address → Spec                    -- Mint to address
  burn : Nat → Spec                        -- Burn token
  transferFrom : Address → Address → Nat → Spec
  approve : Address → Nat → Spec          -- Approve specific token
  setApprovalForAll : Address → Bool → Spec  -- Approve all tokens
  
  -- Events
  emitTransfer : Address → Address → Nat → Event
  emitApproval : Address → Address → Nat → Event
  emitApprovalForAll : Address → Address → Bool → Event

Properties to Prove (30+)

Uniqueness Properties (5)

1. Unique ownership: Each tokenId has exactly one owner
2. No phantom tokens: tokenId exists ⇒ owner exists
3. Balance consistency: balances[owner] = #{tokens owned by owner}
4. Supply consistency: totalSupply = |knownTokenIds|
5. Owner set consistency: knownOwners = {addr | balances[addr] > 0}

Transfer Properties (7)

6. Transfer changes owner: transferFrom sets new owner
7. Transfer updates balances: Decreases sender, increases recipient
8. Transfer preserves supply: totalSupply unchanged
9. Transfer requires ownership: Reverts if not owner or approved
10. Transfer clears approval: Token approval reset after transfer
11. Transfer to zero fails: Can't transfer to 0x0 address
12. Transfer self-preserves: transfer(self, tokenId) preserves ownership

Approval Properties (8)

13. Approve authorization: Only owner can approve
14. Approve sets allowance: getApproved returns approved address
15. Approve emits event: Approval event emitted
16. Operator approval independence: setApprovalForAll doesn't affect token approvals
17. Operator approval symmetric: isApprovedForAll is symmetric for (owner, operator)
18. Approval clears on transfer: Token approval cleared when transferred
19. Self-approval allowed: Can approve self (no-op)
20. Zero address approval: approve(0x0, tokenId) clears approval

Mint Properties (5)

21. Mint increases supply: totalSupply increases by 1
22. Mint increases balance: balances[to] increases by 1
23. Mint creates ownership: ownerOf(newTokenId) = to
24. Mint no duplicate IDs: Can't mint same tokenId twice
25. Mint emits Transfer: Transfer(0x0, to, tokenId) emitted

Burn Properties (5)

26. Burn decreases supply: totalSupply decreases by 1
27. Burn decreases balance: balances[owner] decreases by 1
28. Burn removes ownership: ownerOf(tokenId) = None after burn
29. Burn requires ownership: Only owner can burn
30. Burn emits Transfer: Transfer(owner, 0x0, tokenId) emitted

Implementation Phases

Phase 1: State Model & Spec (1 week)

• Define ERC721State structure
• Implement FiniteNatSet for token tracking
• Define ERC721Spec

Phase 2: EDSL Implementation (1 week)

• Implement core functions (mint, burn, transfer)
• Implement approval functions
• Add event emission

Phase 3: Uniqueness Proofs (1 week)

• Prove properties 1-5
• Requires sum properties over finite sets
• Similar to Ledger sum proofs

Phase 4: Transfer & Approval Proofs (1 week)

• Prove properties 6-20
• Complex ownership tracking
• Approval state transitions

Phase 5: Mint & Burn Proofs (3 days)

• Prove properties 21-30
• Supply consistency
• Edge cases

Phase 6: Testing & Documentation (2 days)

• Property tests for all theorems
• Differential testing
• Coverage validation

Technical Challenges

Challenge 1: Finite Token Set Tracking

Problem: Need to prove balances[owner] = count of owned tokens
Solution: Use FiniteNatSet similar to FiniteAddressSet

def FiniteNatSet := FiniteSet Nat

def countOwnedTokens (owner : Address) (state : ERC721State) : Nat :=
  state.knownTokenIds.elements.filter (fun tokenId => 
    state.owners tokenId = owner
  ).length

theorem balance_equals_count (owner : Address) (state : ERC721State) :
    state.balances owner = countOwnedTokens owner state

Challenge 2: Approval State Complexity

Problem: Two-level approval (token-level + operator-level)
Solution: Clear precedence rules and independence proofs

Challenge 3: Sum Properties

Problem: Need to prove Σ balances = totalSupply
Solution: Reuse patterns from Ledger (#65)

Dependencies

• Issue [Proofs] Complete Ledger sum property helper lemmas #65: Ledger sum proofs (patterns for finite set reasoning)
• Issue [Integration] Integrate EVMYulLean UInt256 arithmetic library #67: EVMYulLean UInt256 (for safe arithmetic)
• Issue [Example Contract] Implement ERC20 standard token with full verification #69: ERC20 implementation (similar approval patterns)

Impact

✅ ERC721 is second most important standard
✅ Complex state pushes verification limits
✅ Demonstrates NFT platform capability
✅ Attracts NFT project audits
✅ Template for ERC1155 (multi-token standard)

Estimated Effort

4 weeks for experienced Lean developer

Success Criteria

• Full ERC721 compliance (per EIP-721)
• All 30+ properties proven (no sorry)
• Property tests for all theorems
• CI passes
• Documentation complete
• Differential tests against reference ERC721

Related Issues

• Builds on ERC20 ([Example Contract] Implement ERC20 standard token with full verification #69)
• Requires sum proofs ([Proofs] Complete Ledger sum property helper lemmas #65)
• Uses verified arithmetic ([Integration] Integrate EVMYulLean UInt256 arithmetic library #67)

Future Work

• ERC721Enumerable extension
• ERC721Metadata extension (name, symbol, tokenURI)
• ERC1155 multi-token standard

[Th0rgal]

Review Findings

1. Wrong File Paths

All DumbContracts/ paths should be Verity/:

• DumbContracts/Examples/ERC721/ → Verity/Examples/ERC721.lean (or directory)
• References to DumbContracts/Core/FiniteSet.lean → Verity/Core/FiniteSet.lean

2. FiniteSet Infrastructure May Be Insufficient

The issue mentions needing FiniteNatSet for token IDs. Currently only FiniteAddressSet (wrapping FiniteSet String) exists in Verity/Core/FiniteSet.lean. A FiniteNatSet or FiniteSet Nat would need to be added.

The existing FiniteSet is generic (FiniteSet α) but FiniteAddressSet is the only concrete instantiation. Adding FiniteNatSet should be straightforward but is not mentioned as a prerequisite.

3. Depends on #69 Which Has Issues

This issue lists #69 (ERC20) as a dependency for "approval patterns." Since #69 itself has incorrect claims about SimpleToken (see comment on #69), the dependency chain should be reassessed.

4. 30+ Properties is Ambitious

The issue proposes 30+ properties. For comparison, SimpleToken (the largest current contract) has 56 theorems but is structurally simpler (no multi-level approvals). The 4-week estimate may be optimistic given that sum properties (#65) are already 2+ weeks estimated for simpler Ledger contract.