汇编与 EVM 课程 - Gas 2

视频 AI 总结： 该视频主要讲解了如何使用 Certora 工具对智能合约进行形式化验证，特别是针对 Gas 优化后的合约进行等价性验证。视频通过一个 NFT 市场的例子，展示了如何定义 ghost 变量、使用 hooks 监控合约状态变化、编写 invariants 来验证合约行为，以及如何利用 method summaries 和 prover arguments 来解决验证过程中遇到的问题，最终实现对 Gas 优化合约的功能等价性证明。

视频中提出的关键信息包括：

1. Ghost 变量： 用于在形式化验证中追踪合约状态，但不会影响合约的实际执行。
2. Hooks： 用于在特定 EVM 操作码执行时触发自定义逻辑，例如更新 ghost 变量。
3. Invariants： 用于声明合约状态必须满足的条件，Certora 会尝试找到违反这些条件的执行路径。
4. Method Summaries： 用于简化或替换合约中的函数行为，例如使用 dispatcher 关键字来限制外部调用的影响。
5. Prover Arguments： 用于配置 Certora 的行为，例如使用 optimistic fallback 来假设外部调用不会对合约状态产生任意修改。
6. Parametric Rules： 允许验证具有未定义方法变量的规则，用于比较不同合约在相同输入下的行为。
7. Vacuity Checks： 用于检测规则是否过于严格，以至于没有输入可以满足所有前提条件。
8. 等价性验证： 通过比较 Gas 优化前后合约的 getter 函数返回值，证明它们在功能上是等价的。