परिचय
पिछले अध्यायों में, हमने उन स्टोरेज वैल्यूज़ और मात्राओं को रिकॉर्ड करने के लिए घोस्ट वेरिएबल्स (ghost variables) (Sstore हुक्स के माध्यम से) का उपयोग किया था जिन्हें स्मार्ट कॉन्ट्रैक्ट्स में स्पष्ट रूप से ट्रैक नहीं किया गया था — उदाहरण के लिए, सभी बैलेंसेस का योग। वे वेरिफिकेशन के दौरान समय के साथ स्टेट या स्टेट वेरिएबल्स के बीच के संबंधों में बदलाव को देखने और तर्क करने की अनुमति देते हैं।
हालाँकि, किसी कॉन्ट्रैक्ट मेथड को कॉल किए जाने के बाद रूल के निष्पादन (rule execution) के दौरान, घोस्ट वेरिएबल्स को:
- havoc किया जा सकता है जब Prover को कोई अनरिज़ॉल्व्ड एक्सटर्नल कॉल (unresolved external call) मिलता है, या
- कॉल के रिवर्ट (revert) होने पर उनकी पिछली स्टेट में रोल बैक (रीसेट) किया जा सकता है।
अनरिज़ॉल्व्ड एक्सटर्नल कॉल के दौरान घोस्ट्स havoc हो जाते हैं क्योंकि Prover कॉल किए गए कॉन्ट्रैक्ट का इम्प्लीमेंटेशन नहीं देख सकता है। चूंकि एक्सटर्नल कॉन्ट्रैक्ट संभावित रूप से कॉलर को वापस कॉल कर सकता है और स्टोरेज को मॉडिफाई कर सकता है, इसलिए Prover इस बात को खारिज नहीं कर सकता कि घोस्ट वेरिएबल्स को उनके हुक्स के माध्यम से अपडेट किया जा सकता है। इस अनिश्चितता को संभालने के लिए, Prover घोस्ट वेरिएबल्स को नॉन-डिटरमिनिस्टिक (nondeterministic) वैल्यूज़ असाइन करता है।
जब कोई कॉल रिवर्ट होती है, तो घोस्ट्स नॉन-डिटरमिनिस्टिक नहीं होते हैं। इसके बजाय, वे कॉल शुरू होने से पहले की वैल्यू पर रोल बैक (रीसेट) हो जाते हैं। Certora docs के अनुसार, “Ghosts को वेरिफिकेशन के अधीन कॉन्ट्रैक्ट्स की स्टेट के विस्तार के रूप में देखा जा सकता है। इसका मतलब यह है कि यदि कोई कॉल रिवर्ट होती है, तो घोस्ट वैल्यूज़ अपनी प्री-स्टेट (pre-state) में रिवर्ट हो जाएंगी।”
ये घोस्ट्स के डिफ़ॉल्ट व्यवहार हैं: वे अनरिज़ॉल्व्ड कॉल्स में havoc हो जाते हैं और मेथड कॉल के रिवर्ट होने पर रीसेट हो जाते हैं। हालाँकि, एक विशेष प्रकार का घोस्ट होता है जिसे persistent ghost कहा जाता है, जो अनरिज़ॉल्व्ड एक्सटर्नल कॉल्स और रिवर्ट्स दोनों के दौरान अपनी वैल्यू बनाए रखता है (havoc नहीं होता है)।
इस अध्याय में, हम यह प्रदर्शित करेंगे कि persistent ghosts कैसे काम करते हैं, वे रेगुलर घोस्ट्स से कैसे अलग हैं, उनका उपयोग कब करना चाहिए और कब नहीं।
persistent ghost डिक्लेयर करना
एक persistent ghost को persistent कीवर्ड के साथ डिक्लेयर किया जाता है, जैसा कि नीचे दिखाया गया है:
persistent ghost bool g_flag;
persistent ghost uint256 g_count;
पढ़ने में आसानी के लिए, हम इस लेख में सभी घोस्ट वेरिएबल्स के लिए g_ प्रीफ़िक्स का उपयोग करते हैं, हालाँकि उन्हें कोई भी नाम दिया जा सकता है।
persistent ghosts को विशिष्ट वैल्यूज़ के साथ इनिशियलाइज़ (initialize) करने के लिए, घोस्ट डिक्लेरेशन के भीतर init_state axiom जोड़ें:
persistent ghost bool g_flag {
init_state axiom g_flag == false;
}
persistent ghost uint256 g_count {
init_state axiom g_count == 0;
}
नोट: हालांकि अनरिज़ॉल्व्ड मेथड कॉल्स के दौरान persistent ghosts havoc नहीं होते हैं, वे रूल्स के लिए प्री-कॉल स्टेट में और इनवैरिएंट्स (invariants) के बेस केस (base case) में havoc हो जाते हैं; यही बात रेगुलर घोस्ट्स पर भी लागू होती है। इसलिए, उन्हें अभी भी रूल्स में एक पूर्व शर्त (precondition) के रूप में (require स्टेटमेंट्स के माध्यम से) ठीक से कंस्ट्रैन (constrain) किया जाना चाहिए और इनवैरिएंट्स के बेस केसेस के लिए init_state axiom का उपयोग करके इनिशियलाइज़ किया जाना चाहिए।
persistent बनाम regular ghosts का व्यवहार
नीचे दिया गया चित्र दिखाता है कि कैसे एक persistent ghost रिवर्टेड कॉल्स और अनरिज़ॉल्व्ड एक्सटर्नल कॉल्स में अपनी वैल्यू बनाए रखता है। रूल के निष्पादन के दौरान, जब कोई हुक ghostVar को कोई वैल्यू असाइन करता है, तो वह वैल्यू कभी भी रिवर्ट (रीसेट) या havoc नहीं होती है, इसलिए इसकी अंतिम स्टेट हमेशा हुक द्वारा असाइन की गई अंतिम वैल्यू को दर्शाती है:
persistent ghosts के विपरीत, रेगुलर घोस्ट्स अनरिज़ॉल्व्ड एक्सटर्नल कॉल्स पर havoc हो जाते हैं और रिवर्ट होने पर रीसेट हो जाते हैं:
नोट: persistent और regular दोनों घोस्ट्स केवल एक सिंगल रूल निष्पादन के भीतर अपनी वैल्यू बनाए रखते हैं और रूल्स के बीच कैरी ओवर (carry over) नहीं होते हैं। अंतर यह है कि persistent ghosts उस निष्पादन के भीतर अनरिज़ॉल्व्ड या रिवर्टेड कॉल्स के दौरान भी बचे रहते हैं, जबकि रेगुलर घोस्ट्स नहीं।
persistent ghosts के साथ रिवर्ट्स को ट्रैक करना
यह अनुभाग प्रदर्शित करता है कि कैसे persistent ghosts ऐसे तरीके से रिवर्ट्स को ट्रैक करने में सक्षम बनाते हैं जो रेगुलर घोस्ट्स नहीं कर सकते। यह बताता है कि इस उपयोग के मामले (use case) में रेगुलर घोस्ट्स क्यों विफल होते हैं और दिखाता है कि persistent ghosts इस समस्या को कैसे हल करते हैं।
मेथड कॉल के रिवर्ट होने पर regular ghost रीसेट हो जाता है
जब कोई मेथड रिवर्ट होता है, तो रेगुलर घोस्ट्स की स्टेट भी रोल बैक हो जाती है। यह व्यवहार इस बात से मेल खाता है कि कैसे विफल कॉल के दौरान स्टोरेज वेरिएबल्स अपनी पिछली वैल्यूज़ पर रिवर्ट हो जाते हैं।
इस व्यवहार को स्पष्ट करने के लिए, इस कॉन्ट्रैक्ट SimpleVault पर विचार करें, जहाँ यूज़र्स ETH जमा (deposit) और निकाल (withdraw) सकते हैं:
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract SimpleVault {
mapping(address => uint256) public balanceOf;
/// deposit ETH into the vault
function deposit() external payable {
balanceOf[msg.sender] += msg.value;
}
/// withdraw ETH from the vault
function withdraw(uint256 amount) external {
require(balanceOf[msg.sender] >= amount, "Insufficient balance");
balanceOf[msg.sender] -= amount;
(bool success, ) = msg.sender.call{value: amount}("");
require(success, "ETH transfer failed");
}
}
लक्ष्य यह वेरिफाई करना है कि withdraw() ठीक इन्हीं मामलों में रिवर्ट होता है:
- निकासी (withdrawal) की राशि जमा किए गए बैलेंस से अधिक हो (
amount > balanceBefore) - एक नॉन-ज़ीरो
msg.valueको इस नॉन-पेएबल (non-payable) फ़ंक्शन में भेजा जाता है (e.msg.value != 0) - ETH ट्रांसफर विफल हो जाता है, या लो-लेवल कॉल (low-level call) ने false रिटर्न किया हो
यह अनुभाग विशेष रूप से तीसरे मामले पर केंद्रित है: ETH ट्रांसफर विफलताओं को ट्रैक करना।
निम्नलिखित रूल “Account Balances” अध्याय से एक एस्सर्शन पैटर्न (assertion pattern) को लागू करता है। यह बाइकंडीशनल ऑपरेटर (<=>) का उपयोग करता है और सभी अपेक्षित रिवर्ट शर्तों को अलग-अलग (||) सूचीबद्ध करता है। यह सभी संभावित मेथड रिवर्ट्स का हिसाब रखता है यदि और केवल यदि इनमें से कोई एक शर्त होती है:
ghost bool g_lowLevelCallSuccess; // regular ghost
rule withdraw_revert(env e) {
uint256 amount;
require g_lowLevelCallSuccess; // by requiring it to be true initially, you can detect when it becomes false during execution
mathint balanceBefore = balanceOf(e.msg.sender);
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
amount > balanceBefore || // insufficient balance: withdrawal amount exceeds user balance
e.msg.value != 0 || // non-payable: ETH was sent to this non-payable function
!g_lowLevelCallSuccess // transfer failure: low-level call ETH transfer failed
);
}
ETH ट्रांसफर के परिणाम को ट्रैक करने के लिए, हम एक CALL हुक का उपयोग करते हैं; एक CVL फ़ीचर जो लो-लेवल EVM CALL इंस्ट्रक्शन की निगरानी करता है और इसके रिटर्न कोड को कैप्चर करता है। हम इस रिटर्न कोड को g_lowLevelCallSuccess को असाइन करते हैं (विफलता के लिए 0, सफलता के लिए 1):
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
if (returnCode == 0) {
g_lowLevelCallSuccess = false;
} else {
g_lowLevelCallSuccess = true;
}
}
यहाँ पूरी स्पेसिफिकेशन दी गई है:
methods {
function balanceOf(address) external returns uint256 envfree;
}
ghost bool g_lowLevelCallSuccess;
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
if (returnCode == 0) {
g_lowLevelCallSuccess = false;
} else {
g_lowLevelCallSuccess = true;
}
}
rule withdraw_revert(env e) {
uint256 amount;
require g_lowLevelCallSuccess;
mathint balanceBefore = balanceOf(e.msg.sender);
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
amount > balanceBefore || // insufficient balance: withdrawal amount exceeds user balance
e.msg.value != 0 || // non-payable: ETH was sent to this non-payable function
!g_lowLevelCallSuccess // transfer failure: low-level call ETH transfer failed
);
}
रेगुलर घोस्ट्स का उपयोग करने पर, वेरिफिकेशन विफल हो जाता है:
विफल Prover रन देखें: link
आइए जांचें कि विफलता क्यों हुई।
Regular ghost वैल्यू रीसेट — कॉल ट्रेस
वेरिफिकेशन विफल हो जाता है क्योंकि g_lowLevelCallSuccess एक रेगुलर घोस्ट है जो रिवर्ट होने पर रीसेट हो जाता है। CALL हुक विफलता (returnCode == 0) को कैप्चर करता है, लेकिन जब withdraw रिवर्ट होता है, तो घोस्ट रीसेट हो जाता है और इस वैल्यू को खो देता है।
जैसा कि नीचे दी गई छवि में दिखाया गया है, withdraw() मेथड को कॉल किए जाने से पहले (प्री-कॉल स्टेट में) g_lowLevelCallSuccess, true होता है:
जब लो-लेवल ETH ट्रांसफर कॉल विफल हो जाता है, तो CALL हुक विफल कॉल (0 की रिटर्न वैल्यू) को कैप्चर करता है, जो g_lowLevelCallSuccess को false पर सेट कर देता है:
जब CALL ऑपकोड (CVL CALL हुक द्वारा कैप्चर किया गया) शून्य (zero) रिटर्न करता है, तो इसका मतलब है कि ETH ट्रांसफर विफल हो गया है। रूल के भीतर, जब withdraw@withrevert(e, amount) का इन्वोकेशन रिवर्ट होता है, तो घोस्ट अपनी प्री-कॉल स्टेट में रीसेट हो जाता है। नीचे दी गई छवि दिखाती है कि विफल ट्रांसफर के बावजूद घोस्ट true पर वापस आ रहा है:
persistent ghost के साथ स्पेसिफिकेशन को ठीक करना
रेगुलर घोस्ट के साथ कॉल ट्रेस में हमने जो देखा उसे संक्षेप में बताने के लिए, निष्पादन इस प्रकार होता है:
- घोस्ट
g_lowLevelCallSuccessकोtrueपर इनिशियलाइज़ किया जाता है (requireस्टेटमेंट के माध्यम से)। withdrawफ़ंक्शन निष्पादित होता है और एक लो-लेवलCALLको ट्रिगर करता है जो विफल हो जाता है।CALLहुक विफलता (returnCode == 0) का पता लगाता है औरg_lowLevelCallSuccessकोfalseपर सेट करता है।withdrawफ़ंक्शन रिवर्ट हो जाता है क्योंकिrequire(success)तब विफल होता है जबsuccess,falseहोता है।- रिवर्ट के कारण घोस्ट अपनी प्री-कॉल स्टेट
trueपर रीसेट हो जाता है।
मुख्य समस्या स्पष्ट है: चरण 5 में रिवर्ट घोस्ट को वापस true पर रीसेट कर देता है, जिससे चरण 3 में ट्रांसफर विफलता को रिकॉर्ड करने वाली false वैल्यू मिट जाती है।
इसे ठीक करने के लिए, घोस्ट को persistent के रूप में डिक्लेयर करें ताकि CALL हुक द्वारा असाइन की गई बूलियन वैल्यू रिवर्ट के दौरान भी बची रहे और रूल में एक्सेसिबल रहे:
methods {
function balanceOf(address) external returns uint256 envfree;
}
persistent ghost bool g_lowLevelCallSuccess;
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
if (returnCode == 0) {
g_lowLevelCallSuccess = false;
} else {
g_lowLevelCallSuccess = true;
}
}
rule withdraw_revert(env e) {
uint256 amount;
require g_lowLevelCallSuccess;
mathint balanceBefore = balanceOf(e.msg.sender);
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;
assert isLastReverted <=> (
amount > balanceBefore || // insufficient balance: withdrawal amount exceeds user balance
e.msg.value != 0 || // non-payable: ETH was sent to this non-payable function
!g_lowLevelCallSuccess // transfer failure: low-level call ETH transfer failed
);
}
जैसी कि उम्मीद थी, रूल वेरिफाई हो जाता है:
Prover रन: link
persistent ghost के साथ, हमने रिवर्ट के बावजूद लो-लेवल कॉल ETH ट्रांसफर विफलता को सफलतापूर्वक ट्रैक किया, जो रेगुलर घोस्ट के साथ असंभव था। यह उदाहरण persistent ghosts के लिए एक उचित उपयोग का मामला दिखाता है: उस स्टेट जानकारी को कैप्चर करना जो अन्यथा रिवर्ट के दौरान नष्ट हो जाती।
persistent ghosts का उपयोग कब नहीं करना चाहिए
persistent ghosts के लिए एक उचित उपयोग का मामला देखने के बाद, यह समझना भी उतना ही महत्वपूर्ण है कि उनका उपयोग कब नहीं किया जाना चाहिए।
एक रेगुलर घोस्ट में persistent कीवर्ड जोड़ने की सरलता इसे दुरुपयोग (misuse) के प्रति संवेदनशील बनाती है। जब आपको यह देखने की आवश्यकता हो कि रिवर्ट किए गए या अनरिज़ॉल्व्ड निष्पादन में क्या होता है, तब जानबूझकर persistent ghosts का उपयोग करें — न कि रूल्स या इनवैरिएंट्स के वेरिफाई होने में विफल रहने पर एक अस्थायी समाधान (workaround) के रूप में।
दुरुपयोग की समस्या को प्रदर्शित करने के लिए, आइए एक ऐसे ही वॉल्ट पर विचार करें जो ETH के बजाय ERC-20 टोकन स्वीकार करता है। इसकी बैलेंस मैपिंग प्राइवेट है, इसलिए आंतरिक बैलेंसेस को मिरर करने के लिए एक घोस्ट वेरिएबल की आवश्यकता है क्योंकि पढ़ने के लिए कोई गेटर (getter) फ़ंक्शन नहीं है:
/// minimal ERC20 interface
interface IERC20 {
function transfer(address to, uint256 amount) external returns (bool);
...
}
contract SimpleVault20 {
IERC20 public immutable token;
mapping(address => uint256) private balanceOf;
constructor(address _token) {
token = IERC20(_token);
}
function deposit(uint256 amount) external {
require(amount > 0, "Zero deposit");
balanceOf[msg.sender] += amount;
require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
}
...
}
आइए deposit() फ़ंक्शन के लिए स्पेसिफिकेशन्स लिखें। घोस्ट और हुक्स के लिए:
- घोस्ट को रेगुलर घोस्ट के रूप में डिक्लेयर करें
- प्रति अकाउंट जमाकर्ता के बैलेंसेस में बदलावों को ट्रैक करने के लिए
Sstoreहुक को लागू करें - स्टोरेज और घोस्ट के रीड्स को सिंक करने के लिए
Sloadहुक लागू करें
ghost mapping(address => mathint) g_balanceOf;
hook Sstore balanceOf[KEY address account] uint256 newVal (uint256 oldVal) {
g_balanceOf[account] = g_balanceOf[account] + newVal - oldVal;
}
hook Sload uint256 balance balanceOf[KEY address account] {
require g_balanceOf[account] == balance;
}
रूल के लिए, हम यह वेरिफाई करते हैं कि कोई राशि (depositAmount) जमा करने पर वह वॉल्ट में भेजने वाले के बैलेंस में सही ढंग से क्रेडिट हो जाती है:
rule deposit(env e) {
uint256 depositAmount;
require currentContract != e.msg.sender;
require g_balanceOf[e.msg.sender] == 0;
deposit(e, depositAmount);
assert g_balanceOf[e.msg.sender] == depositAmount;
}
आइए वेरिफिकेशन चलाएं। चूँकि deposit फ़ंक्शन एक अज्ञात ERC-20 इम्प्लीमेंटेशन को कॉल करता है (जो havoc का कारण बनेगा), इसलिए हमें उम्मीद है कि यह विफल हो जाएगा:
Prover रन: link
वेरिफिकेशन विफल क्यों हुआ
मुख्य कारण SimpleVault20 कॉन्ट्रैक्ट की निम्नलिखित लाइन में है, जहाँ यह एक अज्ञात ERC-20 इम्प्लीमेंटेशन को कॉल करता है:
contract SimpleVault20 {
...
function deposit(uint256 amount) external {
require(amount > 0, "Zero deposit");
balanceOf[msg.sender] += amount;
// `token` is an unknown ERC-20 implementation
require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
}
...
}
नीचे दी गई छवि में, हम देखते हैं कि Prover ने depositAmount को 0xa (या 10) वैल्यू असाइन की, जिसे बाद में Sstore हुक के माध्यम से घोस्ट मैपिंग वेरिएबल g_balanceOf[address] में पास किया गया:
फिर एक एक्सटर्नल कॉन्ट्रैक्ट को कॉल के दौरान घोस्ट havoc हो गया क्योंकि इसका इम्प्लीमेंटेशन अज्ञात था:
havoc एरर को देखकर, कोई इसे छिपाने के लिए persistent कीवर्ड जोड़ने के लिए ललचा सकता है। हालाँकि इससे वेरिफिकेशन पास हो जाता है, लेकिन यह वास्तविक समस्या को छुपाता है: हम नहीं जानते कि एक्सटर्नल ERC-20 कॉन्ट्रैक्ट को कैसे इम्प्लीमेंट किया गया है:
Prover रन: link
Prover गलत धारणा के साथ वेरिफाई करता है
Prover रूल को वेरिफाईड के रूप में दिखाता है, लेकिन यह एक गलत धारणा (assumption) पर आधारित है। एक persistent घोस्ट का उपयोग करके, स्पेसिफिकेशन यह मान लेता है कि ERC-20 इम्प्लीमेंटेशन कभी भी कॉलिंग कॉन्ट्रैक्ट के स्टोरेज को रिवर्ट या मॉडिफाई नहीं करता है। इसलिए, यह msg.sender को 0xa (या 10) की राशि क्रेडिट करता है, भले ही ट्रांसफर वास्तव में विफल हो सकता है:
यह प्रदर्शित करता है कि इस मामले में persistent घोस्ट का उपयोग करना भ्रामक क्यों है: यह एक्सटर्नल कॉन्ट्रैक्ट के व्यवहार की अनिश्चितता को नज़रअंदाज़ करता है, संभावित बग्स को उजागर करने के बजाय उन्हें छिपाता है।
वास्तविक टोकन इम्प्लीमेंटेशन वॉल्ट से लिंक्ड होना चाहिए
उचित समाधान persistent ghost का उपयोग करना नहीं है। इसके बजाय, हमें scene में एक ज्ञात ERC-20 इम्प्लीमेंटेशन को “लिंक” (link) करना चाहिए — चाहे वह प्रोटोकॉल का अपना ERC20, WETH, DAI हो, या कोई भी ERC-20 टोकन जिसका कोड उपलब्ध हो।
लिंकिंग Prover को एक्सटर्नल कॉल्स के लिए वेरिफिकेशन सीन में शामिल वास्तविक कॉन्ट्रैक्ट इम्प्लीमेंटेशन का उपयोग करने का निर्देश देती है, बजाय इसके कि उन कॉल्स को havoc व्यवहार के रूप में माना जाए।
SimpleVault20 के लिए, टोकन एड्रेस इम्यूटेबल है, जिसका अर्थ है कि उपयोग किए जाने वाले ERC-20 को डिप्लॉयमेंट के समय जाना जाता है और यह कॉन्ट्रैक्ट के पूरे जीवनकाल में नहीं बदलेगा। इसलिए, हम सीन में ERC-20 कॉन्ट्रैक्ट को जोड़कर और स्पेसिफिकेशन में इसे कॉन्फ़िगर करके इसे एक ERC-20 इम्प्लीमेंटेशन से “बाध्य” (bind) करने के लिए link का उपयोग कर सकते हैं। यह Prover को वास्तविक टोकन इम्प्लीमेंटेशन के विरुद्ध SimpleVault20 कॉन्ट्रैक्ट को वेरिफाई करने की अनुमति देता है। अन्यथा, लिंकिंग के बिना, Prover टोकन के साथ वॉल्ट के इंटरेक्शन को सटीक रूप से वेरिफाई नहीं कर सकता है, जिससे ऊपर दिखाए गए अनुसार फॉल्स पॉज़िटिव्स (false positives) आते हैं।
link पर अधिक जानकारी के लिए, Certora डॉक्यूमेंटेशन देखें: [1, 2]
सारांश
- Persistent ghosts, havoc और रिवर्ट्स के दौरान बचे रहते हैं, जबकि रेगुलर घोस्ट्स अज्ञात कॉन्ट्रैक्ट्स को एक्सटर्नल कॉल्स के दौरान havoc हो जाते हैं और रिवर्ट्स के दौरान रीसेट हो जाते हैं।
- अज्ञात कॉन्ट्रैक्ट्स को एक्सटर्नल कॉल्स havoc का कारण बनते हैं क्योंकि Prover कॉली (callee) का इम्प्लीमेंटेशन नहीं देख सकता है, इसलिए यह सभी संभावित रिटर्न वैल्यूज़ और स्टोरेज प्रभावों का मॉडल बनाता है।
- persistent ghosts का एक उचित उपयोग CVL हुक्स से जानकारी कैप्चर करना है — जैसे कि
CALLरिटर्न कोड्स — जो विफल निष्पादन पथों में भी बचे रहने चाहिए, जैसे कि विफल लो-लेवल ETH ट्रांसफर्स को ट्रैक करना। - विफल होने वाले रूल्स को पास करने के लिए त्वरित फिक्स (quick fix) के रूप में
persistentकीवर्ड जोड़ना अज्ञात कॉन्ट्रैक्ट इम्प्लीमेंटेशन्स या अनरिज़ॉल्व्ड कॉल्स के प्रभावों को नज़रअंदाज़ करके वेरिफिकेशन की सफलता का झूठा आभास पैदा करता है।
यह लेख Certora Prover का उपयोग करके फॉर्मल वेरिफिकेशन (formal verification using the Certora Prover) पर एक सीरीज़ का हिस्सा है।