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

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

Formal Verification का परिचय Formal verification गणितीय रूप से यह सिद्ध करने की प्रक्रिया है कि कोई प्रोग्राम किसी specification का पालन करता है। यह लेख वैचारिक रूप से इस बात का परिचय देता है कि formal verification कैसे...

Certora में Revert Call की टेस्टिंग इस अध्याय में, हम सीखेंगे कि स्मार्ट कॉन्ट्रैक्ट एग्जीक्यूशन में अपेक्षित reverts को सत्यापित करने के लिए CVL में method tags ( और ) और special variable का उपयोग कैसे किया जाता है। सेटअप करना...

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

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

Certora Require, Assert, और Satisfy पिछले अध्याय में, हमने सीखा कि स्पेसिफिकेशन CVL में लिखा गया कोड का एक हिस्सा होता है जो किसी स्मार्ट कॉन्ट्रैक्ट के अपेक्षित व्यवहार का वर्णन करता है। एक...

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

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

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

OpenZeppelin में Nonces.Sol को औपचारिक रूप से सत्यापित करना। Nonces, जिसका अर्थ "number used once" है, का उपयोग replay attacks को रोकने के लिए डिजिटल सिग्नेचर योजनाओं में किया जाता है। इस लेख के प्रयोजनों के लिए, हम यह मान लेते हैं...

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