परिचय
यह अध्याय OpenZeppelin’s ERC-721 CVL specification के हमारे कोड वॉकथ्रू का चौथा भाग (4/5) है और यह safe mint और safe transfer ऑपरेशंस को फॉर्मली वेरीफाई (formally verifying) करने पर केंद्रित है, विशेष रूप से:
_safeMint()और_safeMint(bytes)safeTransferFrom()औरsafeTransferFrom(bytes)
_safeMint() फंक्शन एक अतिरिक्त चेक के साथ _mint() को एक्सटेंड करता है: यदि प्राप्तकर्ता (recipient) एक कॉन्ट्रैक्ट है, तो यह चेक करता है कि कॉन्ट्रैक्ट ERC-721 टोकन को हैंडल कर सकता है या नहीं। यह NFTs को उन कॉन्ट्रैक्ट्स में फंसने से रोकता है जिनमें ट्रांसफर लॉजिक नहीं होता है।
OpenZeppelin में ERC-721 के safeMint के दो वर्ज़न हैं: एक जो bytes data पैरामीटर लेता है, और दूसरा जो नहीं लेता है। सरल वर्ज़न (बिना bytes के) bytes वाले वर्ज़न को कॉल करता है, जिसमें data पैरामीटर के रूप में एक एम्प्टी स्ट्रिंग (empty string) पास की जाती है:
// ERC721.sol
function _safeMint(address to, uint256 tokenId) internal {
_safeMint(to, tokenId, "");
}
function _safeMint(address to, uint256 tokenId, bytes memory data) internal virtual {
_mint(to, tokenId);
ERC721Utils.checkOnERC721Received(_msgSender(), address(0), to, tokenId, data);
}
नोट: लाइब्रेरी ERC721Utils को यहाँ पाया जा सकता है।
दोनों वर्ज़न एड्रेस to पर एक NFT मिंट करते हैं, फिर प्राप्तकर्ता पर हुक फंक्शन onERC721Received() को कॉल करते हैं यदि वह एक कॉन्ट्रैक्ट है। bytes पैरामीटर वाला वर्ज़न अतिरिक्त रूप से प्राप्त करने वाले कॉन्ट्रैक्ट के onERC721Received हुक को data फॉरवर्ड करता है, जो प्राप्तकर्ता को दिए गए डेटा के आधार पर अपने व्यवहार को कस्टमाइज़ करने की अनुमति देता है। उदाहरण के लिए, एक गेम कॉन्ट्रैक्ट सीधे किसी खिलाड़ी के इन्वेंट्री कॉन्ट्रैक्ट में NFT को मिंट कर सकता है और गेम इवेंट्स को ट्रिगर करने के लिए आइटम टाइप, रेयरिटी (rarity), या प्रारंभिक एट्रिब्यूट्स को निर्दिष्ट करने वाला data शामिल कर सकता है।
दोनों वर्ज़न रिवर्ट (revert) हो जाते हैं और मिंट को अनडू (undo) कर देते हैं यदि:
- प्राप्तकर्ता
onERC721Received()को इम्प्लीमेंट नहीं करता है, - कॉलबैक रिवर्ट हो जाता है, या
- कॉलबैक अपेक्षित सेलेक्टर
0x150b7a02के अलावा कोई अन्य वैल्यू रिटर्न करता है।
प्राप्तकर्ता कॉन्ट्रैक्ट में इसके एक्सटर्नल कॉल को रिज़ॉल्व किए बिना _safeMint() को फॉर्मली वेरीफाई करना संभव नहीं है।
जब एक रूल में _safeMint() को इनवोक किया जाता है, तो यह checkOnERC721Received() को कॉल करता है, जो बदले में प्राप्तकर्ता कॉन्ट्रैक्ट पर onERC721Received() के लिए एक एक्सटर्नल कॉल करता है। Prover यह निर्धारित नहीं कर सकता कि onERC721Received() क्या करेगा, इसलिए यह कॉल को अनरिज़ॉल्व्ड (unresolved) मानता है। अनरिज़ॉल्व्ड एक्सटर्नल कॉल्स के कारण Prover स्टोरेज में आर्बिट्रेरी (मनमाने) बदलाव मान लेता है, जिसका अर्थ है कि पोस्ट-कॉल एशर्शन्स (assertions) में स्टोरेज वेरिएबल्स और घोस्ट (ghost) वेरिएबल्स नॉन-डिटरमिनिस्टिक वैल्यू लेते हैं, जिससे एशर्शन्स अर्थहीन हो जाते हैं।
एक्सटर्नल कॉल को रिज़ॉल्व करने के लिए, एक मॉक रिसीवर कॉन्ट्रैक्ट (mock receiver contract) जोड़ा जाता है जिसका onERC721Received फंक्शन 0x150b7a02 (this.onERC721Received.selector की वैल्यू) रिटर्न करता है।
// ERC721ReceiverHarness.sol -- this is a mock contract
import "contracts/interfaces/IERC721Receiver.sol";
contract ERC721ReceiverHarness is IERC721Receiver {
function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
return this.onERC721Received.selector; // always returns 0x150b7a02
}
}
हम एक्सटर्नल रिसीवर कॉन्ट्रैक्ट को वेरीफाई नहीं करते हैं क्योंकि इसका इम्प्लीमेंटेशन हमारे नियंत्रण से बाहर है। इसके बजाय, onERC721Received कॉल को एक मॉक रिसीवर कॉन्ट्रैक्ट पर डिस्पैच किया जाता है जो हमेशा अपेक्षित सेलेक्टर 0x150b7a02 रिटर्न करता है। इसका मतलब है कि स्पेसिफिकेशन उन केसेस का परीक्षण नहीं करता है जहां कॉलबैक रिवर्ट हो जाता है या गलत वैल्यू रिटर्न करता है।
हालाँकि, इसका मतलब यह नहीं है कि यदि रियल एग्जीक्यूशन में कॉलबैक फेल हो जाता है तो _safeMint() रिवर्ट नहीं होगा। लाइवनेस एशर्शन (liveness assertion) यह सुनिश्चित करता है कि ऐसे मामलों में फंक्शन रिवर्ट होकर सही ढंग से व्यवहार करे।
लाइवनेस एशर्शन कॉलबैक की रिटर्न वैल्यू का स्वयं निरीक्षण नहीं करता है; यह चेक करता है कि पूरा कॉल सफल हुआ या रिवर्ट हो गया। जैसा कि “Mint and Burn” अध्याय में चर्चा की गई है, मिंट रिवर्ट नहीं होता है (!lastReverted) यदि और केवल यदि ownerBefore == address(0) और to != address(0):
bool success = !lastReverted;
assert success <=> (ownerBefore == 0 && to != 0);
जब रिसीवर कॉलबैक एक रिवर्ट का कारण बनता है, तो राइट-हैंड-साइड (ownerBefore == 0 && to != 0) संतुष्ट रहता है क्योंकि इन वैल्यूज को कॉल से पहले कैप्चर किया गया था। हालाँकि, success फॉल्स (false) होता है, जो बाइकंडीशनल (biconditional) एशर्शन का उल्लंघन करता है। Prover इस विरोधाभास का पता लगाता है और एक वायलेशन की रिपोर्ट करता है। इसलिए, कॉलबैक रिटर्न वैल्यू को स्पष्ट रूप से चेक करने के लिए किसी अतिरिक्त एशर्शन की आवश्यकता नहीं है।
सेफ मिंट (safe mint) के साथ ऊपर चर्चा किया गया समान सिद्धांत सेफ टोकन ट्रांसफर्स (safe token transfers) पर भी लागू होता है।
safeTransferFrom के भी दो वर्ज़न हैं: एक जो bytes data पैरामीटर लेता है, और दूसरा जो नहीं लेता है:
// ERC721.sol
function safeTransferFrom(address from, address to, uint256 tokenId) public {
safeTransferFrom(from, to, tokenId, "");
}
function safeTransferFrom(address from, address to, uint256 tokenId, bytes memory data) public virtual {
transferFrom(from, to, tokenId);
ERC721Utils.checkOnERC721Received(_msgSender(), from, to, tokenId, data);
}
bytes पैरामीटर वाले वर्ज़न में, data को प्राप्त करने वाले कॉन्ट्रैक्ट के onERC721Received हुक पर फॉरवर्ड किया जाता है ताकि प्राप्तकर्ता ट्रांसफर के दौरान अतिरिक्त डेटा प्रोसेस कर सके। यदि प्राप्तकर्ता एक कॉन्ट्रैक्ट है जो onERC721Received को इम्प्लीमेंट नहीं करता है या अमान्य प्रतिक्रिया (invalid response) रिटर्न करता है, तो पूरा ट्रांजैक्शन रिवर्ट हो जाता है।
दोनों safeMint() और safeTransferFrom() एक ही एक्सटर्नल कॉल पैटर्न का पालन करते हैं, इसलिए स्पेसिफिकेशन इन फंक्शंस को वेरीफाई करते समय एक ही मॉक रिसीवर कॉन्ट्रैक्ट का उपयोग करता है।
safe mint को फॉर्मली वेरीफाई करना
चूंकि _safeMint() और _safeMint(bytes) इंटरनल फंक्शंस हैं, OpenZeppelin उन्हें हार्नेस (harness) फंक्शंस के माध्यम से एक्सपोज़ करता है जिन्हें Prover इनवोक कर सकता है:
// ERC721Harness.sol
function safeMint(address to, uint256 tokenId) external {
_safeMint(to, tokenId);
}
function safeMint(address to, uint256 tokenId, bytes memory data) external {
_safeMint(to, tokenId, data);
}
नीचे दिया गया safeMint रूल method f का उपयोग करता है, जो आर्बिट्रेरी फंक्शन कॉल है, उसी तरह जैसे पैरामेट्रिक रूल्स करते हैं। टिपिकल पैरामेट्रिक रूल्स में, फंक्शन और आर्गुमेंट्स दोनों आर्बिट्रेरी होते हैं (f(e, args))। यहाँ, filtered ब्लॉक method f को केवल दो safeMint वेरिएंट्स तक सीमित करता है, और आर्गुमेंट्स to और tokenId को args का उपयोग करने के बजाय स्पष्ट रूप से डिक्लेयर किया गया है। यह स्पष्ट डिक्लेरेशन रूल को पूर्व-शर्तें (preconditions) लागू करने की अनुमति देता है जो इन आर्गुमेंट्स को कंस्ट्रेन (constrain) करती हैं, जिसे सीधे calldataarg args कंस्ट्रक्ट के भीतर नहीं किया जा सकता है। इसका मतलब है कि फंक्शन एक अनुमत सेट (allowed set) के भीतर आर्बिट्रेरी है, जबकि आर्गुमेंट्स नियंत्रित हैं, जो एक फुल पैरामेट्रिक पैटर्न से अलग है।
यहाँ रूल दिया गया है, जिसे हम आगे समझेंगे:
// ERC721.spec -- safeMint
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
} {
require nonpayable(e);
// requireInvariant notMintedUnset(tokenId);
uint256 otherTokenId;
address otherAccount;
require balanceLimited(to);
mathint supplyBefore = _supply;
uint256 balanceOfToBefore = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore = unsafeOwnerOf(tokenId);
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
helperMintWithRevert@withrevert(e, f, to, tokenId);
bool success = !lastReverted;
assert success <=> (
ownerBefore == 0 &&
to != 0
);
// effect
assert success => (
_supply == supplyBefore + 1 &&
to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
unsafeOwnerOf(tokenId) == to
);
// no side effect
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to;
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
}
method f को safeMint वेरिएंट्स पर फ़िल्टर करना
method f पैरामीटर Prover को आर्बिट्रेरी फंक्शंस का परीक्षण करने के लिए कहता है, लेकिन filtered क्लॉज़ (clause) परीक्षण को केवल safeMint के दो वर्ज़न्स तक सीमित करता है:
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
} {
...
helperMintWithRevert@withrevert(e, f, to, tokenId);
...
}
एक ही रूल के भीतर दोनों वेरिएंट्स को हैंडल करने के लिए, हम एक हेल्पर फंक्शन helperMintWithRevert का उपयोग करते हैं जो फंक्शन सेलेक्टर के आधार पर कॉल को उपयुक्त वर्ज़न पर रूट करता है:
function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
if (f.selector == sig:safeMint(address,uint256).selector) {
safeMint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
bytes params;
require params.length < 0xffff;
safeMint(e, to, tokenId, params);
} else {
require false;
}
}
हेल्पर फंक्शन रूल को method f का उपयोग करके एक ही रूल के भीतर safeMint() और safeMint(bytes) दोनों का परीक्षण करने की अनुमति देता है, इसलिए प्रत्येक वेरिएंट के लिए अलग रूल लिखने की कोई आवश्यकता नहीं है। यह फंक्शन सेलेक्टर के आधार पर कॉल को रूट करता है और एग्जीक्यूशन को संबंधित if/else ब्रांच की ओर निर्देशित करता है।
आइए प्रत्येक कंडीशन को स्पष्ट करें:
-
f.selector == sig:safeMint(address,uint256).selectorयदि आर्बिट्रेरी मेथड कॉल दो-पैरामीटर वाला
safeMint(address,uint256)है, तो CVL हेल्पर फंक्शनsafeMint(e, to, tokenId)को इनवोक करता है। -
f.selector == sig:safeMint(address,uint256,bytes).selectorयदि आर्बिट्रेरी मेथड कॉल तीन-पैरामीटर वाला
safeMint(address, uint256, bytes)है, तो CVL हेल्पर फंक्शनsafeMint(e, to, tokenId, params)को इनवोक करता है, जहाँparamsकोrequire params.length < 0xffffके माध्यम से0xffff( या 65,535 बाइट्स) से कम तक कंस्ट्रेन (constrain) किया गया है।चूंकि
bytesएक डायनामिकली-साइज़्ड ऐरे है,require params.length <0xffffएक व्यावहारिक वेरिफिकेशन सीमा है — जोsafeMintडेटा पैरामीटर के लिए यथार्थवादी यूज़ केसेस को कवर करने के लिए पर्याप्त बड़ी है, लेकिन Prover को अवास्तविक रूप से बड़े इनपुट्स को एक्सप्लोर करने से रोकने के लिए पर्याप्त छोटी है। -
else { require false; }इस ब्रांच को केवल कैच-ऑल (catch-all) के रूप में शामिल किया गया है, लेकिन इस रूल में यहाँ तक पहुँचना संभव नहीं है (unreachable) क्योंकि
filteredक्लॉज़ पहले से हीmethod fको दोsafeMintवेरिएंट्स तक सीमित करता है। Prover कोई अन्य फंक्शन सेलेक्टर सप्लाई नहीं कर सकता है, इसलिएelseब्लॉक केवल एक सैद्धांतिक केस को कवर करता है जो फ़िल्टर्ड रूल के तहत नहीं हो सकता है।
नोट: मूल OpenZeppelin स्पेसिफिकेशन में, इस हेल्पर helperMintWithRevert में mint(address,uint256) के लिए एक ब्रांच भी शामिल थी, लेकिन उस केस को रूल में filtered क्लॉज़ द्वारा पहले ही हटा दिया गया है। चूंकि रूल केवल safeMint() और safeMint(bytes) की अनुमति देता है, हमने स्पष्टता के लिए बिना उपयोग वाली ब्रांच को हटा दिया। संदर्भ के लिए, यहाँ मूल helperMintWithRevert कोड है।
onERC721Received को मॉक रिसीवर पर डिस्पैच करना
Prover को वेरिफिकेशन सीन में किसी भी कॉन्ट्रैक्ट (वाइल्डकार्ड _ द्वारा निरूपित) पर कॉल डिस्पैच करने का निर्देश देने के लिए methods ब्लॉक में DISPATCHER जोड़ा गया है, जो निर्दिष्ट मेथड (onERC721Received) को इम्प्लीमेंट करता है:
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
चूंकि केवल मॉक रिसीवर ही इस मेथड को इम्प्लीमेंट करता है, इसलिए कॉलबैक हमेशा इसी पर डिस्पैच होता है। यदि एक से अधिक कॉन्ट्रैक्ट्स ने onERC721Received को इम्प्लीमेंट किया होता, तो Prover उनमें से प्रत्येक पर डिस्पैच करता और सभी वेरिफिकेशन पाथ्स का एक्सप्लोर करता।
इसके बिना, Prover onERC721Received कॉल को अनरिज़ॉल्व्ड (unresolved) मानता है। परिणामस्वरूप, Prover ऐसे काउंटर-एग्जांपल्स (counterexamples) उत्पन्न करता है जो safeMint और safeTransferFrom रूल्स में अनरिज़ॉल्व्ड एक्सटर्नल कॉल के कारण एशर्शन्स का उल्लंघन करते हैं।
डिस्पाची (Dispatchee) — मॉक रिसीवर कॉन्ट्रैक्ट
डिस्पाची (dispatchee) सीन में वह कॉन्ट्रैक्ट होता है जो डिस्पैच कॉल का लक्ष्य होता है। सीन में कम से कम एक कॉन्ट्रैक्ट होना चाहिए जो onERC721Received को इम्प्लीमेंट करता हो। निम्नलिखित कॉन्ट्रैक्ट इस उद्देश्य के लिए एक न्यूनतम डिस्पाची प्रदान करता है:
contract ERC721ReceiverHarness is IERC721Receiver {
function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
return this.onERC721Received.selector;
}
}
यह IERC721Receiver इंटरफ़ेस का एक न्यूनतम इम्प्लीमेंटेशन है। यह किसी भी आने वाले ERC721 टोकन को स्वीकार करता है और एक सफल ट्रांसफर का संकेत देने के लिए अपेक्षित सेलेक्टर (0x150b7a02) रिटर्न करता है। हालाँकि यह कोई अतिरिक्त लॉजिक परफॉर्म नहीं करता है, यह Prover को onERC721Received के लिए एक वैध डिस्पाची देता है।
पूर्ण स्पेसिफिकेशन (Full specification) — safeMint
एशर्शन्स पूरी तरह से “Mint and Burn” अध्याय के mint रूल के समान हैं, जहाँ liveness, effect और no side-effect चेक को विस्तार से समझाया गया है। इस कारण से, हम यहाँ इस चर्चा को नहीं दोहराते हैं और अधिक स्पष्टीकरण के लिए पाठकों को उस अध्याय का संदर्भ लेने का सुझाव देते हैं।
नीचे safeMint के लिए संपूर्ण CVL स्पेसिफिकेशन दिया गया है:
methods {
function balanceOf(address) external returns (uint256) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helpers │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
if (f.selector == sig:safeMint(address,uint256).selector) {
// safeMint@withrevert(e, to, tokenId);
safeMint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
bytes params;
require params.length < 0xffff;
// safeMint@withrevert(e, to, tokenId, params);
safeMint(e, to, tokenId, params);
} else {
require false;
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _supply {
init_state axiom _supply == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: safeMint behavior and side effects │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
} {
require nonpayable(e);
// requireInvariant notMintedUnset(tokenId);
uint256 otherTokenId;
address otherAccount;
require balanceLimited(to);
mathint supplyBefore = _supply;
uint256 balanceOfToBefore = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore = unsafeOwnerOf(tokenId);
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
helperMintWithRevert@withrevert(e, f, to, tokenId);
bool success = !lastReverted;
// liveness
assert success <=> (
ownerBefore == 0 &&
to != 0
);
// effect
assert success => (
_supply == supplyBefore + 1 &&
to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
unsafeOwnerOf(tokenId) == to
);
// no side effect
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to;
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
}
नोट: वर्ज़न 8.1.0 में पेश किया गया एक नया Prover फीचर CVL फंक्शंस को @withRevert का उपयोग करने की अनुमति देता है। यह फंक्शन के अंदर सिंटैक्स को बदल देता है: प्रत्येक मेथड इनवोकेशन पर @withRevert रखने के बजाय, यह अब CVL फंक्शन पर लागू होता है। हमने सिंटैक्स को अपडेट कर दिया है ताकि यह नवीनतम Prover वर्ज़न के साथ काम करे।
यहाँ Prover रन है: लिंक
safe transferFrom को फॉर्मली वेरीफाई करना
कॉन्ट्रैक्ट फंक्शन safeTransferFrom() onERC721Received सेफ्टी चेक के साथ transferFrom() को एक्सटेंड करता है। इसलिए, safeTransferFrom रूल की पूर्व-शर्तें (preconditions), प्री-कॉल स्टेट और एशर्शन्स पिछले अध्याय के transferFrom रूल के समान हैं, लेकिन यह safeMint के समान ही मेथड एग्जीक्यूशन पैटर्न का पालन करता है:
- यह दोनों वेरिएंट्स का परीक्षण करने के लिए फ़िल्टरिंग के साथ
method fका उपयोग करता है, - एक CVL हेल्पर फंक्शन के माध्यम से एग्जीक्यूशन को रूट करता है, और
onERC721Received()को मॉक रिसीवर पर डिस्पैच करता है।
यहाँ रूल है। safeMint की तरह, हम इस बात पर ध्यान केंद्रित करते हैं कि मेथड फ़िल्टरिंग, हेल्पर फंक्शन रूटिंग, और एक्सटर्नल कॉलबैक हैंडलिंग का उपयोग दोनों safeTransferFrom वेरिएंट्स को वेरीफाई करने के लिए कैसे किया जाता है:
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
require nonpayable(e);
require authSanity(e);
address operator = e.msg.sender;
uint256 otherTokenId;
address otherAccount;
requireInvariant ownerHasBalance(tokenId);
require balanceLimited(to);
uint256 balanceOfFromBefore = balanceOf(from);
uint256 balanceOfToBefore = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore = unsafeOwnerOf(tokenId);
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
address approvalBefore = unsafeGetApproved(tokenId);
address otherApprovalBefore = unsafeGetApproved(otherTokenId);
helperTransferWithRevert@withrevert(e, f, from, to, tokenId);
bool success = !lastReverted;
assert success <=> (
from == ownerBefore &&
from != 0 &&
to != 0 &&
(operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
);
// effect
assert success => (
to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) &&
to_mathint(balanceOf(to)) == balanceOfToBefore + assert_uint256(from != to ? 1: 0) &&
unsafeOwnerOf(tokenId) == to &&
unsafeGetApproved(tokenId) == 0
);
// no side effect
assert balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId;
}
method f को safeTransferFrom वेरिएंट्स पर फ़िल्टर करना
rule safeTransferFrom एग्जीक्यूशन को दो मेथड्स (method f के माध्यम से) तक सीमित करता है, जो हैं:
safeTransferFrom(address, address, uint256)safeTransferFrom(address, address, uint256, bytes)
इसके बाद यह कॉल को CVL फंक्शन helperTransferWithRevert() में पास करता है जैसा कि नीचे दिखाया गया है:
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
...
helperTransferWithRevert@withrevert(e, f, from, to, tokenId);
bool success = !lastReverted;
...
}
हमारे पास safeTransferFrom() के लिए अलग कंडीशनल लॉजिक है — एक bytes पैरामीटर वाले वेरिएंट के लिए और एक बिना इसके।
bytes वाले वेरिएंट के लिए, हम ऐरे को एक व्यावहारिक सीमा के भीतर रखने और एक्सप्लोरेशन स्पेस को सीमित करने के लिए bytes पैरामीटर की लंबाई को 0xffff से कम तक कंस्ट्रेन करते हैं। इस कंस्ट्रेंट के अलावा, दोनों safeTransferFrom() वेरिएंट समान लॉजिक का पालन करते हैं और समान रूल स्ट्रक्चर का उपयोग करते हैं:
function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
bytes params;
require params.length < 0xffff;
safeTransferFrom(e, from, to, tokenId, params);
} else {
calldataarg args;
f(e, args);
}
}
नोट: safeMint रूल की तरह, f.selector == sig:transferFrom(address,address,uint256).selector कंडीशनल ब्रांच को इस CVL फंक्शन से हटा दिया गया था क्योंकि यह अनावश्यक है। रूल पहले से ही safeTransferFrom() और safeTransferFrom(bytes) को छोड़कर अन्य सभी फंक्शंस को फ़िल्टर कर देता है। संदर्भ के लिए, यहाँ मूल helperTransferWithRevert कोड है: लिंक
onERC721Received कॉलबैक को डिस्पैच करना
safeMint अनुभाग में, हमने मॉक रिसीवर और DISPATCHER(true) सेटअप कॉन्फ़िगर किया है ताकि Prover एक्सटर्नल कॉलबैक onERC721Received को मॉडल कर सके।
यहाँ भी उसी सेटअप की आवश्यकता है क्योंकि safeMint और safeTransferFrom दोनों एक ERC-721 रिसीवर के लिए एक्सटर्नल कॉल को ट्रिगर करते हैं। इस डिस्पैच कॉन्फ़िगरेशन के बिना, Prover कॉलबैक को एक अनरिज़ॉल्व्ड एक्सटर्नल कॉल के रूप में मानेगा, जो अव्यवस्था (havoc) का कारण बनता है और पोस्ट-कॉल एशर्शन्स को अर्थहीन बना देता है।
पूर्ण स्पेसिफिकेशन (Full specification) — safeTransferFrom
एशर्शन्स पिछले अध्याय, “Transfer and Approval” के transferFrom रूल के समान हैं, जहाँ liveness, effect, और no side-effect चेक को विस्तार से समझाया गया है।
नीचे safeTransferFrom के लिए संपूर्ण CVL स्पेसिफिकेशन दिया गया है:
methods {
function balanceOf(address) external returns (uint256) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function unsafeGetApproved(uint256) external returns (address) envfree;
function isApprovedForAll(address,address) external returns (bool) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition authSanity(env e) returns bool = e.msg.sender != 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helpers │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
// safeTransferFrom@withrevert(e, from, to, tokenId);
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
bytes params;
require params.length < 0xffff;
// safeTransferFrom@withrevert(e, from, to, tokenId, params);
safeTransferFrom(e, from, to, tokenId, params);
} else {
calldataarg args;
f@withrevert(e, args);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: safeTransferFrom behavior and side effects │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
require nonpayable(e);
require authSanity(e);
address operator = e.msg.sender;
uint256 otherTokenId;
address otherAccount;
// requireInvariant ownerHasBalance(tokenId);
require balanceLimited(to);
uint256 balanceOfFromBefore = balanceOf(from);
uint256 balanceOfToBefore = balanceOf(to);
uint256 balanceOfOtherBefore = balanceOf(otherAccount);
address ownerBefore = unsafeOwnerOf(tokenId);
address otherOwnerBefore = unsafeOwnerOf(otherTokenId);
address approvalBefore = unsafeGetApproved(tokenId);
address otherApprovalBefore = unsafeGetApproved(otherTokenId);
helperTransferWithRevert@withrevert(e, f, from, to, tokenId);
bool success = !lastReverted;
// liveness
assert success <=> (
from == ownerBefore &&
from != 0 &&
to != 0 &&
(operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
);
// effect
assert success => (
to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) &&
to_mathint(balanceOf(to)) == balanceOfToBefore + assert_uint256(from != to ? 1: 0) &&
unsafeOwnerOf(tokenId) == to &&
unsafeGetApproved(tokenId) == 0
);
// no side effect
assert balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId;
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId;
}
नोट: वर्ज़न 8.1.0 में पेश किया गया एक नया Prover फीचर CVL फंक्शंस को @withRevert का उपयोग करने की अनुमति देता है। यह फंक्शन के अंदर सिंटैक्स को बदल देता है: प्रत्येक मेथड इनवोकेशन पर @withRevert रखने के बजाय, यह अब CVL फंक्शन पर लागू होता है। हमने सिंटैक्स को अपडेट कर दिया है ताकि यह नवीनतम Prover वर्ज़न के साथ काम करे।
यहाँ Prover रन है।
यह लेख Certora Prover का उपयोग करके फॉर्मल वेरिफिकेशन (formal verification using the Certora Prover) पर एक श्रृंखला का हिस्सा है।