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

Compiler/Proofs/SpecCorrectness/ERC721.lean

@@ -0,0 +1,43 @@
+/-
+  Compiler.Proofs.SpecCorrectness.ERC721
+
+  Initial bridge theorem surface for ERC721 scaffolding.
+-/
+
+import Verity.Specs.ERC721.Spec
+import Verity.Examples.ERC721
+import Verity.Proofs.ERC721.Basic
+
+namespace Compiler.Proofs.SpecCorrectness
+
+open Verity
+open Verity.Specs.ERC721
+
+/-- Spec/EDSL agreement for read-only `balanceOf`. -/
+theorem erc721_balanceOf_spec_correct (s : ContractState) (addr : Address) :
+    balanceOf_spec addr ((Verity.Examples.ERC721.balanceOf addr).runValue s) s := by
+  simpa using Verity.Proofs.ERC721.balanceOf_meets_spec s addr
+
+/-- Spec/EDSL agreement for read-only `ownerOf`. -/
+theorem erc721_ownerOf_spec_correct (s : ContractState) (tokenId : Uint256) :
+    ownerOf_spec tokenId ((Verity.Examples.ERC721.ownerOf tokenId).runValue s) s := by
+  simpa using Verity.Proofs.ERC721.ownerOf_meets_spec s tokenId
+
+/-- Spec/EDSL agreement for read-only `getApproved`. -/
+theorem erc721_getApproved_spec_correct (s : ContractState) (tokenId : Uint256) :
+    getApproved_spec tokenId ((Verity.Examples.ERC721.getApproved tokenId).runValue s) s := by
+  simpa using Verity.Proofs.ERC721.getApproved_meets_spec s tokenId
+
+/-- Spec/EDSL agreement for read-only `isApprovedForAll`. -/
+theorem erc721_isApprovedForAll_spec_correct (s : ContractState) (ownerAddr operator : Address) :
+    isApprovedForAll_spec ownerAddr operator
+      ((Verity.Examples.ERC721.isApprovedForAll ownerAddr operator).runValue s) s := by
+  simpa using Verity.Proofs.ERC721.isApprovedForAll_meets_spec s ownerAddr operator
+
+/-- Spec/EDSL agreement for `setApprovalForAll` with sender-bound owner. -/
+theorem erc721_setApprovalForAll_spec_correct (s : ContractState) (operator : Address) (approved : Bool) :
+    setApprovalForAll_spec s.sender operator approved s
+      ((Verity.Examples.ERC721.setApprovalForAll operator approved).runState s) := by
+  simpa using Verity.Proofs.ERC721.setApprovalForAll_meets_spec s operator approved
+
+end Compiler.Proofs.SpecCorrectness

README.md

@@ -28,7 +28,7 @@ source ~/.elan/env
 # 2. Clone and build
 git clone https://github.com/Th0rgal/verity.git
 cd verity
-lake build                                    # Verifies all 412 theorems
+lake build                                    # Verifies all 423 theorems
 
 # 3. Generate a new contract
 python3 scripts/generate_contract.py MyContract
@@ -88,11 +88,13 @@ One spec can have many competing implementations - naive, gas-optimized, packed
 | Ledger | 33 | Deposit/withdraw/transfer with balance conservation |
 | SimpleToken | 61 | Mint/transfer, supply conservation, storage isolation |
 | ERC20 | 11 | Foundation scaffold with initial spec/read-state proofs |
+| ERC721 | 11 | Foundation scaffold with token ownership/approval proof baseline |
 | ReentrancyExample | 4 | Reentrancy vulnerability vs safe withdrawal |
 
 **Unverified examples**:
 - [CryptoHash](Verity/Examples/CryptoHash.lean) demonstrates external library linking via the [Linker](Compiler/Linker.lean) but has no specs or proofs.
 - [ERC20](Verity/Examples/ERC20.lean) is a new foundation scaffold with executable logic plus formal spec/invariant modules in `Verity/Specs/ERC20/`, with proof development tracked in [#69](https://github.com/Th0rgal/verity/issues/69).
+- [ERC721](Verity/Examples/ERC721.lean) is a new foundation scaffold with executable logic plus formal spec/invariant modules in `Verity/Specs/ERC721/`, with proof development tracked in [#73](https://github.com/Th0rgal/verity/issues/73).
 
 ### Using External Libraries (Linker)
 
@@ -126,7 +128,7 @@ Stmt.letVar "h" (Expr.externalCall "myHash" [Expr.param "a", Expr.param "b"])
 
 See [`examples/external-libs/README.md`](examples/external-libs/README.md) for a step-by-step guide and [`docs-site/content/guides/linking-libraries.mdx`](docs-site/content/guides/linking-libraries.mdx) for the full documentation.
 
-412 theorems across 10 categories, all fully proven. 376 Foundry tests across 33 test suites. 231 covered by property tests (56% coverage, 181 proof-only exclusions). 1 documented axioms. 0 `sorry` — Ledger sum proofs completed in Conservation.lean ([#65](https://github.com/Th0rgal/verity/issues/65)).
+423 theorems across 11 categories, all fully proven. 377 Foundry tests across 34 test suites. 242 covered by property tests (57% coverage, 181 proof-only exclusions). 1 documented axioms. 0 `sorry` — Ledger sum proofs completed in Conservation.lean ([#65](https://github.com/Th0rgal/verity/issues/65)).
 
 ## What's Verified
 
@@ -163,7 +165,7 @@ FOUNDRY_PROFILE=difftest forge test
 <details>
 <summary><strong>Testing</strong></summary>
 
-**Foundry tests** (376 tests) validate EDSL = Yul = EVM execution:
+**Foundry tests** (377 tests) validate EDSL = Yul = EVM execution:
 
 ```bash
 FOUNDRY_PROFILE=difftest forge test                                          # run all

TRUST_ASSUMPTIONS.md

@@ -79,7 +79,7 @@ theorem increment_correct (state : ContractState) :
     finalState.storage countSlot = add (state.storage countSlot) 1
 ```
 
-**Coverage**: All 401 theorems are formally proven (100% proof coverage). Additionally, 231 theorems have corresponding Foundry property tests (56% runtime test coverage).
+**Coverage**: All 401 theorems are formally proven (100% proof coverage). Additionally, 242 theorems have corresponding Foundry property tests (57% runtime test coverage).
 
 **What this guarantees**:
 - Contract behavior matches specification
@@ -690,7 +690,7 @@ Verity provides **strong formal verification** with a **small trusted computing
 ✅ Contract implementations match specifications (Layer 1)
 ✅ Specifications preserved through compilation (Layer 2)
 ✅ IR semantics equivalent to Yul semantics (Layer 3)
-✅ 412 theorems across 10 categories (220 covered by property tests)
+✅ 423 theorems across 11 categories (220 covered by property tests)
 
 ### What is Trusted (Validated but Not Proven)
 ⚠️ Solidity compiler (solc) - Validated by 70k+ differential tests

Verity/AST/ERC721.lean

@@ -0,0 +1,28 @@
+/-
+  Verity.AST.ERC721: initial AST bridge scaffold.
+
+  This file establishes the AST/denotation seam for ERC721 foundation work.
+-/
+
+import Verity.Denote
+import Verity.Examples.ERC721
+
+namespace Verity.AST.ERC721
+
+open Verity
+open Verity.AST
+open Verity.Denote
+open Verity.Examples.ERC721 (balanceOf)
+
+/-- AST for `balanceOf(addr)`: return mapping slot3[addr]. -/
+def balanceOfAST : Stmt :=
+  .bindUint "x" (.mapping 3 (.varAddr "addr"))
+    (.ret (.var "x"))
+
+/-- `balanceOf` AST denotes to the EDSL `balanceOf` function. -/
+theorem balanceOf_equiv (addr : Address) :
+    denoteUint emptyEnv (fun s => if s == "addr" then addr else 0) balanceOfAST
+    = balanceOf addr := by
+  rfl
+
+end Verity.AST.ERC721

Verity/All.lean

@@ -28,6 +28,7 @@ import Verity.AST.Owned
 import Verity.AST.OwnedCounter
 import Verity.AST.SimpleToken
 import Verity.AST.ERC20
+import Verity.AST.ERC721
 
 -- Common specifications
 import Verity.Specs.Common
@@ -49,6 +50,7 @@ import Verity.Examples.OwnedCounter
 import Verity.Examples.Ledger
 import Verity.Examples.SimpleToken
 import Verity.Examples.ERC20
+import Verity.Examples.ERC721
 import Verity.Examples.ReentrancyExample
 import Verity.Examples.CryptoHash
 
@@ -111,3 +113,10 @@ import Verity.Specs.ERC20.Invariants
 import Verity.Specs.ERC20.Proofs
 import Verity.Proofs.ERC20.Basic
 import Verity.Proofs.ERC20.Correctness
+
+-- ERC721 (foundation scaffold): Spec + initial bridge/basic proofs
+import Verity.Specs.ERC721.Spec
+import Verity.Specs.ERC721.Invariants
+import Verity.Specs.ERC721.Proofs
+import Verity.Proofs.ERC721.Basic
+import Verity.Proofs.ERC721.Correctness

Verity/Examples/ERC721.lean

@@ -0,0 +1,132 @@
+/-
+  ERC721 (foundation scaffold):
+  - balances mapping
+  - token ownership by tokenId
+  - token approvals and operator approvals
+
+  This module provides a compile-safe executable baseline for issue #73.
+-/
+
+import Verity.Core
+import Verity.EVM.Uint256
+import Verity.Stdlib.Math
+
+namespace Verity.Examples.ERC721
+
+open Verity
+open Verity.EVM.Uint256
+open Verity.Stdlib.Math
+
+-- Storage layout
+def owner : StorageSlot Address := ⟨0⟩
+def totalSupply : StorageSlot Uint256 := ⟨1⟩
+def nextTokenId : StorageSlot Uint256 := ⟨2⟩
+def balances : StorageSlot (Address → Uint256) := ⟨3⟩
+def owners : StorageSlot (Uint256 → Uint256) := ⟨4⟩
+def tokenApprovals : StorageSlot (Uint256 → Uint256) := ⟨5⟩
+def operatorApprovals : StorageSlot (Address → Address → Uint256) := ⟨6⟩
+
+def addressToWord (a : Address) : Uint256 :=
+  (a.toNat : Uint256)
+
+def wordToAddress (w : Uint256) : Address :=
+  Verity.Core.Address.ofNat (w : Nat)
+
+def boolToWord (b : Bool) : Uint256 :=
+  if b then 1 else 0
+
+def isOwner : Contract Bool := do
+  let sender ← msgSender
+  let currentOwner ← getStorageAddr owner
+  return sender == currentOwner
+
+def onlyOwner : Contract Unit := do
+  let ownerCheck ← isOwner
+  require ownerCheck "Caller is not the owner"
+
+-- Constructor initializes owner and zeroes core counters.
+def constructor (initialOwner : Address) : Contract Unit := do
+  setStorageAddr owner initialOwner
+  setStorage totalSupply 0
+  setStorage nextTokenId 0
+
+-- Core ERC721 view helpers.
+def balanceOf (addr : Address) : Contract Uint256 := do
+  getMapping balances addr
+
+def ownerOf (tokenId : Uint256) : Contract Address := do
+  let ownerWord ← getMappingUint owners tokenId
+  return wordToAddress ownerWord
+
+def getApproved (tokenId : Uint256) : Contract Address := do
+  let approvedWord ← getMappingUint tokenApprovals tokenId
+  return wordToAddress approvedWord
+
+def isApprovedForAll (ownerAddr operator : Address) : Contract Bool := do
+  let flag ← getMapping2 operatorApprovals ownerAddr operator
+  return flag != 0
+
+-- Approve a specific address for a single tokenId.
+def approve (approved : Address) (tokenId : Uint256) : Contract Unit := do
+  let sender ← msgSender
+  let tokenOwner ← ownerOf tokenId
+  require (sender == tokenOwner) "Not token owner"
+  setMappingUint tokenApprovals tokenId (addressToWord approved)
+
+-- Set or clear global operator approval for sender.
+def setApprovalForAll (operator : Address) (approved : Bool) : Contract Unit := do
+  let sender ← msgSender
+  setMapping2 operatorApprovals sender operator (boolToWord approved)
+
+-- Owner-only mint with sequential token IDs.
+def mint (to : Address) : Contract Uint256 := do
+  onlyOwner
+  require (to != 0) "Invalid recipient"
+
+  let tokenId ← getStorage nextTokenId
+  let currentOwnerWord ← getMappingUint owners tokenId
+  require (currentOwnerWord == 0) "Token already minted"
+
+  let recipientBalance ← getMapping balances to
+  let newRecipientBalance ← requireSomeUint (safeAdd recipientBalance 1) "Balance overflow"
+
+  let currentSupply ← getStorage totalSupply
+  let newSupply ← requireSomeUint (safeAdd currentSupply 1) "Supply overflow"
+
+  setMappingUint owners tokenId (addressToWord to)
+  setMapping balances to newRecipientBalance
+  setStorage totalSupply newSupply
+  setStorage nextTokenId (add tokenId 1)
+  return tokenId
+
+-- Transfer token from owner to recipient with approval checks.
+def transferFrom (fromAddr to : Address) (tokenId : Uint256) : Contract Unit := do
+  let sender ← msgSender
+  require (to != 0) "Invalid recipient"
+
+  let ownerWord ← getMappingUint owners tokenId
+  require (ownerWord != 0) "Token does not exist"
+
+  let tokenOwner := wordToAddress ownerWord
+  require (tokenOwner == fromAddr) "From is not owner"
+
+  let approvedWord ← getMappingUint tokenApprovals tokenId
+  let operatorWord ← getMapping2 operatorApprovals fromAddr sender
+  let senderWord := addressToWord sender
+  let authorized := sender == fromAddr || approvedWord == senderWord || operatorWord != 0
+  require authorized "Not authorized"
+
+  if fromAddr == to then
+    pure ()
+  else
+    let fromBalance ← getMapping balances fromAddr
+    require (fromBalance >= 1) "Insufficient balance"
+    let toBalance ← getMapping balances to
+    let newToBalance ← requireSomeUint (safeAdd toBalance 1) "Balance overflow"
+    setMapping balances fromAddr (sub fromBalance 1)
+    setMapping balances to newToBalance
+
+  setMappingUint owners tokenId (addressToWord to)
+  setMappingUint tokenApprovals tokenId 0
+
+end Verity.Examples.ERC721