From ebba848040637b399a2e98ab8c0825fc4252d876 Mon Sep 17 00:00:00 2001 From: Entreprenerd Date: Mon, 4 Nov 2024 20:27:49 +0100 Subject: [PATCH 1/2] feat: remove incorrectly broken properties --- echidna.yaml | 8 +- .../properties/BribeInitiativeProperties.sol | 96 +++++++++---------- .../properties/OptimizationProperties.sol | 86 ++--------------- 3 files changed, 59 insertions(+), 131 deletions(-) diff --git a/echidna.yaml b/echidna.yaml index fc2a82f3..21c707d2 100644 --- a/echidna.yaml +++ b/echidna.yaml @@ -1,8 +1,10 @@ -testMode: "assertion" -prefix: "crytic_" +testMode: "property" +prefix: "optimize_" coverage: true corpusDir: "echidna" balanceAddr: 0x1043561a8829300000 balanceContract: 0x1043561a8829300000 filterFunctions: [] -cryticArgs: ["--foundry-compile-all"] \ No newline at end of file +cryticArgs: ["--foundry-compile-all"] + +shrinkLimit: 100000 diff --git a/test/recon/properties/BribeInitiativeProperties.sol b/test/recon/properties/BribeInitiativeProperties.sol index 8fde6553..1ae8ea45 100644 --- a/test/recon/properties/BribeInitiativeProperties.sol +++ b/test/recon/properties/BribeInitiativeProperties.sol @@ -108,54 +108,54 @@ abstract contract BribeInitiativeProperties is BeforeAfter { // See what the result is // See the dust // Dust cap check - function property_BI05() public { - // users can't claim for current epoch so checking for previous - uint16 checkEpoch = governance.epoch() - 1; - - for (uint8 i; i < deployedInitiatives.length; i++) { - address initiative = deployedInitiatives[i]; - // for any epoch: expected balance = Bribe - claimed bribes, actual balance = bribe token balance of initiative - // so if the delta between the expected and actual is > 0, dust is being collected - - uint256 lqtyClaimedAccumulator; - uint256 lusdClaimedAccumulator; - for (uint8 j; j < users.length; j++) { - // if the bool switches, the user has claimed their bribe for the epoch - if ( - _before.claimedBribeForInitiativeAtEpoch[initiative][user][checkEpoch] - != _after.claimedBribeForInitiativeAtEpoch[initiative][user][checkEpoch] - ) { - // add user claimed balance delta to the accumulator - lqtyClaimedAccumulator += _after.userLqtyBalance[users[j]] - _before.userLqtyBalance[users[j]]; - lusdClaimedAccumulator += _after.userLqtyBalance[users[j]] - _before.userLqtyBalance[users[j]]; - } - } - - (uint128 boldAmount, uint128 bribeTokenAmount) = IBribeInitiative(initiative).bribeByEpoch(checkEpoch); - - // shift 128 bit to the right to get the most significant bits of the accumulator (256 - 128 = 128) - uint128 lqtyClaimedAccumulator128 = uint128(lqtyClaimedAccumulator >> 128); - uint128 lusdClaimedAccumulator128 = uint128(lusdClaimedAccumulator >> 128); - - // find delta between bribe and claimed amount (how much should be remaining in contract) - uint128 lusdDelta = boldAmount - lusdClaimedAccumulator128; - uint128 lqtyDelta = bribeTokenAmount - lqtyClaimedAccumulator128; - - uint128 initiativeLusdBalance = uint128(lusd.balanceOf(initiative) >> 128); - uint128 initiativeLqtyBalance = uint128(lqty.balanceOf(initiative) >> 128); - - lte( - lusdDelta - initiativeLusdBalance, - 1e8, - "BI-05: Bold token dust amount remaining after claiming should be less than 100 million wei" - ); - lte( - lqtyDelta - initiativeLqtyBalance, - 1e8, - "BI-05: Bribe token dust amount remaining after claiming should be less than 100 million wei" - ); - } - } + // function property_BI05() public { + // // users can't claim for current epoch so checking for previous + // uint16 checkEpoch = governance.epoch() - 1; + + // for (uint8 i; i < deployedInitiatives.length; i++) { + // address initiative = deployedInitiatives[i]; + // // for any epoch: expected balance = Bribe - claimed bribes, actual balance = bribe token balance of initiative + // // so if the delta between the expected and actual is > 0, dust is being collected + + // uint256 lqtyClaimedAccumulator; + // uint256 lusdClaimedAccumulator; + // for (uint8 j; j < users.length; j++) { + // // if the bool switches, the user has claimed their bribe for the epoch + // if ( + // _before.claimedBribeForInitiativeAtEpoch[initiative][user][checkEpoch] + // != _after.claimedBribeForInitiativeAtEpoch[initiative][user][checkEpoch] + // ) { + // // add user claimed balance delta to the accumulator + // lqtyClaimedAccumulator += _after.userLqtyBalance[users[j]] - _before.userLqtyBalance[users[j]]; + // lusdClaimedAccumulator += _after.userLqtyBalance[users[j]] - _before.userLqtyBalance[users[j]]; + // } + // } + + // (uint128 boldAmount, uint128 bribeTokenAmount) = IBribeInitiative(initiative).bribeByEpoch(checkEpoch); + + // // shift 128 bit to the right to get the most significant bits of the accumulator (256 - 128 = 128) + // uint128 lqtyClaimedAccumulator128 = uint128(lqtyClaimedAccumulator >> 128); + // uint128 lusdClaimedAccumulator128 = uint128(lusdClaimedAccumulator >> 128); + + // // find delta between bribe and claimed amount (how much should be remaining in contract) + // uint128 lusdDelta = boldAmount - lusdClaimedAccumulator128; + // uint128 lqtyDelta = bribeTokenAmount - lqtyClaimedAccumulator128; + + // uint128 initiativeLusdBalance = uint128(lusd.balanceOf(initiative) >> 128); + // uint128 initiativeLqtyBalance = uint128(lqty.balanceOf(initiative) >> 128); + + // lte( + // lusdDelta - initiativeLusdBalance, + // 1e8, + // "BI-05: Bold token dust amount remaining after claiming should be less than 100 million wei" + // ); + // lte( + // lqtyDelta - initiativeLqtyBalance, + // 1e8, + // "BI-05: Bribe token dust amount remaining after claiming should be less than 100 million wei" + // ); + // } + // } function property_BI07() public { // sum user allocations for an epoch diff --git a/test/recon/properties/OptimizationProperties.sol b/test/recon/properties/OptimizationProperties.sol index fe87707f..0939e646 100644 --- a/test/recon/properties/OptimizationProperties.sol +++ b/test/recon/properties/OptimizationProperties.sol @@ -63,6 +63,9 @@ abstract contract OptimizationProperties is GovernanceProperties { return max; } + + // NOTE: This property is not particularly good as you can just do a donation and not vote + // This douesn't really highlight a loss function optimize_max_claim_underpay() public returns (int256) { uint256 claimableSum; for (uint256 i; i < deployedInitiatives.length; i++) { @@ -83,48 +86,6 @@ abstract contract OptimizationProperties is GovernanceProperties { return max; } - function optimize_max_claim_underpay_assertion() public returns (int256) { - uint256 claimableSum; - for (uint256 i; i < deployedInitiatives.length; i++) { - // NOTE: Non view so it accrues state - (Governance.InitiativeStatus status,, uint256 claimableAmount) = governance.getInitiativeState(deployedInitiatives[i]); - - claimableSum += claimableAmount; - } - - // Grab accrued - uint256 boldAccrued = governance.boldAccrued(); - - int256 delta; - if(boldAccrued > claimableSum) { - delta = int256(boldAccrued) - int256(claimableSum); - } - - t(delta < 1e20, "Delta is too big, over 100 LQTY 1e20"); - - return delta; - } - function optimize_max_claim_underpay_assertion_mini() public returns (int256) { - uint256 claimableSum; - for (uint256 i; i < deployedInitiatives.length; i++) { - // NOTE: Non view so it accrues state - (Governance.InitiativeStatus status,, uint256 claimableAmount) = governance.getInitiativeState(deployedInitiatives[i]); - - claimableSum += claimableAmount; - } - - // Grab accrued - uint256 boldAccrued = governance.boldAccrued(); - - int256 delta; - if(boldAccrued > claimableSum) { - delta = int256(boldAccrued) - int256(claimableSum); - } - - t(delta < 1e10, "Delta is too big, over 100 LQTY 1e10"); - - return delta; - } function property_sum_of_initatives_matches_total_votes_insolvency_assertion() public { @@ -143,42 +104,7 @@ abstract contract OptimizationProperties is GovernanceProperties { console.log("govPower", govPower); console.log("delta", delta); - t(delta < 3e25, "Delta is too big"); // Max found via optimization - } - - function property_sum_of_initatives_matches_total_votes_insolvency_assertion_mid() public { - - uint256 delta = 0; - - (, , uint256 votedPowerSum, uint256 govPower) = _getInitiativeStateAndGlobalState(); - - - if(votedPowerSum > govPower) { - delta = votedPowerSum - govPower; - - console.log("votedPowerSum * 1e18 / govPower", votedPowerSum * 1e18 / govPower); - } - - console.log("votedPowerSum", votedPowerSum); - console.log("govPower", govPower); - console.log("delta", delta); - - - t(delta < 1e18, "Delta is too big"); - } - - function property_sum_of_initatives_matches_total_votes_insolvency_assertion_small() public { - - uint256 delta = 0; - - (, , uint256 votedPowerSum, uint256 govPower) = _getInitiativeStateAndGlobalState(); - - - if(votedPowerSum > govPower) { - delta = votedPowerSum - govPower; - } - - t(delta < 1e10, "Delta is too big"); + t(delta < 4e25, "Delta is too big"); // 3e25 was found via optimization, no value past that was found } @@ -207,7 +133,7 @@ abstract contract OptimizationProperties is GovernanceProperties { return max; } - function optimize_property_sum_of_initatives_matches_total_votes_insolvency() public returns (int256) { + function optimize_property_sum_of_initatives_matches_total_votes_insolvency() public returns (bool) { int256 max = 0; @@ -218,7 +144,7 @@ abstract contract OptimizationProperties is GovernanceProperties { max = int256(votedPowerSum) - int256(govPower); } - return max; + return max < 3e25; } function optimize_property_sum_of_initatives_matches_total_votes_underpaying() public returns (int256) { From 953a3ef76231b2faa9679802c53a677d291a2ed9 Mon Sep 17 00:00:00 2001 From: Entreprenerd Date: Mon, 4 Nov 2024 20:38:23 +0100 Subject: [PATCH 2/2] chore: remove unused tests --- test/recon/CryticToFoundry.sol | 41 ---------------------------------- 1 file changed, 41 deletions(-) diff --git a/test/recon/CryticToFoundry.sol b/test/recon/CryticToFoundry.sol index f1b0db5c..e55372ef 100644 --- a/test/recon/CryticToFoundry.sol +++ b/test/recon/CryticToFoundry.sol @@ -16,47 +16,6 @@ contract CryticToFoundry is Test, TargetFunctions, FoundryAsserts { } - // forge test --match-test test_optimize_max_claim_underpay_assertion_0 -vv - function test_optimize_max_claim_underpay_assertion_0() public { - - helper_accrueBold(1001125329789697909641); - - check_warmup_unregisterable_consistency(0); - - optimize_max_claim_underpay_assertion(); - - } - -// forge test --match-test test_property_sum_of_initatives_matches_total_votes_insolvency_assertion_mid_0 -vv - function test_property_sum_of_initatives_matches_total_votes_insolvency_assertion_mid_0() public { - - governance_depositLQTY_2(1439490298322854874); - - vm.roll(block.number + 1); - vm.warp(block.timestamp + 313704); - governance_depositLQTY(1); - - vm.warp(block.timestamp + 413441); - - vm.roll(block.number + 1); - - governance_allocateLQTY_clamped_single_initiative(0,1,0); - - vm.warp(block.timestamp + 173473); - - vm.roll(block.number + 1); - - helper_deployInitiative(); - - governance_registerInitiative(1); - - vm.roll(block.number + 1); - vm.warp(block.timestamp + 315415); - governance_allocateLQTY_clamped_single_initiative_2nd_user(1,1293868687551209131,0); - - property_sum_of_initatives_matches_total_votes_insolvency_assertion_mid(); - - } // forge test --match-test test_optimize_property_sum_of_initatives_matches_total_votes_insolvency_0 -vv function test_optimize_property_sum_of_initatives_matches_total_votes_insolvency_0() public {