Contracts: add safeTransferFrom to ERC-721 implementation

[Th0rgal]

Summary

The ERC-721 contract in Contracts/ERC721/ERC721.lean is missing safeTransferFrom, which is required for full ERC-721 compliance (EIP-721). This is a contract-level change only — all needed EDSL primitives already exist.

Current ERC-721 surface

Implemented: balanceOf, ownerOf, getApproved, isApprovedForAll, approve, setApprovalForAll, mint, transferFrom

Missing: safeTransferFrom(from, to, tokenId), safeTransferFrom(from, to, tokenId, data)

Implementation

safeTransferFrom = transferFrom + recipient contract check:

1. Call transferFrom(from, to, tokenId) (already implemented)
2. Check if to is a contract (extcodesize(to) > 0) — extcodesize already exists as an Expr
3. If contract, call onERC721Received(operator, from, tokenId, data) on to — achievable via ecmCall / Calls.withReturn ECM
4. Require return value equals selector 0x150b7a02

Both overloads (with and without data parameter) should be implemented.

Proof considerations

The transferFrom portion has existing proofs (ownership transfer, approval checks). The onERC721Received callback is an external call — it should be:

• A local_obligation at the proof level (the callback's behavior is outside the single-contract model)
• Tested via Foundry (receiver contract that returns correct/incorrect selector)

Definition of done

• safeTransferFrom(from, to, tokenId) implemented in Contracts/ERC721/ERC721.lean
• safeTransferFrom(from, to, tokenId, data) implemented (overload with bytes data)
• extcodesize check for contract recipients
• onERC721Received callback via ECM for contract recipients
• Callback declared as local_obligation
• Foundry tests: transfer to EOA succeeds, transfer to compliant contract succeeds, transfer to non-compliant contract reverts
• Existing ERC-721 proofs still pass
• safeTransferFrom inherits transferFrom proof properties (ownership transfer, approval checks)