From a73d7ab57b3190d7be82b2baec5cdd562187e394 Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Wed, 5 Oct 2022 15:30:03 +0200
Subject: [PATCH] get rid of certora/helpers

---
 certora/helpers/DummyERC20A.sol              |  5 --
 certora/helpers/DummyERC20B.sol              |  5 --
 certora/helpers/DummyERC20Impl.sol           | 57 --------------------
 certora/scripts/passes/verifyERC20Wrapper.sh |  3 +-
 4 files changed, 1 insertion(+), 69 deletions(-)
 delete mode 100644 certora/helpers/DummyERC20A.sol
 delete mode 100644 certora/helpers/DummyERC20B.sol
 delete mode 100644 certora/helpers/DummyERC20Impl.sol

diff --git a/certora/helpers/DummyERC20A.sol b/certora/helpers/DummyERC20A.sol
deleted file mode 100644
index 188b92608..000000000
--- a/certora/helpers/DummyERC20A.sol
+++ /dev/null
@@ -1,5 +0,0 @@
-// SPDX-License-Identifier: agpl-3.0
-pragma solidity ^0.8.0;
-import "./DummyERC20Impl.sol";
-
-contract DummyERC20A is DummyERC20Impl {}
\ No newline at end of file
diff --git a/certora/helpers/DummyERC20B.sol b/certora/helpers/DummyERC20B.sol
deleted file mode 100644
index 0f97f1efc..000000000
--- a/certora/helpers/DummyERC20B.sol
+++ /dev/null
@@ -1,5 +0,0 @@
-// SPDX-License-Identifier: agpl-3.0
-pragma solidity ^0.8.0;
-import "./DummyERC20Impl.sol";
-
-contract DummyERC20B is DummyERC20Impl {}
\ No newline at end of file
diff --git a/certora/helpers/DummyERC20Impl.sol b/certora/helpers/DummyERC20Impl.sol
deleted file mode 100644
index 42e7f2302..000000000
--- a/certora/helpers/DummyERC20Impl.sol
+++ /dev/null
@@ -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;
-    }
-}
\ No newline at end of file
diff --git a/certora/scripts/passes/verifyERC20Wrapper.sh b/certora/scripts/passes/verifyERC20Wrapper.sh
index b5ff53587..0a05c60ad 100644
--- a/certora/scripts/passes/verifyERC20Wrapper.sh
+++ b/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 \