You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
165 lines
11 KiB
165 lines
11 KiB
import "helpers/helpers.spec"
|
|
|
|
methods {
|
|
// initialize, reinitialize, disable
|
|
initialize() envfree
|
|
reinitialize(uint8) envfree
|
|
disable() envfree
|
|
|
|
nested_init_init() envfree
|
|
nested_init_reinit(uint8) envfree
|
|
nested_reinit_init(uint8) envfree
|
|
nested_reinit_reinit(uint8,uint8) envfree
|
|
|
|
// view
|
|
version() returns uint8 envfree
|
|
initializing() returns bool envfree
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Definitions │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
definition isUninitialized() returns bool = version() == 0;
|
|
definition isInitialized() returns bool = version() > 0;
|
|
definition isDisabled() returns bool = version() == 255;
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Invariant: A contract must only ever be in an initializing state while in the middle of a transaction execution. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
invariant notInitializing()
|
|
!initializing()
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: The version cannot decrease & disable state is irrevocable. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule increasingVersion(env e) {
|
|
uint8 versionBefore = version();
|
|
bool disabledBefore = isDisabled();
|
|
|
|
method f; calldataarg args;
|
|
f(e, args);
|
|
|
|
assert versionBefore <= version(), "_initialized must only increase";
|
|
assert disabledBefore => isDisabled(), "a disabled initializer must stay disabled";
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Cannot initialize a contract that is already initialized. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule cannotInitializeTwice() {
|
|
require isInitialized();
|
|
|
|
initialize@withrevert();
|
|
|
|
assert lastReverted, "contract must only be initialized once";
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Cannot initialize once disabled. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule cannotInitializeOnceDisabled() {
|
|
require isDisabled();
|
|
|
|
initialize@withrevert();
|
|
|
|
assert lastReverted, "contract is disabled";
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Cannot reinitialize once disabled. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule cannotReinitializeOnceDisabled() {
|
|
require isDisabled();
|
|
|
|
uint8 n;
|
|
reinitialize@withrevert(n);
|
|
|
|
assert lastReverted, "contract is disabled";
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Cannot nest initializers (after construction). │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule cannotNestInitializers_init_init() {
|
|
nested_init_init@withrevert();
|
|
assert lastReverted, "nested initializers";
|
|
}
|
|
|
|
rule cannotNestInitializers_init_reinit(uint8 m) {
|
|
nested_init_reinit@withrevert(m);
|
|
assert lastReverted, "nested initializers";
|
|
}
|
|
|
|
rule cannotNestInitializers_reinit_init(uint8 n) {
|
|
nested_reinit_init@withrevert(n);
|
|
assert lastReverted, "nested initializers";
|
|
}
|
|
|
|
rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) {
|
|
nested_reinit_reinit@withrevert(n, m);
|
|
assert lastReverted, "nested initializers";
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Initialize correctly sets the version. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
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";
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Reinitialize correctly sets the version. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule reinitializeEffects() {
|
|
requireInvariant notInitializing();
|
|
|
|
uint8 versionBefore = version();
|
|
|
|
uint8 n;
|
|
reinitialize@withrevert(n);
|
|
bool success = !lastReverted;
|
|
|
|
assert success <=> versionBefore < n, "can only reinitialize to a latter versions";
|
|
assert success => version() == n, "reinitialize must set version() to n";
|
|
}
|
|
|
|
/*
|
|
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
|
|
│ Rule: Can disable. │
|
|
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
|
|
*/
|
|
rule disableEffect() {
|
|
requireInvariant notInitializing();
|
|
|
|
disable@withrevert();
|
|
bool success = !lastReverted;
|
|
|
|
assert success, "call to _disableInitializers failed";
|
|
assert isDisabled(), "disable state not set";
|
|
}
|
|
|