Merge pull request #600 from morpho-org/certora/update-v5

[Certora] Update to v5 of the prover

Author: QGarchery

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);

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;

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;

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;

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;

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;

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;

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;

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;
 }
 

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;