Merge pull request #666 from morpho-org/certora/update-v6

[Certora] Update to v6 of the prover
morpho-org · Jan 31, 2024 · 129f8f9 · 129f8f9
2 parents 2ffb682 + b705d47
commit 129f8f9
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 17 deletions.
diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec
@@ -25,29 +25,29 @@ methods {
     function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);
 }
 
-ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares {
+persistent ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares {
     init_state axiom (forall MorphoHarness.Id id. sumSupplyShares[id] == 0);
 }
 
-ghost mapping(MorphoHarness.Id => mathint) sumBorrowShares {
+persistent ghost mapping(MorphoHarness.Id => mathint) sumBorrowShares {
     init_state axiom (forall MorphoHarness.Id id. sumBorrowShares[id] == 0);
 }
 
-ghost mapping(MorphoHarness.Id => mathint) sumCollateral {
+persistent ghost mapping(MorphoHarness.Id => mathint) sumCollateral {
     init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
 }
 
-ghost mapping(address => mathint) balance {
+persistent ghost mapping(address => mathint) balance {
     init_state axiom (forall address token. balance[token] == 0);
 }
 
-ghost mapping(address => mathint) idleAmount {
+persistent ghost mapping(address => mathint) idleAmount {
     init_state axiom (forall address token. idleAmount[token] == 0);
 }
 
-ghost mapping(MorphoHarness.Id => address) idToBorrowable;
+persistent ghost mapping(MorphoHarness.Id => address) idToBorrowable;
 
-ghost mapping(MorphoHarness.Id => address) idToCollateral;
+persistent ghost mapping(MorphoHarness.Id => address) idToCollateral;
 
 hook Sstore idToMarketParams[KEY MorphoHarness.Id id].loanToken address token STORAGE {
     idToBorrowable[id] = token;

diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec
@@ -17,8 +17,8 @@ methods {
     function UtilsLib.min(uint256 a, uint256 b) internal returns uint256 => summaryMin(a,b);
 }
 
-ghost uint256 lastPrice;
-ghost bool priceChanged;
+persistent ghost uint256 lastPrice;
+persistent ghost bool priceChanged;
 
 function mockPrice() returns uint256 {
     uint256 somePrice;

diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
@@ -23,7 +23,7 @@ methods {
     function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);
 }
 
-ghost mapping(address => mathint) balance {
+persistent ghost mapping(address => mathint) balance {
     init_state axiom (forall address token. balance[token] == 0);
 }
 

diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec
@@ -5,14 +5,14 @@ methods {
     function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256;
 }
 
-ghost bool delegateCall;
-ghost bool callIsBorrowRate;
+persistent ghost bool delegateCall;
+persistent ghost bool callIsBorrowRate;
 // True when storage has been accessed with either a SSTORE or a SLOAD.
-ghost bool hasAccessedStorage;
+persistent ghost bool hasAccessedStorage;
 // True when a CALL has been done after storage has been accessed.
-ghost bool hasCallAfterAccessingStorage;
+persistent ghost bool hasCallAfterAccessingStorage;
 // True when storage has been accessed, after which an external call is made, followed by accessing storage again.
-ghost bool hasReentrancyUnsafeCall;
+persistent ghost bool hasReentrancyUnsafeCall;
 
 function summaryBorrowRate() returns uint256 {
     uint256 result;

diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec
@@ -23,7 +23,7 @@ methods {
 definition isCreated(MorphoHarness.Id id) returns bool =
     (lastUpdate(id) != 0);
 
-ghost mapping(MorphoHarness.Id => mathint) sumCollateral
+persistent ghost mapping(MorphoHarness.Id => mathint) sumCollateral
 {
     init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
 }

diff --git a/certora/specs/Transfer.spec b/certora/specs/Transfer.spec
@@ -13,7 +13,7 @@ methods {
     function _.totalSupply() external => DISPATCHER(true);
 }
 
-ghost mapping(address => mathint) balance {
+persistent ghost mapping(address => mathint) balance {
     init_state axiom (forall address token. balance[token] == 0);
 }