refactor: fmt spec files

Author: QGarchery

certora/specs/AccrueInterest.spec

@@ -4,8 +4,8 @@ methods {
 
     function Util.maxFee() external returns uint256 envfree;
 
-    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.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);
     // We assume here that all external functions will not access storage, since we cannot show commutativity otherwise.
     // We also need to assume that the price and borrow rate return always the same value (and do not depend on msg.origin), so we use ghost functions for them.

certora/specs/ExchangeRate.spec

@@ -17,8 +17,8 @@ methods {
     function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
     function UtilsLib.min(uint256 x, uint256 y) internal returns uint256 => summaryMin(x, y);
-    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
-    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c);
+    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a, b, c);
+    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a, b, c);
     function MathLib.wTaylorCompounded(uint256, uint256) internal returns uint256 => NONDET;
 
     function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF;
@@ -101,7 +101,7 @@ filtered {
     // Here we assume interest has already been accumulated for this block.
     require lastUpdate(id) == e.block.timestamp;
 
-    f(e,args);
+    f(e, args);
 
     mathint assetsAfter = virtualTotalSupplyAssets(id);
     mathint sharesAfter = virtualTotalSupplyShares(id);
@@ -154,7 +154,7 @@ filtered {
     mathint assetsBefore = virtualTotalBorrowAssets(id);
     mathint sharesBefore = virtualTotalBorrowShares(id);
 
-    f(e,args);
+    f(e, args);
 
     mathint assetsAfter = virtualTotalBorrowAssets(id);
     mathint sharesAfter = virtualTotalBorrowShares(id);

certora/specs/Health.spec

@@ -19,7 +19,7 @@ methods {
     function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree;
 
     function _.price() external => CONSTANT;
-    function UtilsLib.min(uint256 a, uint256 b) internal returns uint256 => summaryMin(a,b);
+    function UtilsLib.min(uint256 a, uint256 b) internal returns uint256 => summaryMin(a, b);
 }
 
 function summaryMin(uint256 a, uint256 b) returns uint256 {

certora/specs/LiquidateBuffer.spec

@@ -18,7 +18,7 @@ methods {
     function Util.oraclePriceScale() external returns (uint256) envfree;
     function Util.wad() external returns (uint256) envfree;
 
-    function Morpho._isHealthy(MorphoHarness.MarketParams memory, MorphoHarness.Id,address) internal returns (bool) => NONDET;
+    function Morpho._isHealthy(MorphoHarness.MarketParams memory, MorphoHarness.Id, address) internal returns (bool) => NONDET;
     function Morpho._accrueInterest(MorphoHarness.MarketParams memory, MorphoHarness.Id) internal => NONDET;
 
     function _.price() external => constantPrice expect uint256;

certora/specs/Reentrancy.spec

@@ -48,14 +48,14 @@ rule reentrancySafe(method f, env e, calldataarg data) {
     // Set up the initial state.
     require !callIsBorrowRate;
     require !hasAccessedStorage && !hasCallAfterAccessingStorage && !hasReentrancyUnsafeCall;
-    f(e,data);
+    f(e, data);
     assert !hasReentrancyUnsafeCall;
 }
 
 // Check that the contract is truly immutable.
 rule noDelegateCalls(method f, env e, calldataarg data) {
     // Set up the initial state.
     require !delegateCall;
-    f(e,data);
+    f(e, data);
     assert !delegateCall;
 }