ERC721: add verified foundation scaffold and proof bridges (#73)

[Th0rgal]

Summary

Adds a merge-safe ERC721 foundation slice for #73, following the same contract-structure/proof-boundary conventions used for existing examples.

What landed

• New executable ERC721 scaffold:
  • Verity/Examples/ERC721.lean
  • storage layout for owner/supply/tokenId plus ownership + approval maps
  • core operations: constructor, mint, approve, setApprovalForAll, transferFrom
  • read helpers: balanceOf, ownerOf, getApproved, isApprovedForAll
• New formal surface:
  • Verity/Specs/ERC721/Spec.lean
  • Verity/Specs/ERC721/Invariants.lean
  • Verity/Proofs/ERC721/Basic.lean
  • Verity/Proofs/ERC721/Correctness.lean
• AST and compiler proof bridges:
  • Verity/AST/ERC721.lean
  • Compiler/Proofs/SpecCorrectness/ERC721.lean
  • Verity/Specs/ERC721/Proofs.lean (re-export)
• Project wiring and test coverage metadata:
  • Verity/All.lean imports
  • test/PropertyERC721.t.sol
  • test/property_manifest.json sync
  • docs count surfaces synced

Validation

• ~/.elan/bin/lake build
• python3 scripts/extract_property_manifest.py
• python3 scripts/check_property_manifest_sync.py
• python3 scripts/check_property_manifest.py
• python3 scripts/check_property_coverage.py
• python3 scripts/check_contract_structure.py
• python3 scripts/check_lean_hygiene.py
• python3 scripts/check_doc_counts.py

Closes #73 (foundation slice).

---

Note

^{Cursor Bugbot is generating a summary for commit db0c1ff. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
dumbcontracts	Ready	Preview, Comment	Feb 20, 2026 11:50am

[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.}

[cursor]

Wrapping add for nextTokenId inconsistent with safeAdd pattern

Low Severity

The mint function uses safeAdd with requireSomeUint for both recipientBalance and totalSupply to guard against overflow, but uses wrapping add for nextTokenId. Every other mint function in the codebase (ERC20, SimpleToken) consistently uses safeAdd for all counter increments. While currently safe because the sequential_supply invariant keeps both values equal and totalSupply's safeAdd reverts first, this inconsistency is fragile — if burn functionality is ever added (decreasing supply but not nextTokenId), the wrapping add could silently wrap nextTokenId to zero.