Minor changes

makerdao · Oct 17, 2024 · 5632164 · 5632164
1 parent c7a043c
commit 5632164
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 10 deletions.
diff --git a/certora/L1FarmProxy.conf b/certora/L1FarmProxy.conf
@@ -1,6 +1,7 @@
 {
     "files": [
         "src/L1FarmProxy.sol",
+        "certora/harness/Auxiliar.sol",
         "test/mocks/L1TokenBridgeMock.sol",
         "test/mocks/GemMock.sol"
     ],

diff --git a/certora/L1FarmProxy.spec b/certora/L1FarmProxy.spec
@@ -1,6 +1,7 @@
 // L1FarmProxy.spec
 
 using GemMock as gem;
+using Auxiliar as aux;
 using L1TokenBridgeMock as l1Bridge;
 
 methods {
@@ -14,6 +15,7 @@ methods {
     function l2Proxy() external returns (address) envfree;
     function l1Bridge() external returns (address) envfree;
     //
+    function aux.getEmptyDataHash() external returns (bytes32) envfree;
     function gem.allowance(address,address) external returns (uint256) envfree;
     function gem.totalSupply() external returns (uint256) envfree;
     function gem.balanceOf(address) external returns (uint256) envfree;
@@ -24,7 +26,6 @@ methods {
     function l1Bridge.lastAmount() external returns (uint256) envfree;
     function l1Bridge.lastMinGasLimit() external returns (uint32) envfree;
     function l1Bridge.lastExtraDataHash() external returns (bytes32) envfree;
-    function l1Bridge.getEmptyDataHash() external returns (bytes32) envfree;
     //
     function _.transfer(address,uint256) external => DISPATCHER(true);
     function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
@@ -194,7 +195,7 @@ rule recover_revert(address token, address receiver, uint256 amount) {
 rule notifyRewardAmount(uint256 reward) {
     env e;
 
-    bytes32 emptyDataHash = l1Bridge.getEmptyDataHash();
+    bytes32 emptyDataHash = aux.getEmptyDataHash();
 
     notifyRewardAmount(e, reward);
 

diff --git a/certora/harness/Auxiliar.sol b/certora/harness/Auxiliar.sol
@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+// Copyright (C) 2024 Dai Foundation
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+pragma solidity ^0.8.21;
+
+contract Auxiliar {
+    function getEmptyDataHash() public view returns (bytes32) {
+        return this.getDataHash("");
+    }
+
+    function getDataHash(bytes calldata data) public pure returns (bytes32) {
+        return keccak256(data);
+    }
+}
diff --git a/test/mocks/L1TokenBridgeMock.sol b/test/mocks/L1TokenBridgeMock.sol
@@ -35,14 +35,6 @@ contract L1TokenBridgeMock {
         escrow = _escrow;
     }
 
-    function getEmptyDataHash() public view returns (bytes32) {
-        return this.getDataHash("");
-    }
-
-    function getDataHash(bytes calldata data) public pure returns (bytes32) {
-        return keccak256(data);
-    }
-
     function bridgeERC20To(
         address        _localToken,
         address        _remoteToken,