एक ERC-20 Token को Formally Verify करना - परिचय इस अध्याय में, हम Solmate के ERC-20 implementation को formally verify करते हैं, जिसमें निम्नलिखित शामिल हैं: Standard state-changing functions: , , Standard view...

Invariants में Ghosts को सीमित करना। पिछले अध्याय में, हमने देखा कि कैसे अनियंत्रित ghost variables, false positives का कारण बन सकते हैं। हमने यह भी सीखा कि कैसे एक statement का उपयोग प्रभावी रूप से सीमित करने के लिए किया जा सकता है...

Rules में Ghost Values को Constrain करना पिछले अध्याय में, हमने सीखा कि कैसे ghost variables जानकारी को hooks से rules में प्रवाहित होने देते हैं। हमने यह भी सीखा कि: Verification की शुरुआत में...

Storage Mappings के साथ Sstore Hooks का उपयोग करना परिचय: "Introduction to Storage Hooks And Ghosts" अध्याय में, हमने सरल storage variables के साथ storage hooks और ghosts पर चर्चा की थी। हमने दिखाया था कि...

ERC-721 के लिए आंशिक रूप से पैरामेट्रिक नियमों का परिचय। यह अध्याय OpenZeppelin के ERC-721 CVL स्पेसिफिकेशन के कोड वॉकथ्रू का अंतिम भाग (5/5) है, जो निम्नलिखित को औपचारिक रूप से सत्यापित करता है...

Storage Hooks और Ghosts का परिचय: यह अक्सर आवश्यक हो जाता है कि विशिष्ट storage स्थानों पर होने वाले बदलावों का निरीक्षण किया जाए ताकि यह साबित किया जा सके कि कोई property या invariant कायम है, खासकर तब जब storage...

Ghost और Hook का उपयोग करके Invariant को Verify करना: किसी भी सही ERC20 implementation में, सभी अकाउंट बैलेंस का योग हमेशा total token supply के बराबर होना चाहिए। यह property हमेशा सत्य रहनी चाहिए...

ERC-721 के लिए Mint और Burn के नियम परिचय ERC-721 non-fungible tokens के लिए Ethereum मानक है, जिसका व्यापक रूप से डिजिटल संपत्ति का प्रतिनिधित्व करने के लिए उपयोग किया जाता है। संपत्ति के किसी भी रूप की तरह, यह आपूर्ति के इर्द-गिर्द घूमता है...

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

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

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

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