Merge branch 'certora/update-v5' into certora/gambit

morpho-org · Nov 21, 2023 · 2e333b0 · 2e333b0
2 parents 3284cce + 6c99282
commit 2e333b0
Show file tree

Hide file tree

Showing 10 changed files with 10 additions and 10 deletions.
diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c);
     function MathLib.wTaylorCompounded(uint256 a, uint256 b) internal returns uint256 => ghostTaylorCompounded(a, b);

diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;

diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;

diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/ExitLiquidity.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;

diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
     function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
     function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;

diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
     function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function totalSupplyAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
     function totalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree;
     function totalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree;

diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;

diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256;
 }
 

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 methods {
-    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE(true);
+    function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
     function owner() external returns address envfree;
     function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;