汇编与 EVM 课程 - NFT 市场 gas 优化

视频 AI 总结：

该视频是 Assembly EVM Op Codes 和 Formal Verification 课程的最后一部分，旨在帮助学习者掌握汇编和形式化验证技术。视频的核心内容是演示如何使用形式化验证工具 Certora 来验证一个用 Solidity 编写的 NFT 市场合约和一个用汇编重写的、更节省 Gas 的版本是否等价。通过这个过程，学习者可以学习到如何确保汇编代码在功能上与 Solidity 参考实现一致，从而构建更高效的智能合约。

视频中提出的关键信息：

• CodeHawks 平台： 学习者可以在完成课程后参与 codehawks 上的形式化验证竞赛，并有机会获得报酬。
• Gas Bad NFT Marketplace 项目： 该项目包含一个用 Solidity 编写的 NFT 市场合约（nft_marketplace.sol）和一个用汇编重写的版本（gas_bad_nft_marketplace.sol），汇编版本旨在节省 Gas 费用。
• 形式化验证目标： 视频将演示如何使用 Certora 验证以下两点：
  • 每当映射（mapping）被更新时，都会发出一个事件（event）。
  • Gas Bad NFT Marketplace 和 NFT Marketplace 在调用任何函数后，最终状态是相同的（除了 Gas 消耗的差异）。
• Certora 的使用： 视频将从头开始编写 Certora 的配置文件和规范文件，并介绍以下概念：
  • Ghost 变量： 用于在验证过程中定义额外的变量，以便在规则和Hook之间传递信息。
  • Hooks（Hook）： 用于在特定的底层操作（如存储变量的加载和存储）上附加 CVL 代码。
  • Init State 和 Axiom： 用于初始化 Ghost 变量，并确保初始状态始终为真。
  • 参数化规则： 包含未定义方法变量的规则，允许对多个方法进行验证。
• NFT Mock 合约： 视频首先使用一个简单的 NFT Mock 合约进行热身，验证总供应量（total supply）永远不会为负，以及铸造（mint）函数总是铸造一个 NFT。
• 乐观循环（Optimistic Loop）： 在某些情况下，需要启用乐观循环来避免循环展开问题。
• 代码仓库： 视频提供了与课程相关的 GitHub 代码仓库链接，学习者可以在其中找到项目代码和资源。