Skip to content

Commit 1182c20

Browse files
committed
fix: lint certora fv
1 parent 12110a3 commit 1182c20

25 files changed

+500
-532
lines changed

.github/workflows/certora-ATokenWithDelegation.yml

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ jobs:
3535
cd certora/atoken-with-delegation
3636
touch applyHarness.patch
3737
make munged
38-
38+
3939
- uses: Certora/certora-run-action@v1
4040
with:
4141
cli-version: 7.31.0
@@ -49,7 +49,7 @@ jobs:
4949
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule vp_change_of_balance_affect_power_NON_DELEGATEE
5050
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_in_balance_affect_power_DELEGATEE
5151
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_of_balance_affect_power_NON_DELEGATEE
52-
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule no_function_changes_both_balance_and_delegation_state
52+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule no_function_changes_both_balance_and_delegation_state
5353
solc-versions: 0.8.27
5454
comment-fail-only: false
5555
solc-remove-version-prefix: "0."
@@ -58,11 +58,3 @@ jobs:
5858
install-java: true
5959
env:
6060
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
61-
62-
63-
64-
65-
66-
67-
68-

.github/workflows/certora-basic.yml

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -64,8 +64,6 @@ jobs:
6464
install-java: true
6565
env:
6666
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
67-
68-
6967
# Put back the following rule after ticket 8889 is closed
70-
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
68+
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
7169

.github/workflows/certora-math-calculations.yml

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -50,8 +50,6 @@ jobs:
5050
install-java: true
5151
env:
5252
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
53-
54-
5553
# Put back the following rule after ticket 8889 is closed
56-
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
54+
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
5755

.github/workflows/certora-solvency.yml

Lines changed: 2 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ jobs:
6161
certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetINloop.conf
6262
certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetNOTINloop.conf
6363
certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf
64-
certora/solvency/confs/solvency/liquidationCall/lemma-SAMEasset.conf
64+
certora/solvency/confs/solvency/liquidationCall/lemma-SAMEasset.conf
6565
solc-versions: 0.8.27
6666
comment-fail-only: false
6767
solc-remove-version-prefix: "0."
@@ -70,21 +70,6 @@ jobs:
7070
install-java: true
7171
env:
7272
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
73-
74-
7573
# Put back the following rule after ticket 8889 is closed
76-
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
77-
78-
79-
80-
81-
82-
83-
84-
85-
86-
87-
88-
89-
74+
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
9075

.github/workflows/certora-stata.yml

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ jobs:
3535
cd certora/stata
3636
touch applyHarness.patch
3737
make munged
38-
38+
3939
- uses: Certora/certora-run-action@v1
4040
with:
4141
cli-version: 7.31.0
@@ -71,5 +71,3 @@ jobs:
7171
install-java: true
7272
env:
7373
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
74-
75-

certora/atoken-with-delegation/harness/ATokenWithDelegation_Harness.sol

Lines changed: 97 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -4,95 +4,98 @@
44
This is an extension of the ATokenWithDelegation with added getters.
55
*/
66

7-
8-
97
pragma solidity ^0.8.0;
108

119
import {ATokenWithDelegationInstance} from 'certora/atoken-with-delegation/munged/src/contracts/instances/ATokenWithDelegationInstance.sol';
1210
import {ScaledBalanceTokenBase} from 'certora/atoken-with-delegation/munged/src/contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol';
1311

14-
import {IPool} from 'certora/atoken-with-delegation/munged/src/contracts/interfaces/IPool.sol';
12+
import {IPool} from 'certora/atoken-with-delegation/munged/src/contracts/interfaces/IPool.sol';
1513

1614
import {IScaledBalanceToken} from 'certora/atoken-with-delegation/munged/src/contracts/interfaces/IScaledBalanceToken.sol';
1715
import {WadRayMath} from 'certora/atoken-with-delegation/munged/src/contracts/protocol/libraries/math/WadRayMath.sol';
1816
import {DelegationMode} from 'certora/atoken-with-delegation/munged/src/contracts/protocol/tokenization/base/DelegationMode.sol';
1917
import {BaseDelegation} from 'certora/atoken-with-delegation/munged/src/contracts/protocol/tokenization/delegation/BaseDelegation.sol';
2018

21-
22-
2319
contract ATokenWithDelegation_Harness is ATokenWithDelegationInstance {
24-
using WadRayMath for uint256;
25-
26-
constructor(IPool pool, address rewardsController, address treasury) ATokenWithDelegationInstance(pool,rewardsController,treasury) {}
27-
28-
function getBalance(address user) public view returns (uint120) {
29-
return _userState[user].balance;
30-
}
31-
32-
// returns user's delegated proposition balance
33-
function getDelegatedPropositionBalance(address user) public view returns (uint72) {
34-
return _getDelegationState(user).delegatedPropositionBalance;
35-
}
36-
37-
// returns user's delegated voting balance
38-
function getDelegatedVotingBalance(address user) public view returns (uint72) {
39-
return _getDelegationState(user).delegatedVotingBalance;
40-
}
41-
42-
//returns user's delegating proposition status
43-
function isDelegatingProposition(address user) public view returns (bool) {
44-
return
45-
_userState[user].delegationMode == DelegationMode.PROPOSITION_DELEGATED ||
46-
_userState[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
47-
}
48-
49-
// returns user's delegating voting status
50-
function isDelegatingVoting(address user) public view returns (bool) {
51-
return
52-
_userState[user].delegationMode == DelegationMode.VOTING_DELEGATED ||
53-
_userState[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
54-
}
55-
56-
// returns user's voting delegate
57-
function getVotingDelegatee(address user) public view returns (address) {
58-
return _votingDelegatee[user];
59-
}
60-
61-
// returns user's proposition delegate
62-
function getPropositionDelegatee(address user) public view returns (address) {
63-
return _propositionDelegatee[user];
64-
}
65-
66-
// returns user's delegation state
67-
function getDelegationMode(address user) public view returns (DelegationMode) {
68-
return _userState[user].delegationMode;
69-
}
70-
71-
72-
function scaledTotalSupply() public view override(IScaledBalanceToken,ScaledBalanceTokenBase) returns (uint256) {
73-
uint256 val = super.scaledTotalSupply();
74-
return val;
75-
}
76-
77-
function additionalData(address user) public view returns (uint128) {
78-
return _userState[user].additionalData;
79-
}
80-
81-
function scaledBalance_to_balance(uint256 bal) public view returns (uint256) {
82-
return bal.rayMul(POOL.getReserveNormalizedIncome(_underlyingAsset));
83-
}
84-
85-
86-
//The following are for the comuunity rules
87-
function ecrecoverWrapper(
88-
bytes32 hash,
89-
uint8 v,
90-
bytes32 r,
91-
bytes32 s
92-
) public pure returns (address) {
93-
return ecrecover(hash, v, r, s);
94-
}
95-
/*
20+
using WadRayMath for uint256;
21+
22+
constructor(
23+
IPool pool,
24+
address rewardsController,
25+
address treasury
26+
) ATokenWithDelegationInstance(pool, rewardsController, treasury) {}
27+
28+
function getBalance(address user) public view returns (uint120) {
29+
return _userState[user].balance;
30+
}
31+
32+
// returns user's delegated proposition balance
33+
function getDelegatedPropositionBalance(address user) public view returns (uint72) {
34+
return _getDelegationState(user).delegatedPropositionBalance;
35+
}
36+
37+
// returns user's delegated voting balance
38+
function getDelegatedVotingBalance(address user) public view returns (uint72) {
39+
return _getDelegationState(user).delegatedVotingBalance;
40+
}
41+
42+
//returns user's delegating proposition status
43+
function isDelegatingProposition(address user) public view returns (bool) {
44+
return
45+
_userState[user].delegationMode == DelegationMode.PROPOSITION_DELEGATED ||
46+
_userState[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
47+
}
48+
49+
// returns user's delegating voting status
50+
function isDelegatingVoting(address user) public view returns (bool) {
51+
return
52+
_userState[user].delegationMode == DelegationMode.VOTING_DELEGATED ||
53+
_userState[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
54+
}
55+
56+
// returns user's voting delegate
57+
function getVotingDelegatee(address user) public view returns (address) {
58+
return _votingDelegatee[user];
59+
}
60+
61+
// returns user's proposition delegate
62+
function getPropositionDelegatee(address user) public view returns (address) {
63+
return _propositionDelegatee[user];
64+
}
65+
66+
// returns user's delegation state
67+
function getDelegationMode(address user) public view returns (DelegationMode) {
68+
return _userState[user].delegationMode;
69+
}
70+
71+
function scaledTotalSupply()
72+
public
73+
view
74+
override(IScaledBalanceToken, ScaledBalanceTokenBase)
75+
returns (uint256)
76+
{
77+
uint256 val = super.scaledTotalSupply();
78+
return val;
79+
}
80+
81+
function additionalData(address user) public view returns (uint128) {
82+
return _userState[user].additionalData;
83+
}
84+
85+
function scaledBalance_to_balance(uint256 bal) public view returns (uint256) {
86+
return bal.rayMul(POOL.getReserveNormalizedIncome(_underlyingAsset));
87+
}
88+
89+
//The following are for the comuunity rules
90+
function ecrecoverWrapper(
91+
bytes32 hash,
92+
uint8 v,
93+
bytes32 r,
94+
bytes32 s
95+
) public pure returns (address) {
96+
return ecrecover(hash, v, r, s);
97+
}
98+
/*
9699
function computeMetaDelegateHash(address delegator, address delegatee, uint256 deadline, uint256 nonce)
97100
public view returns (bytes32) {
98101
bytes32 digest =
@@ -127,15 +130,21 @@ contract ATokenWithDelegation_Harness is ATokenWithDelegationInstance {
127130
return digest;
128131
}
129132
*/
130-
function getPowerCurrent_BaseDelegation(address user, GovernancePowerType delegationType)
131-
public view virtual returns (uint256) {
132-
return BaseDelegation.getPowerCurrent(user,delegationType);
133-
}
134-
135-
function getNonce(address user) public view returns (uint256) {
136-
return _nonces[user];
137-
}
138-
139-
function rayMul_WRP(uint256 a, uint256 b) external returns (uint256) {return a.rayMul(b);}
140-
function rayDiv_WRP(uint256 a, uint256 b) external returns (uint256) {return a.rayDiv(b);}
133+
function getPowerCurrent_BaseDelegation(
134+
address user,
135+
GovernancePowerType delegationType
136+
) public view virtual returns (uint256) {
137+
return BaseDelegation.getPowerCurrent(user, delegationType);
138+
}
139+
140+
function getNonce(address user) public view returns (uint256) {
141+
return _nonces[user];
142+
}
143+
144+
function rayMul_WRP(uint256 a, uint256 b) external returns (uint256) {
145+
return a.rayMul(b);
146+
}
147+
function rayDiv_WRP(uint256 a, uint256 b) external returns (uint256) {
148+
return a.rayDiv(b);
149+
}
141150
}

0 commit comments

Comments
 (0)