Certora CVL में Spec File को समझना। पिछले अध्याय में, हमने देखा कि Certora Prover का उपयोग करके formal verification करने के लिए, हमें Prover को निम्नलिखित प्रमुख चीजें प्रदान करने की आवश्यकता होती है: Smart...

Ownable.sol को औपचारिक रूप से सत्यापित करना Ownable एक एब्स्ट्रैक्ट कॉन्ट्रैक्ट है जो ओनर-आधारित एक्सेस कंट्रोल प्रदान करता है। जब इसे इनहेरिट किया जाता है, तो यह modifier का उपयोग करके विशिष्ट फ़ंक्शंस को ओनर तक सीमित कर देता है। इसमें तीन...

CVL में msg.sender और msg.value की टेस्टिंग परिचय इस अध्याय में, हम CVL में उस वेरिएबल का परिचय देते हैं, जो हमें उन फंक्शन्स के लिए नियम बनाने में सक्षम बनाता है जो , , और ... में अन्य ग्लोबल वेरिएबल्स पर निर्भर करते हैं।

Biconditional Operator का परिचय: Biconditional operator हमें boolean values के बीच if-and-only-if संबंधों को assert करने में सक्षम बनाता है। Implication () यह बताता है कि यदि condition P संतुष्ट होती है, तो Q...

एक Counter को औपचारिक रूप से सत्यापित करना पिछले अध्याय में, हमने औपचारिक सत्यापन के सैद्धांतिक पक्ष के बारे में सीखा, जिसमें यह क्या है और कैसे काम करता है, शामिल है। इस मॉड्यूल में, हम सिद्धांत से आगे बढ़ेंगे और सीखेंगे...

Implication Operator का परिचय Implication operator का उपयोग अक्सर statement के विकल्प के रूप में किया जाता है क्योंकि यह अधिक स्पष्ट होता है। निम्नलिखित उदाहरण पर विचार करें: एक function जो दो unsigned...

Method Properties का परिचय परिचय पिछले अध्याय में, हमने parametric rules के बारे में सीखा था, जो हमें उन properties को formally verify करने की अनुमति देते हैं जिनके हमेशा सत्य रहने की उम्मीद की जाती है, भले ही कोई भी...

Address Balance को Formally Verify करना: पिछले अध्याय में, हमने non-payable संदर्भों पर ध्यान केंद्रित करते हुए CVL में environment-dependent functions के बारे में तर्क (reason) करने के तरीके को कवर किया था। उन उदाहरणों में, एक्सेस...

Overflow और Mathint CVL में, प्रकार असीमित पूर्णांकों का प्रतिनिधित्व करता है, जो Solidity के निश्चित-आकार वाले प्रकारों जैसे कि . के विपरीत है। यह overflow या underflow के बिना अंकगणितीय संचालन करता है, जो ... के आधार पर तर्क करने की अनुमति देता है

CVL में सशर्त कथन और Solady तथा Solmate के कुछ हिस्सों का औपचारिक सत्यापन परिचय कुछ कॉन्ट्रैक्ट व्यवहार (प्रॉपर्टीज़) स्वाभाविक रूप से सशर्त होते हैं, और CVL में if/else जैसे कंस्ट्रक्ट्स का उपयोग करना...

Initializable.sol को औपचारिक रूप से सत्यापित करना यह लेख बताता है कि कैसे Certora ने Initializable.sol OpenZeppelin कॉन्ट्रैक्ट को औपचारिक रूप से सत्यापित किया। हम यह मानकर चलते हैं कि पाठक पहले से ही इस बात से परिचित हैं कि यह कॉन्ट्रैक्ट कैसे...

Cairo में Constructors एक constructor एक one-time-call function है जिसे contract deployment के दौरान state variables को initialize करने, contract setup कार्य करने, cross-contract interactions करने और... के लिए execute किया जाता है।