Browse Source

get rid of certora/helpers

Hadrien Croubois 3 years ago
parent
commit
a73d7ab57b

+ 0 - 5
certora/helpers/DummyERC20A.sol

@@ -1,5 +0,0 @@
-// SPDX-License-Identifier: agpl-3.0
-pragma solidity ^0.8.0;
-import "./DummyERC20Impl.sol";
-
-contract DummyERC20A is DummyERC20Impl {}

+ 0 - 5
certora/helpers/DummyERC20B.sol

@@ -1,5 +0,0 @@
-// SPDX-License-Identifier: agpl-3.0
-pragma solidity ^0.8.0;
-import "./DummyERC20Impl.sol";
-
-contract DummyERC20B is DummyERC20Impl {}

+ 0 - 57
certora/helpers/DummyERC20Impl.sol

@@ -1,57 +0,0 @@
-// SPDX-License-Identifier: agpl-3.0
-pragma solidity ^0.8.0;
-
-// with mint
-contract DummyERC20Impl {
-    uint256 t;
-    mapping (address => uint256) b;
-    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 b[account];
-    }
-    function transfer(address recipient, uint256 amount) external returns (bool) {
-        b[msg.sender] = sub(b[msg.sender], amount);
-        b[recipient] = add(b[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) {
-        b[sender] = sub(b[sender], amount);
-        b[recipient] = add(b[recipient], amount);
-        a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
-        return true;
-    }
-}

+ 1 - 2
certora/scripts/passes/verifyERC20Wrapper.sh

@@ -2,9 +2,8 @@
 
 set -euxo pipefail
 
-    # --link ERC20WrapperHarness:underlying=DummyERC20A \
 certoraRun \
-    certora/harnesses/ERC20WrapperHarness.sol certora/helpers/DummyERC20A.sol certora/helpers/DummyERC20B.sol \
+    certora/harnesses/ERC20WrapperHarness.sol certora/harnesses/ERC20PermitHarness.sol \
     --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \
     --solc solc \
     --optimistic_loop \