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 broken properties #70

Merged
merged 2 commits into from
Nov 13, 2024
+59 −172
Merged

Fix broken properties #70

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ebba848
feat: remove incorrectly broken properties
GalloDaSballo Nov 4, 2024
953a3ef
chore: remove unused tests
GalloDaSballo Nov 4, 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
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
41 changes: 0 additions & 41 deletions test/recon/CryticToFoundry.sol
View file
Original file line number Diff line number Diff line change
@@ -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 {
96 changes: 48 additions & 48 deletions test/recon/properties/BribeInitiativeProperties.sol
View file
Original file line number Diff line number Diff line change
@@ -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
86 changes: 6 additions & 80 deletions test/recon/properties/OptimizationProperties.sol
View file
Original file line number Diff line number Diff line change
@@ -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) {