Skip to content

Commit

Permalink
chore: returns syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
QGarchery committed Dec 10, 2024
1 parent 15536c9 commit 0490f44
Show file tree
Hide file tree
Showing 4 changed files with 6 additions and 6 deletions.
2 changes: 1 addition & 1 deletion certora/specs/ConsistentInstantiation.spec
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion certora/specs/MarketExists.spec
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
4 changes: 2 additions & 2 deletions certora/specs/SafeMath.spec
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
4 changes: 2 additions & 2 deletions certora/specs/SummaryLib.spec
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down

0 comments on commit 0490f44

Please sign in to comment.