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) {