Skip to content

Commit 3684128

Browse files
CheyenneAtapourmiguelmtzinfMichaelMorami
authored
feat: Modular Gho Stewards (#414)
--------- Co-authored-by: miguelmtzinf <miguelmtz.mail@gmail.com> Co-authored-by: Michael Morami <91594326+MichaelMorami@users.noreply.github.com>
1 parent 3a3293b commit 3684128

File tree

60 files changed

+5993
-2543
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

60 files changed

+5993
-2543
lines changed

.github/workflows/certora-steward.yml

+8-1
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,10 @@ jobs:
3232

3333
- name: Install solc
3434
run: |
35+
cd certora/steward/
36+
touch applyHarness.patch
37+
make munged
38+
cd ../..
3539
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
3640
chmod +x solc-static-linux
3741
sudo mv solc-static-linux /usr/local/bin/solc8.10
@@ -48,4 +52,7 @@ jobs:
4852
max-parallel: 16
4953
matrix:
5054
rule:
51-
- rules.conf
55+
- GhoAaveSteward.conf
56+
- GhoBucketSteward.conf
57+
- GhoCcipSteward.conf
58+
- GhoGsmSteward.conf

.github/workflows/node.js.yml

+2
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ jobs:
77
env:
88
ALCHEMY_KEY: '${{secrets.ALCHEMY_KEY}}'
99
ETH_RPC_URL: 'https://eth-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}'
10+
RPC_MAINNET: 'https://eth-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}'
11+
RPC_ARBITRUM: 'https://arb-mainnet.g.alchemy.com/v2/${{secrets.ALCHEMY_KEY}}'
1012
strategy:
1113
matrix:
1214
node-version:
Binary file not shown.

certora/steward/Makefile

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
default: help
2+
3+
PATCH = applyHarness.patch
4+
CONTRACTS_DIR = ../../src
5+
MUNGED_DIR = munged
6+
7+
help:
8+
@echo "usage:"
9+
@echo " make clean: remove all generated files (those ignored by git)"
10+
@echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
11+
@echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
12+
13+
munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
14+
rm -rf $@
15+
mkdir $@
16+
cp -r ../../src $@
17+
patch -p0 -d $@ < $(PATCH)
18+
19+
record:
20+
mkdir tmp
21+
cp -r ../../src tmp
22+
diff -ruN tmp $(MUNGED_DIR) | sed 's+tmp/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH)
23+
rm -rf tmp
24+
25+
clean:
26+
git clean -fdX
27+
touch $(PATCH)
28+

certora/steward/applyHarness.patch

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
diff -ruN .gitignore .gitignore
2+
--- .gitignore 1970-01-01 02:00:00.000000000 +0200
3+
+++ .gitignore 2024-08-12 17:28:45.843705526 +0300
4+
@@ -0,0 +1,2 @@
5+
+*
6+
+!.gitignore
7+
\ No newline at end of file
+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
{
2+
"files": ["certora/steward/harness/GhoAaveSteward_Harness.sol"],
3+
"packages": [
4+
"@aave/core-v3/=lib/aave-v3-core",
5+
"@aave/periphery-v3/=lib/aave-v3-periphery",
6+
"@aave/=lib/aave-token",
7+
"@openzeppelin/=lib/openzeppelin-contracts",
8+
"aave-stk-v1-5/=lib/aave-stk-v1-5",
9+
"ds-test/=lib/forge-std/lib/ds-test/src",
10+
"forge-std/=lib/forge-std/src",
11+
"aave-address-book/=lib/aave-address-book/src",
12+
"aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers",
13+
"aave-v3-core/=lib/aave-address-book/lib/aave-v3-core",
14+
"erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests",
15+
"openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
16+
"solidity-utils/=lib/solidity-utils/src"
17+
],
18+
"build_cache": true,
19+
"optimistic_loop": true,
20+
"process": "emv",
21+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
22+
"smt_timeout": "2000",
23+
"solc": "solc8.10",
24+
"verify": "GhoAaveSteward_Harness:certora/steward/specs/GhoAaveSteward.spec",
25+
"rule_sanity": "basic",
26+
"msg": "GhoAaveSteward: all rules"
27+
}

certora/steward/conf/rules.conf certora/steward/conf/GhoBucketSteward.conf

+4-7
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,6 @@
11
{
22
"files": [
3-
"certora/steward/harness/GhoStewardV2_Harness.sol",
4-
"src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol"
5-
],
6-
"link": [
7-
"GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory",
3+
"src/contracts/misc/GhoBucketSteward.sol"
84
],
95
"packages": [
106
"@aave/core-v3/=lib/aave-v3-core",
@@ -21,12 +17,13 @@
2117
"openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
2218
"solidity-utils/=lib/solidity-utils/src"
2319
],
20+
"build_cache": true,
2421
"optimistic_loop": true,
2522
"process": "emv",
2623
"prover_args": ["-depth 15","-mediumTimeout 1000"],
2724
"smt_timeout": "2000",
2825
"solc": "solc8.10",
29-
"verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec",
26+
"verify": "GhoBucketSteward:certora/steward/specs/GhoBucketSteward.spec",
3027
"rule_sanity": "basic",
31-
"msg": "STEWARD: all rules"
28+
"msg": "GhoBucketSteward: all rules"
3229
}
+27
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
{
2+
"files": ["certora/steward/harness/GhoCcipSteward_Harness.sol"],
3+
"packages": [
4+
"@aave/core-v3/=lib/aave-v3-core",
5+
"@aave/periphery-v3/=lib/aave-v3-periphery",
6+
"@aave/=lib/aave-token",
7+
"@openzeppelin/=lib/openzeppelin-contracts",
8+
"aave-stk-v1-5/=lib/aave-stk-v1-5",
9+
"ds-test/=lib/forge-std/lib/ds-test/src",
10+
"forge-std/=lib/forge-std/src",
11+
"aave-address-book/=lib/aave-address-book/src",
12+
"aave-helpers/=lib/aave-stk-v1-5/lib/aave-helpers",
13+
"aave-v3-core/=lib/aave-address-book/lib/aave-v3-core",
14+
"erc4626-tests/=lib/aave-stk-v1-5/lib/openzeppelin-contracts/lib/erc4626-tests",
15+
"openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
16+
"solidity-utils/=lib/solidity-utils/src"
17+
],
18+
"build_cache": true,
19+
"optimistic_loop": true,
20+
"process": "emv",
21+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
22+
"smt_timeout": "2000",
23+
"solc": "solc8.10",
24+
"verify": "GhoCcipSteward_Harness:certora/steward/specs/GhoCcipSteward.spec",
25+
"rule_sanity": "basic",
26+
"msg": "GhoCcipSteward: all rules"
27+
}
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
{
22
"files": [
3-
"certora/steward/harness/GhoStewardV2_Harness.sol",
4-
"src/contracts/facilitators/aave/interestStrategy/FixedRateStrategyFactory.sol"
3+
"certora/steward/harness/GhoGsmSteward_Harness.sol",
4+
"src/contracts/facilitators/gsm/feeStrategy/FixedFeeStrategyFactory.sol"
55
],
66
"link": [
7-
"GhoStewardV2_Harness:FIXED_RATE_STRATEGY_FACTORY=FixedRateStrategyFactory",
7+
"GhoGsmSteward_Harness:FIXED_FEE_STRATEGY_FACTORY=FixedFeeStrategyFactory",
88
],
99
"packages": [
1010
"@aave/core-v3/=lib/aave-v3-core",
@@ -21,13 +21,13 @@
2121
"openzeppelin-contracts/=lib/aave-stk-v1-5/lib/openzeppelin-contracts",
2222
"solidity-utils/=lib/solidity-utils/src"
2323
],
24+
"build_cache": true,
2425
"optimistic_loop": true,
25-
"prover_args": ["-depth 15","-mediumTimeout 1000","-cache none"],
26+
"process": "emv",
27+
"prover_args": ["-depth 15","-mediumTimeout 1000"],
2628
"smt_timeout": "2000",
2729
"solc": "solc8.10",
28-
"verify": "GhoStewardV2_Harness:certora/steward/specs/rules.spec",
29-
"rule": ["sanity"],
30-
"disable_auto_cache_key_gen" :true,
31-
"cache" :"none",
32-
"msg": "STEWARD::sanity"
30+
"verify": "GhoGsmSteward_Harness:certora/steward/specs/GhoGsmSteward.spec",
31+
"rule_sanity": "basic",
32+
"msg": "GhoGsmSteward: all rules"
3333
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.10;
3+
4+
import {GhoAaveSteward} from '../munged/src/contracts/misc/GhoAaveSteward.sol';
5+
6+
contract GhoAaveSteward_Harness is GhoAaveSteward {
7+
constructor(
8+
address owner,
9+
address addressesProvider,
10+
address poolDataProvider,
11+
address ghoToken,
12+
address riskCouncil,
13+
BorrowRateConfig memory borrowRateConfig
14+
)
15+
GhoAaveSteward(
16+
owner,
17+
addressesProvider,
18+
poolDataProvider,
19+
ghoToken,
20+
riskCouncil,
21+
borrowRateConfig
22+
)
23+
{}
24+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.10;
3+
4+
import {GhoCcipSteward} from '../../../src/contracts/misc/GhoCcipSteward.sol';
5+
6+
contract GhoCcipSteward_Harness is GhoCcipSteward {
7+
constructor(
8+
address ghoToken,
9+
address ghoTokenPool,
10+
address riskCouncil,
11+
bool bridgeLimitEnabled
12+
) GhoCcipSteward(ghoToken, ghoTokenPool, riskCouncil, bridgeLimitEnabled) {}
13+
14+
function getCcipTimelocks() external view returns (CcipDebounce memory) {
15+
return _ccipTimelocks;
16+
}
17+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// SPDX-License-Identifier: MIT
2+
pragma solidity ^0.8.10;
3+
4+
import {GhoGsmSteward} from '../../../src/contracts/misc/GhoGsmSteward.sol';
5+
6+
contract GhoGsmSteward_Harness is GhoGsmSteward {
7+
constructor(
8+
address fixedRateStrategyFactory,
9+
address riskCouncil
10+
) GhoGsmSteward(fixedRateStrategyFactory, riskCouncil) {}
11+
}

certora/steward/munged/.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
*
2+
!.gitignore

0 commit comments

Comments
 (0)