Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix partial redemption stake update #789

Merged
merged 17 commits into from
Mar 10, 2024
Merged

fix partial redemption stake update #789

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
b84d323
fix partial redemption stake update
rayeaster Mar 6, 2024
5a44f60
add update event for stake on failed partial redemption
Mar 6, 2024
4361708
Adding CDP stake related invariants
wtj2021 Mar 6, 2024
c45acde
cannot redeem last CDP
wtj2021 Mar 6, 2024
06ca316
debugging CDPM-09
wtj2021 Mar 7, 2024
28ef54a
removing CDPM-9 from partialLiquidate
wtj2021 Mar 7, 2024
394e181
updating properties
wtj2021 Mar 7, 2024
1d9c933
fixing invariants
wtj2021 Mar 7, 2024
96b13f1
removing bad import
wtj2021 Mar 7, 2024
8490e1e
setting solc version
wtj2021 Mar 7, 2024
4022621
adding remapping
wtj2021 Mar 7, 2024
e58c1f3
remapping
wtj2021 Mar 7, 2024
d423cea
removing remappings
wtj2021 Mar 8, 2024
24d5a29
Merge pull request #791 from ebtc-protocol/adding-invariants-around-s…
wtj2021 Mar 8, 2024
e841fbc
Merge remote-tracking branch 'origin/release-0.8' into feat/fixPartia…
Mar 10, 2024
5dc6669
fix E2F redemption params
Mar 10, 2024
e5703ed
remove known broken test
Mar 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions packages/contracts/contracts/CRLens.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,16 @@ contract CRLens {
return icr;
}

function getRealStake(bytes32 cdpId) external returns (uint256) {
cdpManager.syncAccounting(cdpId);
uint256 collShares = cdpManager.getCdpCollShares(cdpId);
return
cdpManager.totalCollateralSnapshot() == 0
? collShares
: (collShares * cdpManager.totalStakesSnapshot()) /
cdpManager.totalCollateralSnapshot();
}

/// @dev Returns 1 if we're in RM
function getCheckRecoveryMode(bool revertValue) external returns (uint256) {
// Synch State
Expand Down
14 changes: 14 additions & 0 deletions packages/contracts/contracts/CdpManager.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,6 +192,20 @@ contract CdpManager is CdpManagerStorage, ICdpManager, Proxy {
collateral.getPooledEthByShares(newColl) < MIN_NET_STETH_BALANCE ||
newDebt < MIN_CHANGE
) {
_updateStakeAndTotalStakes(_redeemColFromCdp.cdpId);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The addition of _updateStakeAndTotalStakes before marking a partial redemption as cancelled is a critical change to ensure accurate stake accounting during partial redemptions. This adjustment appears to address the identified issue effectively. However, it's essential to consider a few aspects:

  • Reentrancy: Ensure that the _updateStakeAndTotalStakes function does not introduce reentrancy vulnerabilities. Given the context, it seems unlikely, but it's always good practice to review the function's implementation for any external calls or state changes that could be exploited.
  • Gas Costs: This change could increase the gas cost for transactions involving partial redemptions. It would be beneficial to evaluate the impact on gas costs to ensure that it remains within acceptable limits for users.
  • State Changes: Confirm that this state change (updating stakes) is appropriate at this point in the contract's execution flow. It's crucial that this update does not interfere with other parts of the contract logic or lead to inconsistencies in the contract's state.

Overall, the change seems necessary and well-justified based on the PR objectives. However, a thorough review of the mentioned aspects is recommended to ensure the contract's integrity and security.


emit CdpUpdated(
_redeemColFromCdp.cdpId,
ISortedCdps(sortedCdps).getOwnerAddress(_redeemColFromCdp.cdpId),
msg.sender,
_oldDebtAndColl.debt,
_oldDebtAndColl.collShares,
_oldDebtAndColl.debt,
_oldDebtAndColl.collShares,
Cdps[_redeemColFromCdp.cdpId].stake,
CdpOperation.failedPartialRedemption
);

singleRedemption.cancelledPartial = true;
return singleRedemption;
}
Expand Down
7 changes: 6 additions & 1 deletion packages/contracts/contracts/Interfaces/ICdpManagerData.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,8 @@ interface ICdpManagerData is IRecoveryModeGracePeriod {
liquidateInNormalMode,
liquidateInRecoveryMode,
redeemCollateral,
partiallyLiquidate
partiallyLiquidate,
failedPartialRedemption
}

enum Status {
Expand Down Expand Up @@ -265,4 +266,8 @@ interface ICdpManagerData is IRecoveryModeGracePeriod {
) external view returns (uint256 debt, uint256 collShares);

function canLiquidateRecoveryMode(uint256 icr, uint256 tcr) external view returns (bool);

function totalCollateralSnapshot() external view returns (uint256);

function totalStakesSnapshot() external view returns (uint256);
}
26 changes: 23 additions & 3 deletions packages/contracts/contracts/TestContracts/invariants/BeforeAfter.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,8 @@ abstract contract BeforeAfter is BaseStorageVariables {
uint256 cdpCollAfter;
uint256 cdpDebtBefore;
uint256 cdpDebtAfter;
uint256 cdpStakeBefore;
uint256 cdpStakeAfter;
uint256 liquidatorRewardSharesBefore;
uint256 liquidatorRewardSharesAfter;
uint256 sortedCdpsSizeBefore;
Expand Down Expand Up @@ -73,6 +75,12 @@ abstract contract BeforeAfter is BaseStorageVariables {
uint256 cumulativeCdpsAtTimeOfRebase;
uint256 prevStEthFeeIndex;
uint256 afterStEthFeeIndex;
uint256 totalStakesBefore;
uint256 totalStakesAfter;
uint256 totalStakesSnapshotBefore;
uint256 totalStakesSnapshotAfter;
uint256 totalCollateralSnapshotBefore;
uint256 totalCollateralSnapshotAfter;
}

Vars vars;
Expand All @@ -87,14 +95,15 @@ abstract contract BeforeAfter is BaseStorageVariables {
address ownerToCheck = sortedCdps.getOwnerAddress(_cdpId);
vars.userSurplusBefore = collSurplusPool.getSurplusCollShares(ownerToCheck);

(uint256 debtBefore, ) = cdpManager.getSyncedDebtAndCollShares(_cdpId);
(uint256 debtBefore, uint256 collBefore) = cdpManager.getSyncedDebtAndCollShares(_cdpId);

vars.nicrBefore = _cdpId != bytes32(0) ? crLens.quoteRealNICR(_cdpId) : 0;
vars.icrBefore = _cdpId != bytes32(0)
? cdpManager.getCachedICR(_cdpId, vars.priceBefore)
: 0;
vars.cdpCollBefore = _cdpId != bytes32(0) ? cdpManager.getCdpCollShares(_cdpId) : 0;
vars.cdpCollBefore = _cdpId != bytes32(0) ? collBefore : 0;
vars.cdpDebtBefore = _cdpId != bytes32(0) ? debtBefore : 0;
vars.cdpStakeBefore = _cdpId != bytes32(0) ? crLens.getRealStake(_cdpId) : 0;
vars.liquidatorRewardSharesBefore = _cdpId != bytes32(0)
? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
: 0;
Expand Down Expand Up @@ -142,6 +151,10 @@ abstract contract BeforeAfter is BaseStorageVariables {
1e18 -
vars.activePoolDebtBefore;
vars.prevStEthFeeIndex = cdpManager.systemStEthFeePerUnitIndex();

vars.totalStakesBefore = cdpManager.totalStakes();
vars.totalStakesSnapshotBefore = cdpManager.totalStakesSnapshot();
vars.totalCollateralSnapshotBefore = cdpManager.totalCollateralSnapshot();
}

function _after(bytes32 _cdpId) internal {
Expand All @@ -150,10 +163,13 @@ abstract contract BeforeAfter is BaseStorageVariables {

vars.priceAfter = priceFeedMock.fetchPrice();

(, uint256 collAfter) = cdpManager.getSyncedDebtAndCollShares(_cdpId);

vars.nicrAfter = _cdpId != bytes32(0) ? crLens.quoteRealNICR(_cdpId) : 0;
vars.icrAfter = _cdpId != bytes32(0) ? cdpManager.getCachedICR(_cdpId, vars.priceAfter) : 0;
vars.cdpCollAfter = _cdpId != bytes32(0) ? cdpManager.getCdpCollShares(_cdpId) : 0;
vars.cdpCollAfter = _cdpId != bytes32(0) ? collAfter : 0;
vars.cdpDebtAfter = _cdpId != bytes32(0) ? cdpManager.getCdpDebt(_cdpId) : 0;
vars.cdpStakeAfter = _cdpId != bytes32(0) ? crLens.getRealStake(_cdpId) : 0;
vars.liquidatorRewardSharesAfter = _cdpId != bytes32(0)
? cdpManager.getCdpLiquidatorRewardShares(_cdpId)
: 0;
Expand Down Expand Up @@ -208,6 +224,10 @@ abstract contract BeforeAfter is BaseStorageVariables {
if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
vars.cumulativeCdpsAtTimeOfRebase += cdpManager.getActiveCdpsCount();
}

vars.totalStakesAfter = cdpManager.totalStakes();
vars.totalStakesSnapshotAfter = cdpManager.totalStakesSnapshot();
vars.totalCollateralSnapshotAfter = cdpManager.totalCollateralSnapshot();
}

function _diff() internal view returns (string memory log) {
Expand Down
29 changes: 29 additions & 0 deletions packages/contracts/contracts/TestContracts/invariants/Properties.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,35 @@ abstract contract Properties is BeforeAfter, PropertiesDescriptions, Asserts, Pr
isApproximateEq(vars.valueInSystemAfter, vars.valueInSystemBefore, 0.01e18);
}

function invariant_CDPM_10(CdpManager cdpManager) internal view returns (bool) {
if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
return cdpManager.totalStakesSnapshot() == cdpManager.totalStakes();
}
return true;
}

function invariant_CDPM_11(CdpManager cdpManager) internal view returns (bool) {
if (vars.afterStEthFeeIndex > vars.prevStEthFeeIndex) {
return cdpManager.totalCollateralSnapshot() == cdpManager.getSystemCollShares();
}
return true;
}

function invariant_CDPM_12(
SortedCdps sortedCdps,
Vars memory vars
) internal view returns (bool) {
bytes32 currentCdp = sortedCdps.getFirst();

uint256 sumStakes;
while (currentCdp != bytes32(0)) {
sumStakes += cdpManager.getCdpStake(currentCdp);
currentCdp = sortedCdps.getNext(currentCdp);
}

return sumStakes == vars.totalStakesAfter;
}

function invariant_CSP_01(
ICollateralToken collateral,
CollSurplusPool collSurplusPool
Expand Down
10 changes: 10 additions & 0 deletions packages/contracts/contracts/TestContracts/invariants/PropertiesDescriptions.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,16 @@ abstract contract PropertiesDescriptions {
string constant CDPM_04 = "CDPM-04: The total system value does not decrease during redemptions";
string constant CDPM_05 = "CDPM-05: Redemptions do not increase the total system debt";
string constant CDPM_06 = "CDPM-06: Redemptions do not increase the total system debt";
string constant CDPM_07 = "CDPM-07: Stake decreases when collShares decreases for a CDP";
string constant CDPM_08 = "CDPM-08: Stake increases when collShares increases for a CDP";
string constant CDPM_09 =
"CDPM-09: expectedStake = coll * totalStakesSnapshot / totalCollateralSnapshot after every operation involving a CDP";
string constant CDPM_10 =
"CDPM-10: totalStakesSnapshot matches totalStakes after an operation, if rebase index changed during the OP";
string constant CDPM_11 =
"CDPM-11: totalCollateralSnapshot matches activePool.systemCollShares after an operation, if rebase index changed during the OP";
string constant CDPM_12 =
"CDPM-12: Sum of all individual CDP stakes should equal to totalStakes";

///////////////////////////////////////////////////////
// Collateral Surplus Pool
Expand Down
53 changes: 52 additions & 1 deletion packages/contracts/contracts/TestContracts/invariants/TargetFunctions.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -287,6 +287,8 @@ abstract contract TargetFunctions is Properties {
lt(cdpManager.lastEBTCDebtErrorRedistribution(), cdpManager.totalStakes(), L_17);
totalCdpDustMaxCap += cdpManager.getActiveCdpsCount();
}

_checkStakeInvariants();
} else if (vars.sortedCdpsSizeBefore > _i) {
assertRevertReasonNotEqual(returnData, "Panic(17)");
}
Expand Down Expand Up @@ -379,6 +381,27 @@ abstract contract TargetFunctions is Properties {
}
}

function _checkStakeInvariants() private {
if (vars.cdpCollAfter < vars.cdpCollBefore) {
lt(vars.cdpStakeAfter, vars.cdpStakeBefore, CDPM_07);
}

if (vars.cdpCollAfter > vars.cdpCollBefore) {
gt(vars.cdpStakeAfter, vars.cdpStakeBefore, CDPM_08);
}

if (vars.totalCollateralSnapshotAfter > 0) {
eq(
vars.cdpStakeAfter,
(vars.cdpCollAfter * vars.totalStakesSnapshotAfter) /
vars.totalCollateralSnapshotAfter,
CDPM_09
);
} else {
eq(vars.cdpStakeAfter, vars.cdpCollAfter, CDPM_09);
}
}
Comment on lines +384 to +403
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The _checkStakeInvariants() function is a crucial addition for ensuring stake consistency. However, there are a few points to consider:

  • The function is marked as private, which is appropriate since it's an internal consistency check. However, ensure that this aligns with the intended use case and that no external contracts require access to this function.

  • The logic within the function appears sound, checking for changes in collateral and stake amounts and ensuring that the stake after is calculated correctly based on the total stakes and collateral snapshots. This is a good practice for maintaining data integrity.

  • It's important to ensure that all variables used within this function (vars.cdpCollAfter, vars.cdpCollBefore, etc.) are accurately updated before this function is called. Any discrepancies in these values could lead to incorrect invariant checks.

  • Consider adding more detailed comments explaining the purpose of each check within the function. This will improve maintainability and understandability for future developers.

  • Ensure comprehensive testing of this function, particularly edge cases where values might be close to the limits of their expected ranges.


/** Active Pool TWAP Revert Checks */
function observe() public {
// We verify that any observation will never revert
Expand Down Expand Up @@ -473,6 +496,8 @@ abstract contract TargetFunctions is Properties {
lt(cdpManager.lastEBTCDebtErrorRedistribution(), cdpManager.totalStakes(), L_17);
totalCdpDustMaxCap += cdpManager.getActiveCdpsCount();
}

_checkStakeInvariants();
} else if (vars.sortedCdpsSizeBefore > _n) {
if (_atLeastOneCdpIsLiquidatable(cdpsBefore, vars.isRecoveryModeBefore)) {
assertRevertReasonNotEqual(returnData, "Panic(17)");
Expand All @@ -492,6 +517,7 @@ abstract contract TargetFunctions is Properties {
_partialRedemptionHintNICR,
false,
false,
false,
_maxFeePercentage,
_maxIterations
);
Expand All @@ -503,6 +529,7 @@ abstract contract TargetFunctions is Properties {
uint256 _partialRedemptionHintNICRFromMedusa,
bool useProperFirstHint,
bool useProperPartialHint,
bool failPartialRedemption,
uint _maxFeePercentage,
uint _maxIterations
) public setup {
Expand All @@ -512,6 +539,7 @@ abstract contract TargetFunctions is Properties {
_partialRedemptionHintNICRFromMedusa,
useProperFirstHint,
useProperPartialHint,
failPartialRedemption,
_maxFeePercentage,
_maxIterations
);
Expand All @@ -523,9 +551,12 @@ abstract contract TargetFunctions is Properties {
uint256 _partialRedemptionHintNICRFromMedusa,
bool useProperFirstHint,
bool useProperPartialHint,
bool failPartialRedemption,
uint _maxFeePercentage,
uint _maxIterations
) internal {
require(cdpManager.getActiveCdpsCount() > 1, "Cannot redeem last CDP");

_EBTCAmount = between(_EBTCAmount, 0, eBTCToken.balanceOf(address(actor)));

_maxIterations = between(_maxIterations, 0, 10);
Expand Down Expand Up @@ -568,7 +599,7 @@ abstract contract TargetFunctions is Properties {
_firstRedemptionHintFromMedusa,
bytes32(0),
bytes32(0),
_partialRedemptionHintNICRFromMedusa,
failPartialRedemption ? 0 : _partialRedemptionHintNICRFromMedusa,
_maxIterations,
_maxFeePercentage
)
Expand Down Expand Up @@ -614,6 +645,8 @@ abstract contract TargetFunctions is Properties {
if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
}

_checkStakeInvariants();
}

///////////////////////////////////////////////////////
Expand Down Expand Up @@ -671,6 +704,8 @@ abstract contract TargetFunctions is Properties {
if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
}

_checkStakeInvariants();
}

///////////////////////////////////////////////////////
Expand Down Expand Up @@ -725,6 +760,8 @@ abstract contract TargetFunctions is Properties {
if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
}

_checkStakeInvariants();
}

function openCdp(uint256 _col, uint256 _EBTCAmount) public setup returns (bytes32 _cdpId) {
Expand Down Expand Up @@ -808,6 +845,8 @@ abstract contract TargetFunctions is Properties {
gte(_EBTCAmount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);
require(invariant_BO_09(cdpManager, priceFeedMock.getPrice(), _cdpId), BO_09);

_checkStakeInvariants();
} else {
assertRevertReasonNotEqual(returnData, "Panic(17)"); /// Done
}
Expand Down Expand Up @@ -908,6 +947,8 @@ abstract contract TargetFunctions is Properties {
}

gte(_coll, borrowerOperations.MIN_CHANGE(), GENERAL_16);

_checkStakeInvariants();
} else {
assertRevertReasonNotEqual(returnData, "Panic(17)");
}
Expand Down Expand Up @@ -978,6 +1019,8 @@ abstract contract TargetFunctions is Properties {
}

gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);

_checkStakeInvariants();
} else {
assertRevertReasonNotEqual(returnData, "Panic(17)");
}
Expand Down Expand Up @@ -1050,6 +1093,8 @@ abstract contract TargetFunctions is Properties {

gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);

_checkStakeInvariants();
} else {
assertRevertReasonNotEqual(returnData, "Panic(17)");
}
Expand Down Expand Up @@ -1122,6 +1167,8 @@ abstract contract TargetFunctions is Properties {

gte(_amount, borrowerOperations.MIN_CHANGE(), GENERAL_16);
gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);

_checkStakeInvariants();
} else {
assertRevertReasonNotEqual(returnData, "Panic(17)");
}
Expand Down Expand Up @@ -1198,6 +1245,8 @@ abstract contract TargetFunctions is Properties {
if (vars.isRecoveryModeBefore && !vars.isRecoveryModeAfter) {
t(!vars.lastGracePeriodStartTimestampIsSetAfter, L_16);
}

_checkStakeInvariants();
} else {
assertRevertReasonNotEqual(returnData, "Panic(17)");
}
Expand Down Expand Up @@ -1285,6 +1334,8 @@ abstract contract TargetFunctions is Properties {
}
}
gte(vars.cdpDebtAfter, borrowerOperations.MIN_CHANGE(), GENERAL_15);

_checkStakeInvariants();
}

///////////////////////////////////////////////////////
Expand Down
12 changes: 12 additions & 0 deletions packages/contracts/contracts/TestContracts/invariants/echidna/EchidnaProperties.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,18 @@ abstract contract EchidnaProperties is TargetContractSetup, Properties {
return invariant_CDPM_03(cdpManager);
}

function echidna_cdp_manager_invariant_10() public returns (bool) {
return invariant_CDPM_10(cdpManager);
}

function echidna_cdp_manager_invariant_11() public returns (bool) {
return invariant_CDPM_11(cdpManager);
}

function echidna_cdp_manager_invariant_12() public returns (bool) {
return invariant_CDPM_12(sortedCdps, vars);
}

// CDPM_04 is a vars invariant

function echidna_coll_surplus_pool_invariant_1() public returns (bool) {
Expand Down
1 change: 1 addition & 0 deletions packages/contracts/foundry.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ test = 'foundry_test'
cache_path = 'forge-cache'
gas_reports = ["*"]
no_match_contract = 'Echidna'
solc_version= '0.8.17'

evm_version = 'london'

Expand Down
Loading
Loading