From 0490f4416d6046fc31cc17d5a96126124f8b735b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 10 Dec 2024 15:26:29 +0100 Subject: [PATCH] chore: returns syntax --- certora/specs/ConsistentInstantiation.spec | 2 +- certora/specs/MarketExists.spec | 2 +- certora/specs/SafeMath.spec | 4 ++-- certora/specs/SummaryLib.spec | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/specs/ConsistentInstantiation.spec b/certora/specs/ConsistentInstantiation.spec index b567236..f310efa 100644 --- a/certora/specs/ConsistentInstantiation.spec +++ b/certora/specs/ConsistentInstantiation.spec @@ -5,7 +5,7 @@ import "SummaryLib.spec"; methods { function _.market(PreLiquidation.Id) external => DISPATCHER(true); - function Util.libId(PreLiquidation.MarketParams) external returns PreLiquidation.Id envfree; + function Util.libId(PreLiquidation.MarketParams) external returns (PreLiquidation.Id) envfree; } // Ensure constructor requirements. diff --git a/certora/specs/MarketExists.spec b/certora/specs/MarketExists.spec index 50da83d..e11b281 100644 --- a/certora/specs/MarketExists.spec +++ b/certora/specs/MarketExists.spec @@ -4,7 +4,7 @@ using Morpho as MORPHO; methods { function _.market(PreLiquidation.Id) external => DISPATCHER(true); - function MORPHO.market(PreLiquidation.Id) external returns (uint128, uint128, uint128,uint128, uint128, uint128) envfree; + function MORPHO.market(PreLiquidation.Id) external returns (uint128, uint128, uint128, uint128, uint128, uint128) envfree; function _.price() external => NONDET; } diff --git a/certora/specs/SafeMath.spec b/certora/specs/SafeMath.spec index daa4e59..9ce9f8e 100644 --- a/certora/specs/SafeMath.spec +++ b/certora/specs/SafeMath.spec @@ -2,11 +2,11 @@ definition WAD() returns mathint = 10^18; -function summaryWMulDown(mathint x,mathint y) returns mathint { +function summaryWMulDown(mathint x, mathint y) returns mathint { return (x * y) / WAD(); } -function summaryWDivUp(mathint x,mathint y) returns mathint { +function summaryWDivUp(mathint x, mathint y) returns mathint { return (x * WAD() + (y-1)) / y; } diff --git a/certora/specs/SummaryLib.spec b/certora/specs/SummaryLib.spec index 9f14db3..d8de352 100644 --- a/certora/specs/SummaryLib.spec +++ b/certora/specs/SummaryLib.spec @@ -4,8 +4,8 @@ using MorphoHarness as MORPHO; using Util as Util; methods { - function MORPHO.virtualTotalBorrowAssets(PreLiquidation.Id) external returns(uint256) envfree; - function MORPHO.virtualTotalBorrowShares(PreLiquidation.Id) external returns(uint256) envfree; + function MORPHO.virtualTotalBorrowAssets(PreLiquidation.Id) external returns (uint256) envfree; + function MORPHO.virtualTotalBorrowShares(PreLiquidation.Id) external returns (uint256) envfree; function MORPHO.borrowShares(PreLiquidation.Id, address) external returns (uint256) envfree; function MORPHO.collateral(PreLiquidation.Id, address) external returns (uint256) envfree; function MORPHO.lastUpdate(PreLiquidation.Id) external returns (uint256) envfree;