From 6c99282d30fe8ffe9b81f061d57af70615119730 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 21 Nov 2023 15:16:25 +0100 Subject: [PATCH] chore: update to v5 DELETE syntax --- certora/specs/AccrueInterest.spec | 2 +- certora/specs/ConsistentState.spec | 2 +- certora/specs/ExactMath.spec | 2 +- certora/specs/ExitLiquidity.spec | 2 +- certora/specs/Health.spec | 2 +- certora/specs/LibSummary.spec | 2 +- certora/specs/Liveness.spec | 2 +- certora/specs/RatioMath.spec | 2 +- certora/specs/Reentrancy.spec | 2 +- certora/specs/Reverts.spec | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec index 3af214790..824cce07e 100644 --- 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 index 5324bd5b4..49e0c1df8 100644 --- 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 index 3ca2c3736..6e08543c8 100644 --- 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 index 30036108b..bf90ec31c 100644 --- 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 index 3602de29c..bac2aeba1 100644 --- 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 index 21cd67538..64322f7dc 100644 --- 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 index 5e7f46b1c..e5b96af82 100644 --- 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 index af690462e..2d138ad13 100644 --- 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 index 0a55276ea..5cb2b1639 100644 --- 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 index c54c06a21..7ecb5be1c 100644 --- 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;