Skip to content

Commit

Permalink
Merge branch 'certora/dev' into certora/gambit
Browse files Browse the repository at this point in the history
  • Loading branch information
QGarchery committed Nov 21, 2023
2 parents 0f8554e + f5dd194 commit 4d394ad
Show file tree
Hide file tree
Showing 31 changed files with 418 additions and 312 deletions.
7 changes: 4 additions & 3 deletions .github/workflows/foundry.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,12 +21,12 @@ jobs:
- type: "slow"
fuzz-runs: 10000
max-test-rejects: 500000
invariant-runs: 48
invariant-depth: 2048
invariant-runs: 0
invariant-depth: 512
- type: "fast"
fuzz-runs: 256
max-test-rejects: 65536
invariant-runs: 16
invariant-runs: 0
invariant-depth: 256

runs-on: ubuntu-latest
Expand All @@ -45,3 +45,4 @@ jobs:
FOUNDRY_FUZZ_MAX_TEST_REJECTS: ${{ matrix.max-test-rejects }}
FOUNDRY_INVARIANT_RUNS: ${{ matrix.invariant-runs }}
FOUNDRY_INVARIANT_DEPTH: ${{ matrix.invariant-depth }}
FOUNDRY_FUZZ_SEED: 0x${{ github.event.pull_request.base.sha || github.sha }}
20 changes: 20 additions & 0 deletions .github/workflows/npm-release.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
name: Publish on NPM

on:
workflow_dispatch:

jobs:
publish-to-npm:
name: Publish to NPM
runs-on: ubuntu-latest
environment:
name: npm
url: https://www.npmjs.com/package/@morpho-org/morpho-blue
steps:
- name: Checkout
uses: actions/checkout@v3

- name: Publish to npm
run: |
echo "//registry.npmjs.org/:_authToken=${{ secrets.NPM_TOKEN }}" > ~/.npmrc
yarn publish --access public
Binary file not shown.
Binary file not shown.
Binary file not shown.
4 changes: 3 additions & 1 deletion certora/configuration/RatioMath.conf
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,9 @@
],
"verify": "MorphoHarness:certora/specs/RatioMath.spec",
"prover_args": [
"-smt_hashingScheme plaininjectivity"
"-smt_hashingScheme plaininjectivity",
"-mediumTimeout 30",
"-timeout 3600"
],
"msg": "Morpho Blue Ratio Math"
}
11 changes: 2 additions & 9 deletions certora/harness/MorphoHarness.sol
Original file line number Diff line number Diff line change
Expand Up @@ -78,21 +78,14 @@ contract MorphoHarness is Morpho {
marketParamsId = Id.wrap(keccak256(abi.encode(marketParams)));
}

function libMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
function libMulDivUp(uint256 x, uint256 y, uint256 d) external pure returns (uint256) {
return MathLib.mulDivUp(x, y, d);
}

function libMulDivDown(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
function libMulDivDown(uint256 x, uint256 y, uint256 d) external pure returns (uint256) {
return MathLib.mulDivDown(x, y, d);
}

function accrueInterest(MarketParams memory marketParams) external {
Id id = marketParams.id();
require(market[id].lastUpdate != 0, ErrorsLib.MARKET_NOT_CREATED);

_accrueInterest(marketParams, id);
}

function isHealthy(MarketParams memory marketParams, address user) external view returns (bool) {
return _isHealthy(marketParams, marketParams.id(), user);
}
Expand Down
10 changes: 5 additions & 5 deletions certora/harness/TransferHarness.sol
Original file line number Diff line number Diff line change
Expand Up @@ -13,23 +13,23 @@ interface IERC20Extended is IERC20 {
contract TransferHarness {
using SafeTransferLib for IERC20;

function libSafeTransferFrom(address token, address from, address to, uint256 value) public {
function libSafeTransferFrom(address token, address from, address to, uint256 value) external {
IERC20(token).safeTransferFrom(from, to, value);
}

function libSafeTransfer(address token, address to, uint256 value) public {
function libSafeTransfer(address token, address to, uint256 value) external {
IERC20(token).safeTransfer(to, value);
}

function balanceOf(address token, address user) public view returns (uint256) {
function balanceOf(address token, address user) external view returns (uint256) {
return IERC20Extended(token).balanceOf(user);
}

function allowance(address token, address owner, address spender) public view returns (uint256) {
function allowance(address token, address owner, address spender) external view returns (uint256) {
return IERC20Extended(token).allowance(owner, spender);
}

function totalSupply(address token) public view returns (uint256) {
function totalSupply(address token) external view returns (uint256) {
return IERC20Extended(token).totalSupply();
}
}
4 changes: 2 additions & 2 deletions certora/specs/Transfer.spec
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ rule transferRevertCondition(address token, address to, uint256 amount) {

libSafeTransfer@withrevert(token, to, amount);

assert lastReverted == (initialBalance < amount);
assert lastReverted <=> initialBalance < amount;
}

// Check the revert condition of the summary of safeTransferFrom.
Expand All @@ -83,5 +83,5 @@ rule transferFromRevertCondition(address token, address from, address to, uint25

libSafeTransferFrom@withrevert(token, from, to, amount);

assert lastReverted == (initialBalance < amount) || allowance < amount;
assert lastReverted <=> initialBalance < amount || allowance < amount;
}
2 changes: 1 addition & 1 deletion foundry.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ via-ir = true
optimizer_runs = 4294967295

[profile.default.invariant]
runs = 16
runs = 8
depth = 256
fail_on_revert = true

Expand Down
11 changes: 8 additions & 3 deletions package.json
Original file line number Diff line number Diff line change
@@ -1,10 +1,15 @@
{
"name": "morpho-blue",
"name": "@morpho-org/morpho-blue",
"description": "Morpho Blue Protocol",
"license": "BUSL-1.1",
"version": "1.0.0",
"version": "0.1.0",
"files": [
"src",
"README.md",
"LICENSE"
],
"scripts": {
"postinstall": "husky install && forge install",
"prepare": "husky install && forge install",
"build:forge": "FOUNDRY_PROFILE=build forge build",
"build:hardhat": "npx hardhat compile",
"test:forge": "FOUNDRY_PROFILE=test forge test",
Expand Down
1 change: 0 additions & 1 deletion remappings.txt

This file was deleted.

Loading

0 comments on commit 4d394ad

Please sign in to comment.