Merge pull request #50 from 0xPolygon/certora/CVL2

Add Certora spec files

.gitignore

@@ -10,3 +10,8 @@ lcov.info
 broadcast/*/31337
 deployments/31337.md
 deployments/json/31337.json
+
+# Certora and Gambit cache
+.certora_internal
+collect.json
+collection_failures.txt

certora/confs/defaultEmissionManager_verified.conf

@@ -0,0 +1,29 @@
+{
+  "files": [
+    "src/PolygonMigration.sol",
+    "src/PolygonEcosystemToken.sol",
+    "certora/harnesses/PowUtilHarness.sol:PowUtilHarness",
+    "certora/harnesses/DefaultEmissionManagerHarness.sol:DefaultEmissionManagerHarness",
+    "certora/harnesses/helpers/DummyERC20.sol:DummyERC20Impl"
+  ],
+  "link": [
+    "DefaultEmissionManagerHarness:token=PolygonEcosystemToken",
+    "DefaultEmissionManagerHarness:migration=PolygonMigration",
+    "PolygonMigration:matic=DummyERC20Impl",
+    "PolygonMigration:polygon=PolygonEcosystemToken"
+
+  ],
+  "verify":
+    "DefaultEmissionManagerHarness:certora/specs/DefaultEmissionManager.spec",
+  "packages": [
+    "openzeppelin-contracts=lib/openzeppelin-contracts"
+  ],
+  "prover_args": [
+    "-optimisticFallback true"
+  ],
+  "multi_assert_check": true,
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "send_only": true,
+  "rule_sanity": "basic"
+}

certora/confs/gambit/defaultEmissionManger.conf

@@ -0,0 +1,8 @@
+{
+  "filename": "../../../src/DefaultEmissionManager.sol",
+  "solc_remappings": [
+    "openzeppelin-contracts=../../../lib/openzeppelin-contracts/",
+    "openzeppelin-contracts-upgradeable=../../../lib/openzeppelin-contracts-upgradeable/"
+  ],
+  "num_mutants" : 100
+}

certora/confs/gambit/polygonEcosystemToken.conf

@@ -0,0 +1,7 @@
+{
+  "filename": "../../../src/PolygonEcosystemToken.sol",
+  "solc_remappings": [
+    "openzeppelin-contracts=../../../lib/openzeppelin-contracts/"
+  ],
+  "num_mutants" : 100
+}

certora/confs/gambit/polygonMigration.conf

@@ -0,0 +1,8 @@
+{
+  "filename": "../../../src/PolygonMigration.sol",
+  "solc_remappings": [
+    "openzeppelin-contracts=../../../lib/openzeppelin-contracts/",
+    "openzeppelin-contracts-upgradeable=../../../lib/openzeppelin-contracts-upgradeable/"
+  ],
+  "num_mutants" : 100
+}

certora/confs/polygonEcosystemToken_verified.conf

@@ -0,0 +1,19 @@
+{
+  "files": [
+    "certora/harnesses/PolygonEcosystemTokenHarness.sol",
+    "certora/harnesses/DefaultEmissionManagerHarness.sol:DefaultEmissionManagerHarness"
+  ],
+  "verify":
+    "PolygonEcosystemTokenHarness:certora/specs/PolygonEcosystemToken.spec",
+  "packages": [
+    "openzeppelin-contracts=lib/openzeppelin-contracts"
+  ],
+  "prover_args": [
+    "-optimisticFallback true" 
+  ],
+  "multi_assert_check": true,
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "send_only": true,
+  "rule_sanity": "basic"
+}

certora/confs/polygonMigration_verified.conf

@@ -0,0 +1,25 @@
+{
+  "files": [
+    "certora/harnesses/PolygonMigrationHarness.sol:PolygonMigrationHarness",
+    "certora/harnesses/DefaultEmissionManagerHarness.sol:DefaultEmissionManagerHarness",
+    "certora/harnesses/helpers/DummyERC20.sol:DummyERC20Impl",
+    "src/PolygonEcosystemToken.sol:PolygonEcosystemToken"
+  ],
+  "link": [
+    "PolygonMigrationHarness:polygon=PolygonEcosystemToken",
+    "PolygonMigrationHarness:matic=DummyERC20Impl"
+    ],
+  "verify":
+    "PolygonMigrationHarness:certora/specs/PolygonMigration.spec",
+  "packages": [
+    "openzeppelin-contracts=lib/openzeppelin-contracts"
+  ],
+  "prover_args": [
+    "-optimisticFallback true"
+  ],
+  "multi_assert_check": true,
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "send_only": true,
+  "rule_sanity": "basic"
+}

certora/confs/powUtil_verified.conf

@@ -0,0 +1,15 @@
+{
+  "files": [
+    "certora/harnesses/PowUtilHarness.sol"
+  ],
+  "verify":
+    "PowUtilHarness:certora/specs/PowUtil.spec",
+  "prover_args": [
+    "-optimisticFallback true"
+  ],
+  "multi_assert_check": true,
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "send_only": true,
+  "rule_sanity": "basic"
+}

certora/confs/runAll.sh

@@ -0,0 +1,15 @@
+#!/bin/bash
+
+# Get a list of all .conf files
+CONF_FILES=$(ls certora/confs/*.conf)
+
+# Iterate over each .conf file
+for CONF_FILE in $CONF_FILES; do
+    echo "Executing $CONF_FILE..."
+
+    # Execute certoraRun with the current .conf file
+    certoraRun "$CONF_FILE" --msg "$CONF_FILE"
+
+    echo "Done executing $CONF_FILE."
+    echo
+done

certora/harnesses/DefaultEmissionManagerHarness.sol

@@ -0,0 +1,51 @@
+pragma solidity 0.8.21;
+
+import "../../src/DefaultEmissionManager.sol";
+
+
+contract DefaultEmissionManagerHarness is DefaultEmissionManager {
+    using SafeERC20 for IPolygonEcosystemToken;
+
+    constructor(
+        address token_,
+        address migration_,
+        address stakeManager_,
+        address treasury_,
+        address owner_
+    )  DefaultEmissionManager(migration_, stakeManager_, treasury_)
+    {
+        if (
+            token_ == address(0) ||
+            migration_ == address(0) ||
+            stakeManager_ == address(0) ||
+            treasury_ == address(0) ||
+            owner_ == address(0)
+        ) revert InvalidAddress();
+
+
+        token = IPolygonEcosystemToken(token_);
+        migration = IPolygonMigration(migration_);
+        stakeManager = stakeManager_;
+        treasury = treasury_;
+        startTimestamp = block.timestamp;
+
+        assert(START_SUPPLY == token.totalSupply());
+
+        token.safeApprove(migration_, type(uint256).max);
+        // initial ownership setup bypassing 2 step ownership transfer process
+        _transferOwnership(owner_);
+
+    }
+
+    function amountToBeMinted() external view returns (uint256) {
+        uint256 timeElapsed = block.timestamp - startTimestamp;
+        uint256 supplyFactor = PowUtil.exp2((INTEREST_PER_YEAR_LOG2 * timeElapsed) / 365 days);
+        uint256 newSupply = (supplyFactor * START_SUPPLY) / 1e18;
+
+        return newSupply - token.totalSupply();
+    }
+
+    function externalExp2(uint256 value) external pure returns (uint256) {
+        return PowUtil.exp2(value);
+    }
+}

certora/harnesses/PolygonEcosystemTokenHarness.sol

@@ -0,0 +1,18 @@
+pragma solidity 0.8.21;
+
+import "../../src/interfaces/IDefaultEmissionManager.sol";
+import "../../src/PolygonEcosystemToken.sol";
+
+
+contract PolygonEcosystemTokenHarness is PolygonEcosystemToken {
+
+    address private _emissionManager;
+    constructor(address migration, address emissionManager, address governance, address permit2Revoker) 
+        PolygonEcosystemToken(migration, emissionManager, governance, permit2Revoker) {
+            _emissionManager = emissionManager;
+    }
+
+    function fetchMaxMint() external view returns (uint256) {
+        return (block.timestamp - lastMint) * mintPerSecondCap;
+    }
+}

certora/harnesses/PolygonMigrationHarness.sol

@@ -0,0 +1,12 @@
+pragma solidity 0.8.21;
+
+import "../../src/PolygonMigration.sol";
+
+
+contract PolygonMigrationHarness is PolygonMigration {
+    constructor(address matic_) PolygonMigration(matic_) {}
+
+    function dead() external pure returns (address) {
+        return 0x000000000000000000000000000000000000dEaD;
+    }
+}

certora/harnesses/PowUtilHarness.sol

@@ -0,0 +1,10 @@
+pragma solidity 0.8.21;
+
+import "../../src/lib/PowUtil.sol";
+
+contract PowUtilHarness {
+    function exp2(uint256 value) external pure returns (uint256) {
+        return PowUtil.exp2(value);
+    }
+}
+

certora/harnesses/helpers/DummyERC20.sol

@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity 0.8.21;
+
+// with mint
+contract DummyERC20Impl {
+    uint256 t;
+    mapping (address => uint256) _balances;
+    mapping (address => mapping (address => uint256)) a;
+
+    string public name;
+    string public symbol;
+    uint public decimals;
+
+    function myAddress() public returns (address) {
+        return address(this);
+    }
+
+    function add(uint a, uint b) internal pure returns (uint256) {
+        uint c = a +b;
+        require (c >= a);
+        return c;
+    }
+    function sub(uint a, uint b) internal pure returns (uint256) {
+        require (a>=b);
+        return a-b;
+    }
+
+    function totalSupply() external view returns (uint256) {
+        return t;
+    }
+    function balanceOf(address account) external view returns (uint256) {
+        return _balances[account];
+    }
+    function transfer(address recipient, uint256 amount) external returns (bool) {
+        _balances[msg.sender] = sub(_balances[msg.sender], amount);
+        _balances[recipient] = add(_balances[recipient], amount);
+        return true;
+    }
+    function allowance(address owner, address spender) external view returns (uint256) {
+        return a[owner][spender];
+    }
+    function approve(address spender, uint256 amount) external returns (bool) {
+        a[msg.sender][spender] = amount;
+        return true;
+    }
+
+    function transferFrom(
+        address sender,
+        address recipient,
+        uint256 amount
+    ) external returns (bool) {
+        _balances[sender] = sub(_balances[sender], amount);
+        _balances[recipient] = add(_balances[recipient], amount);
+        a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
+        return true;
+    }
+}