परिचय (Introduction)
पिछले अध्यायों में, हमने जाना कि CVL invariants कैसे काम करते हैं: ऐसे गुण (properties) जिन्हें कॉन्ट्रैक्ट के निष्पादन (execution) के दौरान हमेशा सत्य रहना चाहिए। Invariants नियमों (rules) में preconditions के रूप में और अन्य invariants में preserved स्थितियों के रूप में कार्य कर सकते हैं, जो वेरिफिकेशन को पहले से साबित हो चुकी गारंटियों पर निर्भर होने की अनुमति देता है और गलत धारणाओं (flawed assumptions) के जोखिम को दूर करता है। Invariants सभी स्टेट बदलने वाले (state-changing) फ़ंक्शन्स पर स्वचालित रूप से चेक किए जाते हैं।
यह अध्याय OpenZeppelin’s ERC-721 CVL specification के कोड वॉकथ्रू के भाग (2/5) के रूप में जारी है और invariant गुणों पर केंद्रित है। यह निम्नलिखित पांच ERC-721 invariants को वेरिफाई करता है:
-
balanceOfConsistencyएक उपयोगकर्ता का बैलेंस और ओनरशिप काउंट हमेशा बराबर होते हैं।
-
ownerHasBalanceटोकन ओनर्स (मालिकों) का बैलेंस हमेशा पॉजिटिव होता है।
-
ownedTotalIsSumOfBalancesस्वामित्व वाले टोकन की कुल संख्या (owned total) सभी उपयोगकर्ताओं के बैलेंस के योग (sum) के बराबर होती है।
-
notMintedUnsetअनमिंट किए गए (Unminted) टोकन के लिए कोई अप्रूव्ड (approved) एड्रेस सेट नहीं होता है।
-
zeroAddressHasNoApprovedOperatorअनमिंट किए गए टोकन के लिए कोई अप्रूव्ड ऑपरेटर (operator) नहीं होता है।
ये invariants गारंटी देते हैं कि बैलेंस स्वामित्व (ownership) को सटीक रूप से दर्शाते हैं और अप्रूवल स्वामित्व की स्थिति के अनुरूप रहते हैं।
balanceOfConsistency invariant
ERC-721 में, किसी अकाउंट का टोकन बैलेंस निर्धारित करने के तीन तरीके हैं:
- पब्लिक
balanceOf(address)फ़ंक्शन को कॉल करके _balancesमैपिंग से पढ़कर- स्टोरेज
_ownersमैपिंग से पढ़कर और एड्रेस के स्वामित्व वाले टोकन की गिनती करके
ये तीनों मात्राएं (quantities) बराबर होनी चाहिए क्योंकि वे सभी एक ही अंतर्निहित (underlying) तथ्य को दर्शाती हैं: उपयोगकर्ता के पास कितने टोकन हैं। कोई भी विसंगति (discrepancy) बैलेंस और ओनरशिप ट्रैकिंग के बीच असंगत अकाउंटिंग का संकेत देगी।
Invariant balanceOfConsistency में, ये मात्राएं balanceOf(user), _balances[user], और _ownedByUser[user] से मेल खाती हैं, जिनमें से प्रत्येक उपयोगकर्ता के टोकन बैलेंस को दर्शाता है:
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user]
...
प्रत्येक बैलेंस प्रस्तुतीकरण को कैसे प्राप्त किया जाता है
इस invariant को वेरिफाई करने के लिए, स्पेसिफिकेशन इनमें से प्रत्येक प्रस्तुतीकरण (representation) को कैप्चर करता है। निम्नलिखित स्पष्ट करता है कि प्रत्येक को कैसे प्राप्त (derive) किया जाता है।
balanceOf(user) — उपयोगकर्ता के बैलेंस का पब्लिक व्यू फ़ंक्शन
balanceOf(user) एक पब्लिक व्यू फ़ंक्शन है जिसे हम उपयोगकर्ता का बैलेंस प्राप्त करने के लिए CVL में सीधे कॉल कर सकते हैं। यह फ़ंक्शन स्टोरेज मैपिंग वेरिएबल _balances में स्टोर की गई वैल्यू लौटाता है।
_balances[user] — स्टोरेज से मिरर किए गए टोकन बैलेंस
_balances[user] एक ghost वेरिएबल है जो Sload हुक (hook) के माध्यम से प्राइवेट स्टोरेज मैपिंग वेरिएबल _balances को पढ़ता और मिरर करता है।
इसे forall क्वांटिफायर के साथ एक init_state एक्सीओम (axiom) का उपयोग करके सभी एड्रेसेस के लिए शून्य पर इनिशियलाइज़ किया जाता है, जो यह बताता है कि प्रत्येक एड्रेस प्रारंभिक स्टेट में शून्य बैलेंस के साथ शुरू होता है, जो कॉन्ट्रैक्ट के डिफ़ॉल्ट स्टोरेज स्टेट से मेल खाता है:
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
...
इस इनिशियलाइज़ेशन के बिना, Prover बैलेंस के लिए मनमाने शुरुआती मान (बेस केस) मान लेता है, जिससे प्रारंभिक स्टेट से ही गलत अकाउंटिंग हो सकती है। यह ट्रैकिंग लॉजिक को अमान्य कर देता है और वेरिफिकेशन के दौरान फॉल्स पॉजिटिव (false positive) उल्लंघन का कारण बनता है।
इनिशियलाइज़ेशन के बाद, स्पेसिफिकेशन को Sload हुक का उपयोग करके ghost स्टेट में स्टोरेज रीड्स को प्रतिबिंबित करना चाहिए। Sload हुक वास्तविक _balances स्टोरेज स्लॉट से वैल्यूज़ पढ़ता है और उन वैल्यूज़ को ghost वेरिएबल के साथ सिंक करता है (ghost और स्टोरेज वेरिएबल का नाम समान है लेकिन वे परस्पर विरोधी नहीं हैं):
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);
}
यह सिंक तब होता है जब Sload हुक द्वारा लौटाई गई स्टोरेज वैल्यू को require के माध्यम से ghost वेरिएबल के बराबर होने के लिए बाध्य (constrained) किया जाता है। यह सिंक आवश्यक है क्योंकि स्टोरेज रीड्स पर ghost वेरिएबल्स स्वचालित रूप से अपडेट नहीं होते हैं।
_ownedByUser[user] — स्टोरेज से प्राप्त टोकन ओनरशिप काउंट
_ownedByUser[user] एक ghost वेरिएबल है जो उन सभी tokenId की संख्या को दर्शाता है जिनके लिए ownerOf(tokenId) == user है:
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
...
दूसरे शब्दों में, यदि हम सभी टोकनों को सूचीबद्ध करते हैं और गिनते हैं कि user के पास कितने हैं, तो हमें _ownedByUser[user] प्राप्त होता है। हम ऐसा परिदृश्य (scenario) नहीं चाहते जहाँ balanceOf(user) 2 रिपोर्ट करे, लेकिन वास्तविक ओनरशिप काउंट 3 हो (उदाहरण के लिए, यदि ownerOf(token1) == user, ownerOf(token2) == user, और ownerOf(token3) == user हो)।
Ghost वेरिएबल _ownedByUser[user] Sstore हुक के माध्यम से यह स्टोर करता है कि एक उपयोगकर्ता के पास कितने टोकन हैं। यह हुक तब चलता है जब कॉन्ट्रैक्ट अपनी प्राइवेट स्टोरेज मैपिंग _owners[tokenId] में एक नई वैल्यू लिखता है, और यह ओनरशिप में हुए बदलाव को निर्धारित करने के लिए oldOwner और newOwner दोनों को ऑब्जर्व करता है।
इन दो वैल्यूज़ की तुलना करके, हम इस अपडेट को मिंट, बर्न या ट्रांसफर के रूप में वर्गीकृत कर सकते हैं:
- Mint:
oldOwner == address(0)औरnewOwner != address(0) - Burn:
oldOwner != address(0)औरnewOwner == address(0) - Transfer:
oldOwnerऔरnewOwnerदोनों गैर-शून्य (nonzero) एड्रेस हैं
हुक इन ओनरशिप परिवर्तनों को दर्शाने के लिए ghost मैपिंग _ownedByUser को अपडेट करता है:
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
नोट: हमने जानबूझकर लाइन _ownedTotal = ... को कमेंट आउट किया है क्योंकि अभी इसकी आवश्यकता नहीं है। हम स्वामित्व वाले टोकनों की कुल संख्या को ट्रैक नहीं कर रहे हैं; हम केवल प्रत्येक व्यक्तिगत उपयोगकर्ता के स्वामित्व वाले टोकनों को ट्रैक कर रहे हैं।
Sstore हुक _owners में पहली लाइन टोकन वृद्धि (increment) को संभालती है, जिसका अर्थ है कि मिंट और ट्रांसफर होता है:
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
- यदि
newOwner != 0है, तोnewOwnerटोकन काउंट में 1 जोड़ा जाता है। यह इन पर लागू होता है:- Mint: जब एक टोकन बनाया जाता है और किसी उपयोगकर्ता को असाइन किया जाता है (
address(0)सेnewOwner) - Transfer: जब एक टोकन एक उपयोगकर्ता से दूसरे उपयोगकर्ता के पास जाता है (
oldOwnerसेnewOwner)
- Mint: जब एक टोकन बनाया जाता है और किसी उपयोगकर्ता को असाइन किया जाता है (
- यदि
newOwner == 0है, तो यह एक बर्न को दर्शाता है, इसलिए किसी भीnewOwnerको टोकन प्राप्त नहीं होता है। टर्नरी एक्सप्रेशन (ternary expression) का मान 0 होता है, इसलिए कोई जोड़ (addition) नहीं होता है। हालाँकि, उस टोकन लॉस (बर्न) को अभी भी गिना जाना चाहिए, और इसे दूसरी लाइन द्वारा संभाला जाता है।
Sstore हुक _owners में दूसरी लाइन टोकन कमी (decrement) को संभालती है, जिसका अर्थ है कि बर्न और ट्रांसफर (भी) होता है:
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
- यदि
oldOwner != 0है, तो पिछला (nonzero) ओनर टोकन रखता था और अब उसे खो देता है, इसलिए हम 1 घटाते हैं। यह ट्रांसफर और बर्न दोनों ऑपरेशन्स पर लागू होता है। - यदि
oldOwner == 0है, तो यह एक मिंट को दर्शाता है, जहाँ टोकन नए सिरे से बनाया गया है और इसका कोई पिछला मालिक नहीं है। टर्नरी का मान 0 होता है, इसलिए कोई घटाव (subtraction) नहीं होता है। ओनरशिप काउंट को इसके बजाय पहली लाइन में संभाला जाता है — वह लाइन जो टोकन वृद्धि को संभालती है।
अब जब हमने invariant एक्सप्रेशन और उपयोगकर्ता के टोकन बैलेंस के तीन प्रस्तुतीकरण (representations) कैसे प्राप्त किए जाते हैं, इस पर चर्चा कर ली है, तो स्पेसिफिकेशन को पूरा करने के लिए एक अंतिम हिस्सा बचा है: सेफ मिंट और सेफ ट्रांसफर ऑपरेशन्स से एक्सटर्नल कॉलबैक को संभालना।
Invariants वेरिफिकेशन के दौरान स्वचालित रूप से सभी स्टेट बदलने वाले फ़ंक्शन्स को इनवोक (invoke) करते हैं, जिसका अर्थ है कि Prover safeMint() और safeTransferFrom() को कॉल करता है — जो दोनों प्राप्तकर्ता कॉन्ट्रैक्ट (recipient contract) पर onERC721Received() के लिए एक्सटर्नल कॉलबैक ट्रिगर करते हैं। हमें यह कॉन्फ़िगर करने की आवश्यकता है कि Prover इस एक्सटर्नल कॉल को कैसे संभालता है। अन्यथा, इन एक्सटर्नल कॉल्स को Prover द्वारा अनसुलझा (unresolved) माना जाता है, जो ghost वेरिएबल्स और स्टोरेज पर havoc (तबाही/अराजकता) का कारण बनता है, और invariant प्रॉपर्टी के फॉल्स-पॉजिटिव उल्लंघनों की ओर ले जाता है।
DISPATCHER — onERC721Received कॉलबैक को हल करना
इस कॉलबैक को हल करने के लिए, स्पेसिफिकेशन onERC721Received() कॉल को एक मॉक रिसीवर कॉन्ट्रैक्ट (mock receiver contract) पर डिस्पैच करता है जो ERC-721 सपोर्ट का संकेत देने के लिए bytes4 सिलेक्टर 0x150b7a02 लौटाता है। इस डिस्पैच को लागू करने के लिए, हमें निम्नलिखित करने की आवश्यकता है:
- एक साधारण ERC721 रिसीवर कॉन्ट्रैक्ट (मॉक) बनाना,
- इसे वेरिफिकेशन scene में शामिल करना,
methodsब्लॉक में एक डिस्पैच निर्देश (instruction) जोड़ना।
ERC721 मॉक रिसीवर कॉन्ट्रैक्ट:
यहाँ रिसीवर कॉन्ट्रैक्ट है, जिसे एक harness के रूप में लागू किया गया है जो bytes4 सिलेक्टर 0x150b7a02 लौटाता है:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
import "contracts/interfaces/IERC721Receiver.sol";
contract ERC721ReceiverHarness is IERC721Receiver {
function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
return this.onERC721Received.selector;
}
}
नोट__: IERC721Receiver को इम्पोर्ट करना एक इंटरफेस चेक के रूप में कार्य करता है, जो यह पुष्टि करता है कि कॉन्ट्रैक्ट अपेक्षित ERC721 रिसीवर स्पेसिफिकेशन के अनुरूप है।
सीन (scene) में मॉक रिसीवर कॉन्ट्रैक्ट जोड़ें:
इसके बाद, हम .conf कॉन्फ़िगरेशन फ़ाइल में ERC721ReceiverHarness.sol जोड़कर इसे सीन में शामिल करते हैं:
// .conf
{
"files": [
"certora/harness/ERC721Harness.sol",
"certora/harness/ERC721ReceiverHarness.sol",
],
...
}
इस बिंदु पर, मॉक रिसीवर वेरिफिकेशन सीन का हिस्सा है और डिस्पैच लक्ष्य के रूप में उपलब्ध है।
DISPATCH निर्देश जोड़ें:
फिर, CVL स्पेसिफिकेशन के methods ब्लॉक में, हम डिस्पैच निर्देश जोड़ते हैं:
// .spec
methods {
function balanceOf(address) external returns (uint256) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
डिस्पैच लाइन: function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true) Prover को निर्देश देती है कि वह onERC721Received() कॉल्स को वेरिफिकेशन सीन के उन सभी कॉन्ट्रैक्ट्स (_ एक वाइल्डकार्ड है) में रूट करे जो onERC721Received() को लागू करते हैं और balanceOfConsistency invariant के विरुद्ध इसके कार्यान्वयन (implementation) का परीक्षण करें। चूँकि हमारे पास केवल एक कॉन्ट्रैक्ट है जो onERC721Received को लागू करता है, जो कि मॉक रिसीवर है, इसलिए यह एकमात्र कॉन्ट्रैक्ट है जिसका Prover परीक्षण करेगा।
DISPATCHER(true) के साथ, डिस्पैच के लिए केवल सीन में मौजूद कॉन्ट्रैक्ट्स का चयन किया जाता है, और Prover प्रत्येक मिलान (matching) वाले कार्यान्वयन का परीक्षण करके यह निर्धारित करने का प्रयास करता है कि क्या कोई उल्लंघन का कारण बन सकता है।
यहाँ उपयोग किया गया मॉक रिसीवर कॉन्ट्रैक्ट जानबूझकर न्यूनतम रखा गया है। यह केवल onERC721Received() फ़ंक्शन को लागू करता है और आवश्यक सिलेक्टर 0x150b7a02 लौटाता है। इसमें ऐसा कोई लॉजिक नहीं है जो कॉलिंग कॉन्ट्रैक्ट के स्टेट को बदलता है या स्टोरेज को प्रभावित करता है। परिणामस्वरूप, यह कॉलबैक कोई भी invariant उल्लंघन उत्पन्न नहीं कर सकता है।
भले ही मॉक रिसीवर safeMint() या safeTransferFrom() (उनके bytes वेरिएंट सहित) को रिवर्ट करने का कारण बनता है — उदाहरण के लिए, गलत कॉलबैक मान लौटाकर — invariants अप्रभावित रहते हैं क्योंकि रिवर्ट्स से कोई स्टेट परिवर्तन नहीं होता है। हालाँकि, बाद के अध्याय में जब हम औपचारिक रूप से सेफ मिंट और सेफ ट्रांसफर फ़ंक्शन्स को वेरिफाई करेंगे तो ऐसा नहीं होगा, जहाँ रिवर्ट होने वाले कॉलबैक असर्शन फेलियर (assertion failures) का कारण बनते हैं।
इस CVL invariant स्पेसिफिकेशन में, DISPATCHER की भूमिका केवल एक्सटर्नल कॉल को हल करना है। इसके बिना, safeMint() और safeTransferFrom() — उनके वेरिएंट सहित — अनसुलझी एक्सटर्नल कॉल्स को इनवोक करते हैं, जो havoc का कारण बनता है और फॉल्स-पॉजिटिव invariant विफलताओं को जन्म देता है।
balanceOfConsistency invariant के लिए पूरा स्पेसिफिकेशन और Prover रन
यहाँ balanceOfConsistency invariant के लिए पूरा CVL स्पेसिफिकेशन दिया गया है, जिसमें methods ब्लॉक, ghost वेरिएबल डिक्लेरेशन और हुक कार्यान्वयन शामिल हैं:
methods {
function balanceOf(address) external returns (uint256) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: 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);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
नोट: प्रिजर्व्ड (preserved) ब्लॉक को जानबूझकर कमेंट आउट किया गया है क्योंकि invariant इसके बिना ही सफलतापूर्वक वेरिफाई हो जाता है, जिसका अर्थ है कि यह सख्ती से आवश्यक नहीं है।
यहाँ वेरिफाई किया गया Prover रन है।
ownerHasBalance invariant — टोकन ओनर्स के पास पॉजिटिव बैलेंस होता है
यह invariant बताता है कि यदि एक tokenId मौजूद है (मालिक गैर-शून्य है), तो उस मालिक का बैलेंस शून्य से अधिक होना चाहिए:
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
...
बाद के अध्यायों में जब ट्रांसफर को वेरिफाई किया जाएगा, तब इस invariant का उपयोग एक पूर्व शर्त (precondition) के रूप में किया जाता है, जहाँ प्रेषक (sender) के पास एक पॉजिटिव बैलेंस होना चाहिए। हम सीधे रूल में unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 को हार्डकोड कर सकते हैं, लेकिन इसे एक invariant के रूप में साबित करना अधिक मजबूत सुरक्षा गारंटी प्रदान करता है।
ownerHasBalance चलने से पहले balanceOfConsistency(ownerOf(tokenId)) को अनिवार्य (require) करने के लिए यहाँ एक प्रिजर्व्ड ब्लॉक की आवश्यकता है। यह Prover को बताता है: “यह जाँचने से पहले कि क्या ओनर के पास बैलेंस है, पहले यह पुष्टि करें कि balanceOf ghosts द्वारा ट्रैक किए गए ओनरशिप काउंट से मेल खाता है।” यह Prover को ऐसे असंगत स्टेट्स में प्रवेश करने से रोकता है जहाँ एक मालिक मौजूद तो होता है लेकिन havoc के कारण उसका बैलेंस शून्य प्रतीत होता है।
यहाँ CVL invariant है:
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
ownerHasBalance invariant के लिए पूरा स्पेसिफिकेशन और Prover रन
यहाँ ownerHasBalance invariant के लिए पूरा CVL स्पेसिफिकेशन दिया गया है, जिसमें methods ब्लॉक, ghost वेरिएबल्स, हुक्स, और preserved balanceOfConsistency invariant शामिल हैं:
methods {
function ownerOf(uint256) external returns (address) envfree;
function balanceOf(address) external returns (uint256) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: 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);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover v8.3.1
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
नोट: मूल invariant एक्सप्रेशन balanceOf(ownerOf(tokenId)) > 0 था, लेकिन Prover वर्ज़न 8.3.1 के साथ वेरिफाई करने के लिए इसे अपडेट करके unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 कर दिया गया था।
यहाँ Prover रन है।
ownedTotalIsSumOfBalances invariant — स्वामित्व वाले कुल टोकन सभी बैलेंस के योग के बराबर होते हैं
इस invariant स्पेसिफिकेशन में, स्वामित्व वाले टोकनों की कुल संख्या और कुल सप्लाई प्राप्त (derive) की जाती है क्योंकि कोर ERC-721 मानक कुल सप्लाई (total supply) की किसी भी धारणा (notion) को एक्सपोज नहीं करता है — केवल ERC-721 Enumerable ही totalSupply() को परिभाषित करता है। चूँकि इस invariant को सीधे किसी मानक फ़ंक्शन के विरुद्ध वेरिफाई नहीं किया जा सकता है, इसलिए इन मानों (values) को ghost वेरिएबल्स (_ownedTotal और _supply) और हुक्स का उपयोग करके फिर से बनाया (reconstruct) जाता है।
_ownedTotal यह गिनता है कि वर्तमान में कितने टोकन मौजूद हैं। यह स्टोरेज वेरिएबल _owners पर Sstore हुक के माध्यम से ओनरशिप में हुए बदलावों को ऑब्जर्व करके किया जाता है। _supply सभी उपयोगकर्ता बैलेंस का योग है, जिसे एक ghost के रूप में भी ट्रैक किया जाता है।
इन दो मानों को फिर से बनाने और ghosts के रूप में ट्रैक करने के साथ, invariant यह वेरिफाई करता है कि _ownedTotal _supply के बराबर है। यह एक सुसंगत (consistent) बैलेंस अकाउंटिंग सुनिश्चित करता है। यदि स्वामित्व वाले टोकन सप्लाई से अधिक हैं, तो बैलेंस को कम गिना गया है (टोकन मौजूद हैं लेकिन बैलेंस में नहीं दिखते)। यदि सप्लाई स्वामित्व वाले टोकनों से अधिक है, तो बैलेंस को अधिक गिना गया है (बैलेंस वास्तव में मौजूद टोकनों की तुलना में अधिक टोकन का दावा करते हैं)।
इसलिए यह समानता इस बात की गारंटी देती है कि हर स्वामित्व वाले टोकन को बैलेंस टोटल में ठीक एक बार गिना जाता है:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
// preserved blocks will be shown later
}
_supply और _ownedTotal दोनों ghost मैपिंग वेरिएबल्स हैं जिनका उपयोग Sstore हुक्स के माध्यम से कुल टोकन सप्लाई को ट्रैक करने के लिए किया जाता है, लेकिन अलग-अलग दृष्टिकोण से:
-
_supplyहर बार_balancesमें स्टोरेज राइट होने पर पुराने बैलेंस को घटाकर और नया बैलेंस जोड़कर कुल सप्लाई को ट्रैक करता है:hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { _supply = _supply - oldValue + newValue; }स्टोरेज स्तर पर बैलेंस को ऑब्जर्व करके,
_supplyप्राप्त किया जाता है, और_supplyपर प्रभाव ऑपरेशन के प्रकार पर निर्भर करता है:- जब उपयोगकर्ता के लिए एक टोकन मिंट किया जाता है और बैलेंस
oldValue = 2सेnewValue = 3में बदल जाता है, तो_supplyकी गणना_supply = _supply - 2 + 3के रूप में की जाती है, जिसके परिणामस्वरूप 1 की शुद्ध वृद्धि (net increase) होती है। - जब किसी टोकन को ओनर से बर्न किया जाता है और बैलेंस
oldValue = 3सेnewValue = 2में बदल जाता है, तो_supplyकी गणना_supply = _supply - 3 + 2के रूप में की जाती है, जिसके परिणामस्वरूप 1 की शुद्ध कमी (net decrease) होती है। - जब कोई उपयोगकर्ता किसी अन्य उपयोगकर्ता को टोकन ट्रांसफर करता है, तो भेजने वाले का बैलेंस 1 कम हो जाता है जबकि प्राप्त करने वाले का बैलेंस 1 बढ़ जाता है। भेजने वाले से होने वाली कमी प्राप्त करने वाले की वृद्धि को संतुलित (offset) कर देती है, इसलिए
_supplyअपरिवर्तित रहता है।
- जब उपयोगकर्ता के लिए एक टोकन मिंट किया जाता है और बैलेंस
-
_ownedTotalएकSstoreहुक के माध्यम से ओनरशिप क्लियर होने पर 1 घटाकर और गैर-शून्य एड्रेस पर टोकन असाइन किए जाने पर 1 जोड़कर स्वामित्व वाले टोकनों की संख्या को ट्रैक करता है:hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) { ... _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0); }आइए ओनरशिप परिवर्तनों के आधार पर इसे सिमुलेट (simulate) करें, लेकिन पहले, आइए स्पष्टता के लिए कोड को पुनर्व्यवस्थित (rearrange) करें:
_ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);-
यदि
oldOwnerऔरnewOwnerदोनों गैर-शून्य एड्रेस हैं, तो ट्रांसफर होता है:newOwnerगैर-शून्य है, इसलिए टर्नरी एक्सप्रेशन का मान1होता है, और1जोड़ा जाता है।oldOwnerगैर-शून्य है, इसलिए टर्नरी एक्सप्रेशन का मान1होता है, और1घटाया जाता है।
शुद्ध प्रभाव (net effect)
_ownedTotalमें कोई बदलाव नहीं है, क्योंकि1जोड़ा जाता है और1घटाया जाता है। सिद्धांत रूप में, एक ट्रांसफर ऑपरेशन कुल ओनरशिप काउंट को प्रभावित नहीं करता है। -
यदि
oldOwnerशून्य है औरnewOwnerगैर-शून्य है, तो मिंट होता है:newOwnerगैर-शून्य है, इसलिए टर्नरी एक्सप्रेशन का मान1होता है, और1जोड़ा जाता है।oldOwnerशून्य है, इसलिए टर्नरी एक्सप्रेशन का मान0होता है, और0घटाया जाता है।
शुद्ध प्रभाव
+1है, क्योंकि1जोड़ा जाता है और कुछ भी नहीं घटाया जाता है। सिद्धांत रूप में, मिंट ऑपरेशन कुल ओनरशिप काउंट में वृद्धि करता है। -
यदि
oldOwnerगैर-शून्य है औरnewOwnerशून्य है, तो बर्न होता है:newOwnerशून्य है, इसलिए टर्नरी एक्सप्रेशन का मान0होता है, और0जोड़ा जाता है।oldOwnerगैर-शून्य है, इसलिए टर्नरी एक्सप्रेशन का मान1होता है, और1घटाया जाता है।
शुद्ध प्रभाव
–1है, क्योंकि कुछ भी नहीं जोड़ा जाता है और1घटाया जाता है। सिद्धांत रूप में, बर्न ऑपरेशन कुल ओनरशिप काउंट को कम करता है।
-
प्रिजर्व्ड क्लॉज़ (Preserved Clauses):
Invariant में प्रिजर्व्ड क्लॉज़ शामिल हैं। निम्नलिखित उनमें से प्रत्येक को संक्षेप में प्रस्तुत करता है:
-
मिंट के लिए:
mint(),safeMint(),safeMint(bytes)-
require balanceLimited(to)Prover को अवास्तविक ओवरफ़्लो रास्तों (overflow paths) की खोज करने से रोकने के लिए प्राप्तकर्ता का बैलेंस
max_uint256से नीचे रहना चाहिए।
-
-
बर्न के लिए:
burn()-
requireInvariant ownerHasBalance(tokenId)बर्न किए जाने से पहले टोकन के मालिक के पास पॉजिटिव बैलेंस होना चाहिए।
-
-
ट्रांसफर के लिए:
transferFrom(),safeTransferFrom(),safeTransferFrom(bytes)-
require balanceLimited(to)प्राप्तकर्ता का बैलेंस
max_uint256से नीचे रहना चाहिए। -
requireInvariant ownerHasBalance(tokenId)टोकन गैर-शून्य बैलेंस वाले एक वैध मालिक से आना चाहिए।
-
यहाँ वह invariant है जिसमें प्रिजर्व्ड क्लॉज़ शामिल हैं:
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
preserved mint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
}
preserved burn(uint256 tokenId) with (env e) {
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(ownerOf(tokenId));
}
preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
}
नोट: Invariant ownedTotalIsSumOfBalances बिना requireInvariant balanceOfConsistency के भी सफलतापूर्वक वेरिफाई हो जाता है। चर्चा के उद्देश्य से, हमने इसे कमेंट आउट कर दिया ताकि पाठक देख सकें कि invariant को वेरिफाई करने के लिए कौन सी प्रिजर्व्ड स्थितियाँ सख्ती से आवश्यक हैं। इसका मतलब यह नहीं है कि यह बेकार है — चूँकि यह पहले ही साबित हो चुका है, इसलिए यह माना जा सकता है कि यह हमेशा सत्य रहेगा। इसलिए, इसे सुरक्षित रूप से फिर से लागू किया जा सकता है। इसे एक प्रिजर्व्ड स्थिति के रूप में जोड़ने से आम तौर पर Prover रन का समय कम हो जाता है।
ownedTotalIsSumOfBalances invariant के लिए पूरा स्पेसिफिकेशन और Prover रन
यहाँ ownedTotalIsSumOfBalances invariant के लिए पूरा CVL स्पेसिफिकेशन दिया गया है, जिसमें methods ब्लॉक, ghost वेरिएबल्स, हुक्स, और preserved ownerHasBalance और balanceOfConsistency invariants शामिल हैं:
methods {
function ownerOf(uint256) external returns (address) envfree;
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 balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
ghost mathint _ownedTotal {
init_state axiom _ownedTotal == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
_ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _supply {
init_state axiom _supply == 0;
}
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
preserved mint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
}
preserved burn(uint256 tokenId) with (env e) {
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(ownerOf(tokenId));
}
preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
}
Prover रन: लिंक
notMintedUnset invariant — अनमिंट किए गए टोकनों के लिए कोई अप्रूवल नहीं होता है
यदि कोई टोकन मिंट नहीं किया गया है (अर्थात इसका कोई मालिक नहीं है), तो इसका कोई अप्रूव्ड एड्रेस भी नहीं होना चाहिए:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
unsafeOwnerOf() और unsafeGetApproved() harness व्यू फ़ंक्शन्स हैं जो tokenId अनमिंट होने पर रिवर्ट करने के बजाय शून्य एड्रेस (zero address) लौटाते हैं। इसके विपरीत, मानक ownerOf() और getApproved() फ़ंक्शन्स अनमिंट किए गए टोकन के लिए रिवर्ट करते हैं और इसलिए कभी भी ये शून्य एड्रेस वैल्यूज़ नहीं लौटाते हैं।
ownerOf() और getApproved() का उपयोग करने से invariant मूल्यांकन (evaluation) के लिए समस्या उत्पन्न होगी। Invariants बुलियन (boolean) एक्सप्रेशन्स होने चाहिए जिनका मान true या false आता हो, लेकिन जब Prover किसी ऐसे invariant का मूल्यांकन करता है जो एक अनमिंट किए गए tokenId पर ownerOf(tokenId) या getApproved(tokenId) को कॉल करता है, तो फ़ंक्शन कॉल रिवर्ट हो जाता है। एक रिवर्ट न तो true है और न ही false, जो invariant एक्सप्रेशन को बुलियन वैल्यू में मूल्यांकित होने से रोकता है। जबकि रूल्स रिवर्टिंग कॉल्स को संभालने के लिए @withrevert का उपयोग कर सकते हैं और lastReverted फ्लैग का निरीक्षण कर सकते हैं, invariants शुद्ध बुलियन एक्सप्रेशन हैं और ऐसे नियंत्रण-प्रवाह (control-flow) लॉजिक का समर्थन नहीं करते हैं।
Harness फ़ंक्शन्स unsafeOwnerOf() और unsafeGetApproved() का उपयोग करके, जो रिवर्ट करने के बजाय शून्य एड्रेस लौटाते हैं, Prover अनमिंट किए गए टोकन सहित सभी tokenId वैल्यूज़ के लिए invariant एक्सप्रेशन का मूल्यांकन एक बुलियन वैल्यू के रूप में कर सकता है।
यह invariant महत्वपूर्ण है क्योंकि यदि किसी ऐसे tokenId के लिए अप्रूवल किसी तरह सेट हो जाता है जो मौजूद नहीं है, और उस tokenId को बाद में एक अलग एड्रेस पर मिंट किया जाता है, तो पहले से अप्रूव किया गया एड्रेस अभी भी ट्रांसफर अधिकार बनाए रखेगा। यह मिंटिंग के तुरंत बाद अनधिकृत ट्रांसफर (unauthorized transfers) की अनुमति दे सकता है। यह invariant गारंटी देता है कि सभी टोकन डिफ़ॉल्ट स्थिति से शुरू होते हैं — न कोई मालिक, न कोई अप्रूवल।
notMintedUnset invariant के लिए पूरा स्पेसिफिकेशन और Prover रन
methods {
function unsafeGetApproved(uint256) external returns (address) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
Prover रन: लिंक
zeroAddressHasNoApprovedOperator invariant — अनमिंट किए गए टोकनों के लिए कोई अप्रूव्ड ऑपरेटर नहीं होता है
isApprovedForAll एक पब्लिक फ़ंक्शन है जो यह जांचता है कि क्या कोई ऑपरेटर (एक एड्रेस) किसी विशेष अकाउंट के स्वामित्व वाले सभी टोकन को प्रबंधित करने के लिए अधिकृत (authorized) है। यह invariant बताता है कि किसी भी एड्रेस को कभी भी address(0) के लिए ऑपरेटर के रूप में स्वीकृत नहीं किया जाना चाहिए। चूँकि address(0) अनमिंट किए गए टोकन का अंतर्निहित (implicit) मालिक है, इसलिए यह किसी भी ऑपरेटर को मिंट होने से पहले टोकन प्रबंधित करने के लिए पूर्व-अधिकृत (pre-authorized) होने से रोकता है।
इसलिए, व्यू फ़ंक्शन isApprovedForAll(0, a) को हमेशा false लौटाना चाहिए:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
हालाँकि, यह केवल इस प्रिजर्व्ड शर्त के तहत मान्य है कि कॉलर (msg.sender) शून्य एड्रेस नहीं है (require nonzerosender(e)) जैसा कि परिभाषा के अनुसार है:
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
यह धारणा (assumption) उचित है क्योंकि address(0) के पास कोई प्राइवेट की (private key) नहीं है, इसलिए कोई भी इस एड्रेस से ट्रांज़ैक्शन शुरू नहीं कर सकता है, जिससे वास्तव में किसी भी फ़ंक्शन को कॉल करना असंभव हो जाता है। हालाँकि, चूँकि setApprovalForAll() फ़ंक्शन स्पष्ट रूप से शून्य एड्रेस को इसे कॉल करने से नहीं रोकता है, इसलिए Prover इस संभावना का पता लगाएगा, जिससे फॉल्स पॉजिटिव उल्लंघन हो सकते हैं, जहाँ Prover ऐसे उल्लंघन की रिपोर्ट करता है जो व्यवहार में नहीं हो सकता।
msg.sender के गैर-शून्य होने को सुनिश्चित करने वाली प्रिजर्व्ड शर्त के साथ, यह invariant गारंटी देता है कि address(0) के कभी भी अप्रूव्ड ऑपरेटर्स नहीं हो सकते हैं। इसलिए, अनमिंट किए गए टोकन का कोई ऑपरेटर नहीं हो सकता।
zeroAddressHasNoApprovedOperator invariant के लिए पूरा स्पेसिफिकेशन और Prover रन
अब यहाँ invariant zeroAddressHasNoApprovedOperator का पूरा स्पेसिफिकेशन है, जिसमें methods ब्लॉक और definition शामिल हैं:
methods {
function isApprovedForAll(address,address) external returns (bool) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
Prover रन: लिंक
सभी Invariants के लिए समेकित (Consolidated) CVL स्पेसिफिकेशन
अब जब हमने प्रत्येक invariant पर स्वतंत्र रूप से चर्चा कर ली है, तो हम उन्हें एक ही स्पेसिफिकेशन में समेकित कर सकते हैं:
methods {
function balanceOf(address) external returns (uint256) envfree;
function ownerOf(uint256) external returns (address) envfree;
function isApprovedForAll(address,address) external returns (bool) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function unsafeGetApproved(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _ownedTotal {
init_state axiom _ownedTotal == 0;
}
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
_ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _supply {
init_state axiom _supply == 0;
}
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover V8
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
preserved mint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
}
preserved burn(uint256 tokenId) with (env e) {
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(ownerOf(tokenId));
}
preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
यहाँ Prover रन है।
यह लेख Certora Prover का उपयोग करके औपचारिक सत्यापन (formal verification) पर एक श्रृंखला का हिस्सा है