本文介绍了 Certora 是如何对 OpenZeppelin 的 Initializable.sol 合约进行形式化验证的。我们假设读者已经熟悉该合约的使用方法。如果不熟悉，请参阅我们关于 Initializable Contracts 的文章。

在可升级合约中，不使用构造函数（constructor）。取而代之的是，在部署之后，部署者会调用 initialize(...)，这将状态变量设置为它们的初始状态。initialize(...) 函数必须只能被调用一次。

为了允许在以后的时间将存储变量设置为另一个值（例如，如果 ERC-20 代币更改了其名称或 totalSupply），这些更改必须通过 reinitialize 函数来进行。外部函数不需要被命名为 “initializer” 和 “reinitializer”，但它们确实需要将 OpenZeppelin 库中的 initializer() 和 reinitializer() 修饰符应用到这些函数上。

出于安全考虑，关于初始化器（initializer），可升级合约必须具备以下属性：

1. 一旦调用了初始化器，它就绝不应该再被调用（所有的调用都应该 revert）。
2. 不应该能在实现合约（implementation contract）中调用初始化器。只有代理（proxy）中的初始化器应该是可调用的，因为所有的状态都保存在代理合约中。这就是为什么代理模式的逻辑合约会在构造函数中调用 _disableInitializers() 的原因。
3. 一旦初始化器和重新初始化器被禁用，它们应该永久保持禁用状态。
4. 如果我们调用重新初始化函数，我们必须在前一个版本的基础上递增版本号。该版本号存储为一个 uint64 变量。

请注意，对初始化器和重新初始化器的访问控制超出了本合约的范围。该合约甚至不强制规定这些函数的名称，它只确保修饰符的功能是正确的。

我们将涵盖 OpenZeppelin 的 Initializable.spec 文件的大部分内容，但不是全部，因为其中一些内容依赖于我们尚未涵盖的技术。然而，基于我们到目前为止在课程中所涵盖的内容，绝大部分内容应该是可以理解的。

这是我们检查的第一条规则：

Copy
rule cannotInitializeTwice() {
    require isInitialized();

    initialize@withrevert();

    assert lastReverted, "contract must only be initialized once";
}

这表示如果合约已被初始化，那么调用 initialize() 将会 revert。这条规则 并没有 说如果合约未初始化，调用 initialize() 就不会 revert；换句话说，未初始化的合约 可以 被初始化。require 语句设定了规则的作用域，使其仅涵盖初始化器已经被调用过的场景。

关于未初始化合约可以被初始化的规范由以下规则涵盖：

Copy
rule initializeEffects() {
    requireInvariant notInitializing();

    bool isUninitializedBefore = isUninitialized();

    initialize@withrevert();
    bool success = !lastReverted;

    assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts";
    assert success => version() == 1,         "initialize must set version() to 1";
    
}

该规则表示，当且仅当合约之前未被初始化过时，initialize 才会成功。如果初始化成功，那么版本必须被设置为 1。requireInvariant 语法我们尚未介绍，我们将在后面的教程中重新探讨它。

重新初始化器不能覆盖禁用状态的规则很大程度上是不言自明的：

Copy
rule cannotReinitializeOnceDisabled() {
    require isDisabled();

    uint64 n;
    reinitialize@withrevert(n);

    assert lastReverted, "contract is disabled";
}

换句话说，如果合约被禁用，那么任何对 reinitialize 的调用都会导致 revert。

当调用重新初始化器时，必须设置一个新版本，且该版本必须大于旧版本。以下规则表示，如果新版本是参数中传入的版本，并且如果交易没有 revert，那么该新版本一定大于前一个版本。

Copy
rule reinitializeEffects() {
    requireInvariant notInitializing();

    uint64 versionBefore = version();

    uint64 n;
    reinitialize@withrevert(n);
    bool success = !lastReverted;

    assert success <=> versionBefore < n, "can only reinitialize to a later versions";
    assert success => version() == n,     "reinitialize must set version() to n";
}

我们检查的最后一条规则声明，如果合约未处于“初始化状态”（合约当前正在设置存储变量或进行重新初始化），那么调用 disable 总是会成功。

Copy
rule disableEffect() {
    requireInvariant notInitializing();

    disable@withrevert();
    bool success = !lastReverted;

    assert success,      "call to _disableInitializers failed";
    assert isDisabled(), "disable state not set";
}

总结

我们在这里展示的规则非常容易理解，但我们回顾它们是为了证明形式化验证并不总是非得复杂不可。我们这里展示的规则也可以通过单元测试来实现，但形式化验证更彻底且安全保证度更高。

本文是 使用 Certora Prover 进行形式化验证 系列文章的一部分