Skip to content

Commit

Permalink
feat: remove incorrectly broken properties
Browse files Browse the repository at this point in the history
  • Loading branch information
@GalloDaSballo
GalloDaSballo committed Nov 4, 2024
1 parent de65c89 commit ebba848
Show file tree
Hide file tree
Showing 3 changed files with 59 additions and 131 deletions.
8 changes: 5 additions & 3 deletions echidna.yaml
View file
Original file line number Diff line number Diff line change
@@ -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"]
cryticArgs: ["--foundry-compile-all"]

shrinkLimit: 100000
96 changes: 48 additions & 48 deletions test/recon/properties/BribeInitiativeProperties.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
86 changes: 6 additions & 80 deletions test/recon/properties/OptimizationProperties.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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++) {
Expand All @@ -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 {

Expand All @@ -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
}


Expand Down Expand Up @@ -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;

Expand All @@ -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) {
Expand Down

0 comments on commit ebba848

Please sign in to comment.