77 lines
2.3 KiB
Ruby
77 lines
2.3 KiB
Ruby
using CommunityOwnerTokenRegistry as CommunityOwnerTokenRegistry;
|
|
|
|
methods {
|
|
function owner() external returns (address) envfree;
|
|
function deploymentRegistry() external returns (address) envfree;
|
|
function ownerTokenFactory() external returns (address) envfree;
|
|
function masterTokenFactory() external returns (address) envfree;
|
|
function deploy(CommunityTokenDeployer.TokenConfig, CommunityTokenDeployer.TokenConfig, CommunityTokenDeployer.DeploymentSignature, bytes) external returns (address, address);
|
|
|
|
function CommunityOwnerTokenRegistry.getEntry(address) external returns (address) envfree;
|
|
function CommunityOwnerTokenRegistry.tokenDeployer() external returns (address) envfree;
|
|
|
|
|
|
function _.balanceOf(address _owner) external => DISPATCHER(true);
|
|
}
|
|
|
|
rule integrityOfDeploy {
|
|
|
|
env e;
|
|
CommunityTokenDeployer.TokenConfig ownerToken;
|
|
CommunityTokenDeployer.TokenConfig masterToken;
|
|
CommunityTokenDeployer.DeploymentSignature signature;
|
|
bytes signerPublicKey;
|
|
|
|
deploy(e, ownerToken, masterToken, signature, signerPublicKey);
|
|
|
|
address tokenAddress = CommunityOwnerTokenRegistry.getEntry(signature.signer);
|
|
assert tokenAddress != 0;
|
|
}
|
|
|
|
rule registryMutability(method f) {
|
|
env e;
|
|
CommunityTokenDeployer.DeploymentSignature signature;
|
|
calldataarg args;
|
|
|
|
address tokenAddressBefore = CommunityOwnerTokenRegistry.getEntry(signature.signer);
|
|
require tokenAddressBefore != 0;
|
|
|
|
f(e, args);
|
|
|
|
address tokenAddressAfter = CommunityOwnerTokenRegistry.getEntry(signature.signer);
|
|
assert tokenAddressBefore == tokenAddressAfter;
|
|
}
|
|
|
|
rule registryChange(method f) {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
address registryBefore = deploymentRegistry();
|
|
f(e, args);
|
|
address registryAfter = deploymentRegistry();
|
|
|
|
assert registryBefore != registryAfter => e.msg.sender == owner();
|
|
}
|
|
|
|
rule ownerTokenFactoryChange(method f) {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
address factoryBefore = ownerTokenFactory();
|
|
f(e, args);
|
|
address factoryAfter = ownerTokenFactory();
|
|
|
|
assert factoryBefore != factoryAfter => e.msg.sender == owner();
|
|
}
|
|
|
|
rule masterTokenFactoryChange(method f) {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
address factoryBefore = masterTokenFactory();
|
|
f(e, args);
|
|
address factoryAfter = masterTokenFactory();
|
|
|
|
assert factoryBefore != factoryAfter => e.msg.sender == owner();
|
|
}
|