本文深入探讨了在Certora形式化验证中使用Sstore Hook来处理智能合约中的存储映射（storage mappings）的挑战和解决方案。

聚焦于使用 Certora Prover 对 ERC-721 代币的铸造和销毁操作进行形式化验证。文章详细剖析了 CVL 规则的构建，包括如何设定前置条件、记录状态、处理函数调用及通过存活、影响和无副作用断言来确保智能合约的正确性和安全性。

本文详细介绍了如何使用 Certora Prover 对 Solady WETH 智能合约进行形式化验证。文章通过具体的 CVL 规则和不变式，深入分析了 WETH 的存取款功能及其核心不变性，包括处理以太坊余额、WETH 总供应量变化、事务回滚条件以及利用 ghost 变量和 hook 处理底层调用，最终展示了如何用 requireInvariant 优化验证。

本文介绍了在有限域中执行FFT算法（数论变换）所需的n次单位根，并列举了几个常用的FFT友好的有限域，包括Goldilocks Field、Baby Bear Field、Teddy Bear Field、Koala Bear Field、BN-128 field、STARK Field和BLS12-381，以及它们各自的特征和单位根的阶数，并提供了相应的Python代码验证。

本文介绍了Cairo编程语言的基础知识，包括Cairo在Starknet中的作用、开发环境的搭建、语言的语法要点和数据类型（felt252、整数、bool）、复合类型(元组、结构体、枚举)、字符串处理、控制流以及数组和字典的使用。着重讲解了Cairo与Rust相似的语法结构，以及Cairo中数据类型和错误处理的特殊性。

本文是 Cairo 编程的入门教程，面向有 Solidity 经验的开发者，旨在帮助他们快速上手 Cairo 语言。教程介绍了 Cairo 的基本概念、安装配置、项目结构，以及Cairo与Solidity的异同，还包括Starknet账户创建和初始化，以及如何避免旧版本 Cairo 代码的问题。

本文深入探讨了Starknet中Cairo事件的工作原理和结构，首先介绍了Cairo中事件的基本结构，并通过示例展示了如何使用[event]属性定义事件枚举和结构体。

本文详细介绍了如何在Starknet上构建和测试一个ERC-20代币合约，内容涵盖了ERC-20接口的定义、合约的存储设置、事件声明、以及各个功能的具体实现，包括元数据函数、total_supply、mint、transfer、balance_of、allowance、approve和transfer_from等关键功能，并提供了相应的测试用例和潜在问题的解决方案。

本文介绍了如何使用 Cairo 语言为 Starknet 构建可部署的智能合约。文章从一个简单的合约草图开始，逐步添加功能，演示了 Cairo 合约的核心构建块，包括模块、接口（trait）、存储、合约状态以及不同的注解，最后介绍了合约的编译和测试方法。

本文详细介绍了 Cairo 中整数的工作原理，重点介绍了与 Solidity 的关键区别，包括整数类型、溢出保护、类型转换、常量、最大最小值、字面量表示、位运算、以及特殊的 felt252 类型及其除法运算。文章还提及了 Cairo 编译器如何处理整数与 felt252 之间的转换，并建议在非必要情况下避免直接使用 felt252 以优化 Gas 消耗。