परिचय (Introduction)
DeFi में स्वैप (swaps), लिक्विडिटी प्रोविजन (liquidity provision), स्टेकिंग (staking) और कोलैटरल (collateral) के लिए व्यापक रूप से उपयोग किए जाने वाले ETH को एक ERC-20-कम्पैटिबल वर्ज़न की आवश्यकता होती है ताकि प्रोटोकॉल अन्य टोकन के लिए उपयोग किए जाने वाले समान मानकीकृत इंटरफ़ेस (standardized interface) के माध्यम से इसके साथ इंटरैक्ट कर सकें।
इससे Wrapped ETH (WETH) का उदय हुआ, जिसका सिद्धांत सीधा है: नेटिव ETH डिपॉजिट करने पर यूज़र के अकाउंट में समान मात्रा में WETH मिंट (mint) हो जाता है, जबकि विथड्रॉ करने पर संबंधित WETH बर्न (burn) हो जाता है और नेटिव ETH यूज़र के अकाउंट में वापस आ जाता है।
पिछले अध्याय में, हमने एक सामान्य ERC-20 कॉन्ट्रैक्ट की आवश्यक प्रॉपर्टीज़ को फॉर्मली वेरीफाई किया था। चूँकि WETH स्वयं एक ERC-20 है, हम उन स्पेसिफिकेशन्स को यहाँ नहीं दोहराएँगे और इसके बजाय केवल WETH की विशिष्ट फंक्शनैलिटीज़ पर ध्यान केंद्रित करेंगे। हम Solady WETH इम्प्लीमेंटेशन को फॉर्मली वेरीफाई करेंगे, जो गैस ऑप्टिमाइज़ेशन के लिए इनलाइन असेंबली (inline assembly) का उपयोग करता है।
फॉर्मली वेरीफाई करने के लिए WETH प्रॉपर्टीज़
जब कोई यूज़र ETH डिपॉजिट करता है, तो उसे समान मात्रा में WETH मिलना चाहिए। जब वे विथड्रॉ करते हैं, तो वे किसी भी समय उस WETH को समान मात्रा में ETH के लिए रिडीम करने में सक्षम होने चाहिए।
ये दो व्यवहार मानक ERC-20 फंक्शनैलिटीज़ से परे WETH कॉन्ट्रैक्ट की मुख्य गारंटी को परिभाषित करते हैं। उन्हें बनाए रखने के लिए, कॉन्ट्रैक्ट को दो प्रमुख इनवेरिएंट्स (invariants) को पूरा करना चाहिए:
- कॉन्ट्रैक्ट द्वारा रखा गया ETH हमेशा WETH की कुल सप्लाई से अधिक या उसके बराबर होना चाहिए। यह गारंटी देता है कि सभी WETH होल्डर्स रिडेम्पशन ऑर्डर या समय की परवाह किए बिना, किसी भी समय ETH के लिए अपने टोकन को रिडीम कर सकते हैं।
- WETH की कुल सप्लाई हमेशा सभी WETH बैलेंस के योग से अधिक या उसके बराबर होनी चाहिए। यह गारंटी देता है कि कॉन्ट्रैक्ट अपने द्वारा मिंट किए गए टोकन से अधिक टोकन डिस्ट्रीब्यूट नहीं कर सकता है।
हालाँकि, हम दूसरे इनवेरिएंट को फॉर्मली वेरीफाई नहीं करेंगे क्योंकि Solady WETH कॉन्ट्रैक्ट एक ऐसे ERC-20 इम्प्लीमेंटेशन को इनहेरिट करता है जो अकाउंट बैलेंस के लिए मैपिंग (mapping) का उपयोग नहीं करता है। इसके बजाय, यह प्रत्येक अकाउंट के लिए एक कैलकुलेटेड स्लॉट (calculated slot) का उपयोग करके स्टोरेज से पढ़ता है और उसमें लिखता है।
इसलिए, इस इनवेरिएंट को वेरीफाई करने के लिए CVL “summarization” की आवश्यकता होती है: हमें उन फंक्शन्स को समराइज़ करना होगा जो अकाउंट बैलेंस स्टोरेज को मॉडिफाई करते हैं, उन्हें एक घोस्ट मैपिंग (ghost mapping) का उपयोग करके मिरर करना होगा, और उस घोस्ट स्टेट के माध्यम से इनवेरिएंट के बारे में तर्क देना होगा। यह विषय इस अध्याय के दायरे से बाहर है। अधिक जानकारी के लिए, summarization पर Certora डॉक्यूमेंटेशन देखें।
इस इनवेरिएंट को वेरीफाई करने के बजाय, हम एक और इनवेरिएंट को फॉर्मली वेरीफाई करते हैं: कोई भी अकाउंट बैलेंस कुल सप्लाई से अधिक नहीं होता है। यह मामूली लग सकता है, लेकिन यह बाद में उपयोगी हो जाता है जब डिपॉजिट और विथड्रॉ के नियम बैलेंस-संबंधी प्रीकंडीशन्स (preconditions) पर निर्भर करते हैं। यह इनवेरिएंट हमें requireInvariant का उपयोग करके उन मान्यताओं को बदलने की अनुमति देता है, जो यह गारंटी प्रदान करता है कि जो प्रीकंडीशन्स हम मान रहे हैं वे वास्तव में मान्य हैं।
डिपॉजिट किया गया ETH प्राप्त WETH के बराबर है
जब कोई यूज़र deposit() फंक्शन का उपयोग करके कॉन्ट्रैक्ट में ETH डिपॉजिट करता है, तो उनका WETH बैलेंस बढ़ जाता है और उनका ETH बैलेंस उसी मात्रा में कम हो जाता है। CVL में इस व्यवहार को फॉर्मली वेरीफाई करने के लिए, हम इस प्रकार आगे बढ़ते हैं:
- प्रीकंडीशन्स सेट करें:
- सेंडर स्वयं कॉन्ट्रैक्ट नहीं होना चाहिए (
e.msg.sender != currentContract) क्योंकि सेल्फ-कॉल ETH बैलेंस अकाउंटिंग को तोड़ देते हैं, और कोई भी एग्जीक्यूशन पाथ ऐसे कॉल की अनुमति नहीं देता है। - सेंडर के WETH बैलेंस और डिपॉजिट की गई राशि का योग ओवरफ्लो (overflow) नहीं होना चाहिए (
balanceOf(e.msg.sender) + e.msg.value <= max_uint256)।
- सेंडर स्वयं कॉन्ट्रैक्ट नहीं होना चाहिए (
deposit()को इनवोक (invoke) करने से पहले यूज़र के ETH और WETH बैलेंस को रिकॉर्ड करें।e.msg.valueमें ETH राशि के साथdeposit()को इनवोक करें।deposit()को इनवोक करने के बाद यूज़र के ETH और WETH बैलेंस को रिकॉर्ड करें।- करेक्टनेस कंडीशन (correctness conditions) का दावा (assert) करें:
- अंतिम ETH बैलेंस प्रारंभिक ETH बैलेंस में से डिपॉजिट की गई राशि को घटाने के बराबर है।
- अंतिम WETH बैलेंस प्रारंभिक WETH बैलेंस में डिपॉजिट की गई राशि को जोड़ने के बराबर है।
यहाँ CVL रूल इम्प्लीमेंटेशन है:
rule deposit_ethDepositedEqualsWethReceived(env e) {
require e.msg.sender != currentContract;
require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // will be replaced by an invariant
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}
अब आइए इसे विस्तार से समझें।
प्रीकंडीशन्स
पहली प्रीकंडीशन Prover को उन मामलों को बाहर करने का निर्देश देती है जहाँ कॉलर (msg.sender) स्वयं कॉन्ट्रैक्ट है:
require e.msg.sender != currentContract;
इस प्रीकंडीशन के बिना, Prover यह मान लेता है कि कॉलर currentContract हो सकता है, जिससे रूल फेल हो जाता है। उदाहरण के लिए, यदि कॉन्ट्रैक्ट स्वयं में 1 ETH डिपॉजिट करता है, तो उसके ETH होल्डिंग्स में कोई शुद्ध परिवर्तन नहीं होगा (क्योंकि वह स्वयं को समान राशि भेजता और प्राप्त करता है)। हालाँकि, कॉन्ट्रैक्ट अभी भी 1 WETH मिंट करेगा, जिससे एशर्शन ethBalanceAfter == ethBalanceBefore - e.msg.value फेल हो जाएगा।
दूसरी प्रीकंडीशन, require balanceOf(e.msg.sender) + e.msg.value <= max_uint256, कॉलर के प्रारंभिक WETH बैलेंस और ETH डिपॉजिट को जोड़ते समय ओवरफ्लो की संभावना को खारिज करती है।
चूँकि require स्टेटमेंट्स ऐसी मान्यताएँ हैं जिन्हें Prover वेरीफाई नहीं करता है — यह बस उन्हें दिए गए के रूप में लेता है — हमें बाद के सेक्शन में इसे एक इनवेरिएंट के रूप में फॉर्मली साबित करने की आवश्यकता है। एक बार साबित हो जाने पर, हम requireInvariant का उपयोग करके इस मानी गई प्रीकंडीशन को वेरीफाई किए गए इनवेरिएंट से बदल सकते हैं।
deposit() कॉल से पहले और बाद में यूज़र के ETH और WETH बैलेंस रिकॉर्ड करें
सभी प्रीकंडीशन्स सेट होने के बाद, हमें deposit() को इनवोक करने से पहले और बाद में कॉलर के ETH और WETH बैलेंस को रिकॉर्ड करना होगा। इन रिकॉर्ड किए गए मानों का उपयोग एशर्शन्स (assertions) में बैलेंस परिवर्तन के बारे में तर्क देने के लिए किया जाएगा:
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
एशर्शन्स (Assertions)
पहला एशर्शन यह जाँचता है कि कॉलर का ETH बैलेंस ठीक उसी ETH मात्रा से कम हुआ है जो ट्रांज़ैक्शन के साथ भेजा गया था। दूसरा एशर्शन यह जाँचता है कि कॉलर का WETH बैलेंस ठीक उसी डिपॉजिट की गई ETH मात्रा से बढ़ गया है:
assert ethBalanceAfter == ethBalanceBefore - e.msg.value; // ETH is deposited -- ETH balance decreases
assert wethBalanceAfter == wethBalanceBefore + e.msg.value; // WETH is received -- WETH balance increases
यहाँ deposit_ethDepositedEqualsWethReceived रूल के लिए वेरीफाई किया गया Prover run है।
ETH डिपॉजिट WETH की कुल सप्लाई को बढ़ाता है
बैलेंस बदलने के अलावा, deposit() कॉल का एक और अपेक्षित प्रभाव WETH की totalSupply में वृद्धि है। निम्नलिखित CVL रूल इस व्यवहार को कैप्चर करता है:
rule deposit_ethDepositIncreasesWETHTotalSupply(env e) {
mathint totalSupplyBefore = totalSupply();
deposit(e);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore + e.msg.value;
}
वेरिएबल totalSupplyBefore और totalSupplyAfter एशर्शन में अपेक्षित परिवर्तन को वेरीफाई करने के लिए deposit() कॉल से पहले और बाद के कुल सप्लाई मानों को रिकॉर्ड करते हैं।
चूँकि deposit() फंक्शन आंतरिक रूप से _mint() को कॉल करता है, WETH की कुल सप्लाई डिपॉजिट की गई राशि के बराबर बढ़ जाती है, जैसा कि एशर्शन में परिलक्षित होता है:
assert totalSupplyAfter == totalSupplyBefore + e.msg.value;
ध्यान दें कि यहाँ कोई प्रीकंडीशन require msg.sender != currentContract नहीं है क्योंकि एशर्शन केवल सप्लाई वृद्धि से संबंधित है। सेंडर चाहे जो भी हो, डिपॉजिट की गई ETH राशि (msg.value) से सप्लाई बढ़ जाती है।
यहाँ deposit_ethDepositIncreasesWETHTotalSupply रूल के लिए वेरीफाई किया गया Prover run है।
deposit() में रिवर्ट (revert) के कारणों को वेरीफाई करना
आइए अब deposit() फंक्शन के रिवर्ट पाथ को वेरीफाई करें। हम ऐसे मामलों का पता लगाना चाहते हैं जहाँ यह या तो अप्रत्याशित रूप से रिवर्ट हो जाता है या जब इसे होना चाहिए तब रिवर्ट होने में विफल रहता है।
CVL में इस व्यवहार को फॉर्मली वेरीफाई करने के लिए, हम इस प्रकार आगे बढ़ते हैं:
- एक प्रीकंडीशन सेट करें कि कॉलर का WETH बैलेंस और डिपॉजिट की गई राशि का योग ओवरफ्लो नहीं होना चाहिए (
balanceOf(caller) + ethDeposit <= max_uint256)। deposit()को इनवोक करने से पहले WETHtotalSupplyऔर कॉलर के ETH बैलेंस को रिकॉर्ड करें।- रूल को रिवर्ट का निरीक्षण करने की अनुमति देने के लिए
@withrevertटैग के साथdeposit()को इनवोक करें। lastRevertedका उपयोग करें, जो एक बूलियन (boolean) लौटाता है जो दर्शाता है कि पिछला कॉल रिवर्ट हुआ या नहीं।- दावा करें कि फंक्शन केवल और केवल तभी (
<=>) रिवर्ट होता है जब निम्नलिखित में से कोई भी स्थिति सत्य हो:- कॉल से पहले कॉलर का ETH बैलेंस डिपॉजिट राशि (
e.msg.value) से कम है। - कॉल से पहले कुल WETH सप्लाई और डिपॉजिट राशि का योग
max_uint256से अधिक है।
- कॉल से पहले कॉलर का ETH बैलेंस डिपॉजिट राशि (
यहाँ CVL रूल है:
rule deposit_revert(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}
आइए रूल को और विस्तार से समझें।
पढ़ने में आसानी के लिए, हम क्रमशः e.msg.sender और e.msg.value को caller और ethDeposit असाइन करते हैं:
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
नीचे दी गई प्रीकंडीशन, पिछले रूल deposit_ethDepositedEqualsWethReceived() में भी दिखाई दी थी:
require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant
रिवर्ट स्थितियों के हिस्से के बजाय, यहाँ एक प्रीकंडीशन के रूप में इसकी पुनरावृत्ति, इसे फॉर्मली वेरीफाई करने की आवश्यकता को और मजबूत करती है।
इसके बाद, हम deposit() फंक्शन को इनवोक करने से पहले totalSupplyBefore (WETH कुल सप्लाई) और कॉलर के nativeBalances के मान रिकॉर्ड करते हैं:
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
अब, हम @withrevert टैग के साथ deposit() फंक्शन को इनवोक करते हैं और रिकॉर्ड करते हैं कि कॉल रिवर्ट हुआ या नहीं:
deposit@withrevert(e);
bool isLastReverted = lastReverted;
अंत में, एशर्शन बाइसकंडीशनल ऑपरेटर (biconditional operator, <=>) का उपयोग करता है और सभी रिवर्ट मामलों को डिज़्ज़ंक्टिव रूप से (OR का उपयोग करके) सूचीबद्ध करता है:
-
फंक्शन तब रिवर्ट होता है जब कॉलर का पिछला ETH बैलेंस (
ethBalanceBefore) ETH डिपॉजिट (e.msg.value) से कम होता है।इसका मतलब है कि कॉलर के पास डिपॉजिट करने के लिए पर्याप्त ETH नहीं है।
-
फंक्शन तब भी रिवर्ट होता है जब WETH कुल सप्लाई (
totalSupplyBefore) और ETH डिपॉजिट का योगmax_uint256से अधिक हो जाता है।चूँकि प्रत्येक डिपॉजिट WETH की समान मात्रा को मिंट करता है,
uint256सीमा से अधिक होने पर ओवरफ्लो हो जाएगा।
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit || // the caller doesn't have enough eth to deposit
totalSupplyBefore + ethDeposit > max_uint256 // results in overflow
);
प्रीकंडीशन msg.sender != currentContract अनावश्यक है क्योंकि रिवर्ट स्थितियाँ अपर्याप्त बैलेंस और ओवरफ्लो से संबंधित हैं, जो कॉलर की पहचान से स्वतंत्र हैं।
यहाँ deposit_revert रूल के लिए वेरीफाई किया गया Prover run है।
विथड्रॉ किया गया ETH घटाए गए WETH के बराबर है
जब कोई यूज़र कॉन्ट्रैक्ट से ETH विथड्रॉ करता है, तो उसका ETH बैलेंस बढ़ जाता है और उसका WETH बैलेंस समान मात्रा में कम हो जाता है। निम्नलिखित CVL रूल इस व्यवहार को कैप्चर करता है:
rule withdraw_ethWithdrawnEqualsWETHReduced(env e) {
uint256 amount;
require e.msg.sender != currentContract;
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw(e,amount);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore + amount;
assert wethBalanceAfter == wethBalanceBefore - amount;
}
यह rule deposit_ethDepositedEqualsWethReceived() के समान संरचना का पालन करता है। अब तक, यह पैटर्न परिचित हो जाना चाहिए:
- प्रीकंडीशन्स सेट करें
withdraw()को इनवोक करने से पहले कॉलर का ETH और WETH बैलेंस रिकॉर्ड करेंwithdraw()इनवोक करें- बाद में कॉलर का ETH और WETH बैलेंस रिकॉर्ड करें
require e.msg.sender != currentContract;
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw(e,amount);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
अब, सीधे एशर्शन पर चलते हैं।
नीचे दिए गए एशर्शन्स में, हम यह वेरीफाई करते हैं कि ETH बैलेंस बढ़ता है और WETH बैलेंस उसी विथड्रॉ की गई राशि (amount) से घटता है:
assert ethBalanceAfter == ethBalanceBefore + amount;
assert wethBalanceAfter == wethBalanceBefore - amount;
प्रीकंडीशन require msg.sender != currentContract आवश्यक है क्योंकि एक सेल्फ-कॉल कॉन्ट्रैक्ट के ETH बैलेंस में कोई बदलाव नहीं लाएगा (स्वयं में जमा करने पर कोई शुद्ध बदलाव नहीं होता है), जिसके कारण एशर्शन ethBalanceAfter == ethBalanceBefore + amount फेल हो जाता है (एक फाल्स पॉजिटिव)।
यहाँ withdraw_ethWithdrawnEqualsWETHReduced रूल के लिए वेरीफाई किया गया Prover run है।
विथड्रॉ किया गया ETH WETH की कुल सप्लाई को कम करता है
जब कोई यूज़र ETH विथड्रॉ करता है, तो संबंधित WETH राशि बर्न हो जाती है, जिससे कुल सप्लाई कम हो जाती है। यह withdraw() फंक्शन का एक अपेक्षित प्रभाव है। निम्नलिखित CVL रूल इस व्यवहार को कैप्चर करता है:
rule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
uint256 amount;
require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}
चूँकि विथड्रॉल कुल सप्लाई को विथड्रॉ की गई राशि (जो बर्न किए गए बैलेंस के बराबर है) से कम कर देता है, निम्नलिखित प्रीकंडीशन यह सुनिश्चित करती है कि totalSupply का घटाव अंडरफ्लो (underflow) नहीं हो सकता, यह आवश्यक बनाकर कि कोई भी व्यक्तिगत बैलेंस कुल सप्लाई से अधिक न हो:
require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant
पिछले रूल की तरह, यह प्रीकंडीशन एक ऐसी मान्यता का प्रतिनिधित्व करती है जिसे बाद में फॉर्मली वेरीफाई किया जाना चाहिए।
इसके बाद, हम एक परिचित पैटर्न का पालन करते हैं, जहाँ हम withdraw कॉल से पहले और बाद में WETH कुल सप्लाई को रिकॉर्ड करते हैं:
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
फिर हम दावा करते हैं कि WETH totalSupply अपेक्षित राशि से कम हो जाती है:
assert totalSupplyAfter == totalSupplyBefore - amount;
प्रीकंडीशन require e.msg.sender != currentContract यहाँ अनावश्यक है क्योंकि सप्लाई में कमी (या सप्लाई में बदलाव) कॉलर कौन है, इससे स्वतंत्र है।
यह रूल पुष्टि करता है कि विथड्रॉल के दौरान WETH को बर्न करने से कुल सप्लाई सही ढंग से कम हो जाती है। यहाँ वेरीफाई किया गया Prover run है।
withdraw() में रिवर्ट के कारणों को वेरीफाई करना
withdraw_revert रूल deposit_revert रूल से अलग पैटर्न का पालन करता है। ऐसा क्यों है, यह समझने के लिए, आइए पहले withdraw फंक्शन पर एक नज़र डालें:
/// @dev Burns `amount` WETH of the caller and sends `amount` ETH to the caller.
function withdraw(uint256 amount) public virtual {
_burn(msg.sender, amount);
/// @solidity memory-safe-assembly
assembly {
// Transfer the ETH and check if it succeeded or not.
if iszero(call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)) {
mstore(0x00, 0xb12d13eb) // `ETHTransferFailed()`.
revert(0x1c, 0x04)
}
}
}
_burn() फंक्शन के अलावा, जो अपने स्वयं के रिवर्ट स्थितियों को इम्प्लीमेंट करता है, withdraw() फंक्शन में असेंबली कोड शामिल है जो यह जाँचता है कि क्या ETH ट्रांसफर सफल हुआ:
assembly {
// Transfer the ETH and check whether it succeeded.
if iszero(call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)) {
mstore(0x00, 0xb12d13eb) // `ETHTransferFailed()`.
revert(0x1c, 0x04)
}
}
यदि ETH ट्रांसफर विफल हो जाता है, तो iszero एक्सप्रेशन ट्रू (true) लौटाता है, जो एक रिवर्ट को ट्रिगर करता है। अन्यथा, यह false लौटाता है, जिसका अर्थ है कि ETH ट्रांसफर सफल रहा। इस असेंबली व्यवहार को वेरीफाई करने के लिए, हम यह देखने के लिए CVL हुक (CALL) का उपयोग करते हैं कि क्या लो-लेवल (low-level) ETH ट्रांसफर कॉल उम्मीद के मुताबिक रिवर्ट होता है।
यहाँ वह CVL रूल है जो लो-लेवल कॉल विफलता सहित सभी withdraw() रिवर्ट स्थितियों को वेरीफाई करता है:
persistent ghost bool g_lowLevelCallFail;
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
if (rc == 0) {
g_lowLevelCallFail = true;
} else {
g_lowLevelCallFail = false;
}
}
rule withdraw_revert(env e) {
uint256 amount; // the amount of eth to claim
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
amount > wethBalanceBefore ||
e.msg.value != 0 ||
g_lowLevelCallFail
);
}
आइए उपरोक्त रूल की व्याख्या करें।
नीचे दी गई लाइन परसिस्टेंट घोस्ट वेरिएबल (persistent ghost variable) का डिक्लेरेशन है:
persistent ghost bool g_lowLevelCallFail;
नोट: रेगुलर घोस्ट और परसिस्टेंट घोस्ट के बीच के अंतर पर चर्चा के लिए अलग अध्याय “Using Persistent Ghosts” देखें।
घोस्ट वेरिएबल को CALL हुक द्वारा अपडेट किया जाता है। हुक तब ट्रिगर होता है जब withdraw() मेथड को इनवोक किया जाता है, विशेष रूप से उस लो-लेवल कॉल द्वारा जो कॉलर को ETH ट्रांसफर करता है। यदि लो-लेवल कॉल विफल हो जाता है (rc == 0), तो घोस्ट वेरिएबल g_lowLevelCallFail को true पर सेट किया जाता है; यदि कॉल सफल होता है (rc != 0), तो इसे false पर सेट किया जाता है, जैसा कि नीचे दिए गए CALL हुक में दिखाया गया है:
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
if (rc == 0) {
g_lowLevelCallFail = true;
} else {
g_lowLevelCallFail = false;
}
}
यह Prover को असेंबली ब्लॉक्स के अंदर ETH ट्रांसफर की सफलता/विफलता को ट्रैक करने का एक तरीका देता है।
अब रूल पर चलते हैं।
हमेशा की तरह, हम withdraw() फंक्शन को कॉल करने से पहले बैलेंस को रिकॉर्ड करते हैं:
mathint wethBalanceBefore = balanceOf(e.msg.sender);
फिर हम @withrevert टैग के साथ withdraw() फंक्शन को इनवोक करते हैं और रिकॉर्ड करते हैं कि क्या कॉल रिवर्ट हुआ:
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
नीचे दिए गए एशर्शन में, फंक्शन केवल और केवल तभी (<=>) रिवर्ट होगा जब निम्नलिखित में से कोई एक शर्त पूरी होती है:
-
विथड्रॉल राशि (
amount) कॉलर के WETH बैलेंस (wethBalanceBefore) से अधिक है।इसका मतलब है कि कॉलर अपने WETH बैलेंस की अनुमति से अधिक ETH निकालने का प्रयास कर रहा है।
-
कॉल के साथ ETH भी भेजा गया था।
इसकी अनुमति नहीं है क्योंकि
withdrawएक पेएबल (payable) फंक्शन नहीं है। -
कॉलर को वापस ETH ट्रांसफर विफल हो गया।
इस स्थिति को
g_lowLevelCallFailघोस्ट वेरिएबल का उपयोग करके लो-लेवलCALLपरिणाम के माध्यम से ट्रैक किया जाता है।
assert isLastReverted <=> (
amount > wethBalanceBefore || // insufficient balance: withdrawal amount exceeds weth balance
e.msg.value != 0 || // non-payable: ETH was sent to a non-payable function
g_lowLevelCallFail // transfer failure: low-level call ETH transfer failed
);
यहाँ withdraw_revert रूल के लिए वेरीफाई किया गया Prover run है।
इनवेरिएंट: कुल ETH डिपॉजिट WETH की कुल सप्लाई से अधिक या उसके बराबर है (solvency)
यूज़र्स को अपने WETH का उपयोग करके सफलतापूर्वक ETH रिडीम करने के लिए, कॉन्ट्रैक्ट द्वारा रखे गए ETH को हमेशा कुल WETH सप्लाई से अधिक या उसके बराबर होना चाहिए। यहाँ वह CVL इनवेरिएंट है जो इस प्रॉपर्टी को कैप्चर करता है:
invariant ethDepositsAlwaysGTEWethTotalSupply()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
}
नीचे दी गई लाइन इनवेरिएंट को व्यक्त करती है:
nativeBalances[currentContract] >= totalSupply()
हालाँकि, यह इनवेरिएंट सार्वभौमिक रूप से लागू नहीं होता है। यह केवल preserved ब्लॉक्स में परिभाषित विशिष्ट स्थितियों के तहत लागू होता है। नीचे दिए गए प्रिज़र्व्ड (preserved) ब्लॉक में यह आवश्यक है कि कॉलर (e.msg.sender) currentContract के बराबर न हो।
preserved with (env e) {
require e.msg.sender != currentContract;
}
यह कोई संयोग नहीं है कि यह require कंडीशन निम्नलिखित रूल्स में दिखाई देती है:
deposit_ethDepositedEqualsWethReceived()withdraw_ethWithdrawnEqualsWETHReduced()
यह स्पष्ट है कि यह ETH डिपॉजिट और WETH जारी करने के बीच अकाउंटिंग से संबंधित है। यदि कॉन्ट्रैक्ट स्वयं को कॉल करता है और ETH डिपॉजिट करता है, तो कोई शुद्ध ETH लाभ नहीं होता है, लेकिन WETH अभी भी मिंट हो सकता है, जिसके कारण totalSupply वास्तविक ETH डिपॉजिट से अधिक हो जाती है।
अगले preserved ब्लॉक में यह आवश्यक है कि msg.sender का बैलेंस totalSupply() से कम या उसके बराबर हो, जो विथड्रॉ ऑपरेशन को अंडरफ्लो पैदा करने से रोकता है:
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
यह कोई आश्चर्य की बात नहीं है कि यह स्थिति एक संबंधित रूल में फिर से दिखाई देती है। हालाँकि यह यहाँ withdraw() के लिए एक प्रिज़र्व्ड कंडीशन के रूप में दिखाई देती है, यह पहले withdraw_ethWithdrawDecreasesWETHSupply रूल में एक प्रीकंडीशन के रूप में दिखाई दी थी।
दोनों ही मामलों में, उद्देश्य अंडरफ्लो-संबंधित काउंटरएक्ज़ाम्पल्स (counterexamples) को रोकना है। यह स्थिति को एक इनवेरिएंट के रूप में साबित करने का एक मजबूत कारण है, जो हम अगले सेक्शन में करेंगे।
यहाँ ethDepositsAlwaysGTEWethTotalSupply इनवेरिएंट के लिए वेरीफाई किया गया Prover run है।
इनवेरिएंट: कोई भी अकाउंट बैलेंस WETH कुल सप्लाई से अधिक नहीं है
यह इनवेरिएंट, जिसे balanceOf(address) <= totalSupply() के रूप में व्यक्त किया गया है, निम्नलिखित की गारंटी देता है:
- कोई भी अकाउंट बैलेंस कभी भी कुल सप्लाई से अधिक नहीं होता है।
- परिणामस्वरूप, चूँकि
totalSupply()स्वयंmax_uint256से अधिक नहीं हो सकता है, इसलिए व्यक्तिगत अकाउंट बैलेंस भी ओवरफ्लो नहीं हो सकते हैं।
जिन पिछले रूल्स पर हमने चर्चा की थी, उनमें ओवरफ्लो से बचाव के लिए निम्नलिखित प्रीकंडीशन्स पेश किए गए थे:
rule deposit_ethDepositedEqualsWethReceived(env e) {
...
require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // precondition
...
}
rule deposit_revert(env e) {
...
require balanceOf(caller) + ethDeposit <= max_uint256; // precondition
...
}
नीचे दिए गए withdraw रूल में, अंडरफ्लो से बचाव के लिए प्रीकंडीशन जोड़ी गई थी:
rule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
...
require balanceOf(e.msg.sender) <= totalSupply(); // precondition
...
}
नीचे दिए गए ethDepositsAlwaysGTEWethTotalSupply इनवेरिएंट में, इसका उपयोग अंडरफ्लो से बचाव के लिए एक प्रिज़र्व्ड कंडीशन के रूप में भी किया जाता है:
invariant ethDepositsAlwaysGTEWethTotalSupply()
nativeBalances[currentContract] >= totalSupply()
{
...
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
}
नीचे दिया गया इनवेरिएंट यह फॉर्मली वेरीफाई करके इन आवर्ती प्रीकंडीशन्स को सीधे संबोधित करता है कि कोई भी अकाउंट बैलेंस कभी भी कुल सप्लाई से अधिक नहीं होता है:
invariant noAccountBalanceExceedsTotalSupply(env e1)
balanceOf(e1.msg.sender) <= totalSupply()
filtered {
f -> f.selector != sig:transfer(address,uint256).selector && // excludes standard ERC-20 transfer function from this invariant
f.selector != sig:transferFrom(address,address,uint256).selector // excludes standard ERC-20 transferFrom function from this invariant
}
{
preserved withdraw(uint256 amount) with (env e2) {
require e1.msg.sender == e2.msg.sender;
}
}
आइए इसे समझते हैं।
नीचे दी गई लाइन इनवेरिएंट है:
balanceOf(e1.msg.sender) <= totalSupply()
हम filtered का उपयोग करके transfer() और transferFrom() को फ़िल्टर (filter) करते हैं क्योंकि ये फंक्शन्स अकाउंट बैलेंस के लिए मैपिंग वेरिएबल का उपयोग करने के बजाय स्टोरेज स्लॉट की गणना करते हैं और उसमें लिखते हैं। इसलिए, अकाउंट बैलेंस को ट्रैक करने के लिए CVL समरीज़ (summaries) का उपयोग करके इन फंक्शन्स को समराइज़ करने की आवश्यकता होगी (एक विषय जो इस अध्याय के दायरे से बाहर है)।
filtered {
f -> f.selector != sig:transfer(address,uint256).selector &&
f.selector != sig:transferFrom(address,address,uint256).selector
}
transfer() और transferFrom() को फ़िल्टर करना उचित है, क्योंकि केवल deposit() और withdraw() (जो क्रमशः _mint() और _burn() को इनवोक करते हैं) इनवेरिएंट को प्रभावित कर सकते हैं। transfer() और transferFrom() केवल उन टोकन्स को मूव करते हैं जो पहले से ही कुल सप्लाई में शामिल हैं। यदि कुल सप्लाई गलत है, तो समस्या deposit() या withdraw() से उत्पन्न होती है, न कि ट्रांसफर से।
यदि Solady WETH ने मैपिंग वेरिएबल्स का उपयोग किया होता (जो वह जानबूझकर डिज़ाइन के अनुसार नहीं करता है), तो बैलेंस को ट्रैक करना और इस इनवेरिएंट को परिभाषित करना सीधा होता, और इन फ़िल्टर्स की आवश्यकता नहीं होती।
इसके बावजूद, प्रीकंडीशन्स और प्रिज़र्व्ड ब्लॉक्स की तरह, फ़िल्टर्स का उपयोग सावधानी के साथ किया जाना चाहिए, क्योंकि वे संभावित रूप से वास्तविक बग्स (bugs) को छिपा सकते हैं।
अंत में, प्रिज़र्व्ड ब्लॉक के लिए आवश्यक है कि e1.msg.sender (वह एड्रेस जिसका बैलेंस हम इनवेरिएंट में चेक कर रहे हैं) withdraw फंक्शन के एग्जीक्यूशन के दौरान कॉलर के बराबर हो:
{
preserved withdraw(uint256 amount) with (env e2) {
require e1.msg.sender == e2.msg.sender;
}
}
प्रिज़र्व्ड कंडीशन require e1.msg.sender == e2.msg.sender Prover को उस अकाउंट पर इनवेरिएंट का परीक्षण करने से रोकती है जो withdraw() को कॉल नहीं करता है।
withdraw() फंक्शन एक बर्न को ट्रिगर करता है, जो केवल कॉलर के बैलेंस को कम करते हुए कुल सप्लाई को कम करता है। यदि इनवेरिएंट एक अलग अकाउंट की जाँच करता है जिसका बैलेंस नहीं बदलता है, तो Prover बर्न के बाद balanceOf(differentAccount) > totalSupply() देख सकता है और एक फाल्स वॉयलेशन (false violation) की रिपोर्ट कर सकता है।
इनवेरिएंट को उसी एड्रेस का पालन करने की आवश्यकता बनाकर जो withdraw() को एग्जीक्यूट करता है, प्रिज़र्व्ड ब्लॉक यह लागू करता है कि जाँच उस अकाउंट पर लागू होती है जिसका बैलेंस वास्तव में कम हो जाता है।
यहाँ वेरीफाई किया गया Prover run है।
प्रीकंडीशन्स को requireInvariant से बदलें
चूँकि noAccountBalanceExceedsTotalSupply() अब फॉर्मली वेरीफाई हो गया है, इसलिए हम निम्नलिखित स्पेसिफिकेशन्स में प्रीकंडीशन्स और प्रिज़र्व्ड कंडीशन्स को इस इनवेरिएंट से बदल सकते हैं:
rule deposit_ethDepositedEqualsWethReceived()rule deposit_revert()rule withdraw_ethWithdrawDecreasesWETHSupply()invariant ethDepositsAlwaysGTEWethTotalSupply()
यहाँ requireInvariant का उपयोग करते हुए रिफैक्टर्ड (refactored) रूल्स और इनवेरिएंट दिए गए हैं:
rule deposit_ethDepositedEqualsWethReceived_withInvariant(env e) {
require e.msg.sender != currentContract;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}
rule deposit_revert_withInvariant(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}
rule withdraw_ethWithdrawDecreasesWETHSupply_withInvariant(env e) {
uint256 amount;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}
invariant ethDepositsAlwaysGTEWethTotalSupply_withInvariant()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
requireInvariant noAccountBalanceExceedsTotalSupply(e);
}
}
और यहाँ इन रूल्स और इनवेरिएंट के लिए वेरीफाई किया गया Prover run है।
पूर्ण CVL स्पेसिफिकेशन और Prover रन
यहाँ इस अध्याय में लिखा गया पूर्ण स्पेसिफिकेशन है:
methods {
function balanceOf(address) external returns (uint256) envfree;
function totalSupply() external returns (uint256) envfree;
}
persistent ghost bool g_lowLevelCallFail;
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
if (rc == 0) {
g_lowLevelCallFail = true;
} else {
g_lowLevelCallFail = false;
}
}
rule deposit_ethDepositedEqualsWethReceived(env e) {
require e.msg.sender != currentContract;
require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // will be replaced by an invariant
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}
rule deposit_ethDepositedEqualsWethReceived_withInvariant(env e) {
require e.msg.sender != currentContract;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
deposit(e);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}
rule deposit_ethDepositIncreasesWETHTotalSupply(env e) {
mathint totalSupplyBefore = totalSupply();
deposit(e);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore + e.msg.value;
}
rule deposit_revert(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}
rule deposit_revert_withInvariant(env e) {
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];
deposit@withrevert(e);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
ethBalanceBefore < ethDeposit ||
totalSupplyBefore + ethDeposit > max_uint256
);
}
rule withdraw_ethWithdrawnEqualsWETHReduced(env e) {
uint256 amount;
require e.msg.sender != currentContract;
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw(e,amount);
mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);
assert ethBalanceAfter == ethBalanceBefore + amount;
assert wethBalanceAfter == wethBalanceBefore - amount;
}
rule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
uint256 amount;
require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}
rule withdraw_ethWithdrawDecreasesWETHSupply_withInvariant(env e) {
uint256 amount;
requireInvariant noAccountBalanceExceedsTotalSupply(e);
mathint totalSupplyBefore = totalSupply();
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();
assert totalSupplyAfter == totalSupplyBefore - amount;
}
rule withdraw_revert(env e) {
uint256 amount; // the amount of eth to claim
mathint wethBalanceBefore = balanceOf(e.msg.sender);
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
amount > wethBalanceBefore ||
e.msg.value != 0 ||
g_lowLevelCallFail
);
}
invariant ethDepositsAlwaysGTEWethTotalSupply()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
require balanceOf(e.msg.sender) <= totalSupply();
}
}
invariant ethDepositsAlwaysGTEWethTotalSupply_withInvariant()
nativeBalances[currentContract] >= totalSupply()
{
preserved with (env e) {
require e.msg.sender != currentContract;
}
preserved withdraw(uint256 amount) with (env e) {
requireInvariant noAccountBalanceExceedsTotalSupply(e);
}
}
invariant noAccountBalanceExceedsTotalSupply(env e1)
balanceOf(e1.msg.sender) <= totalSupply()
filtered {
f -> f.selector != sig:transfer(address,uint256).selector &&
f.selector != sig:transferFrom(address,address,uint256).selector
}
{
preserved withdraw(uint256 amount) with (env e2) {
require e1.msg.sender == e2.msg.sender;
}
}
यहाँ इस अध्याय में चर्चा किए गए WETH स्पेसिफिकेशन का वेरीफाई किया गया Prover run है।
यह लेख formal verification using the Certora Prover पर एक सीरीज़ का हिस्सा है।