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

Jump to bottom

Invariant Testing CI / CD #75

Merged
merged 2 commits into from
Nov 19, 2024
Merged

Invariant Testing CI / CD #75

merged 2 commits into from
Nov 19, 2024

Conversation

GalloDaSballo
Copy link
Collaborator

Pushes to main will trigger a comment with a report from Recon

@recon-getrecon-xyz Recon (getrecon.xyz)
Copy link

Recon Campaign Started

@recon-getrecon-xyz Recon (getrecon.xyz)
Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 5h2m4s
  • Coverage: 45615
  • Failed: 2
  • Passed: 85

Results

Property Status
property_initiative_ts_matches_user_when_non_zero() ✅
check_unregisterable_consistecy(uint8) ❌
property_resetting_never_reverts() ✅
check_claimable_solvency() ✅
excludeSenders() ✅
property_shouldNeverRevertgetInitiativeState(uint8) ✅
check_realized_claiming_solvency() ✅
targetInterfaces() ✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8) ✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint96,uint96) ✅
property_BI02() ✅
property_computingGlobalPowerNeverReverts() ✅
governance_resetAllocations() ✅
property_global_ts_is_always_greater_than_start() ✅
governance_depositLQTYViaPermit(uint88) ✅
targetSenders() ✅
targetContracts() ✅
property_shouldGetTotalVotesAndState() ✅
property_BI10() ✅
property_shouldNeverRevertcalculateVotingThreshold() ✅
depositTsIsRational(uint88) ✅
helper_accrueBold(uint88) ✅
property_sum_of_user_voting_weights_strict() ✅
property_sum_of_user_initiative_allocations() ✅
depositMustFailOnNonZeroAlloc(uint88) ✅
property_summingInitiativesPowerNeverReverts() ✅
withdrwaMustFailOnNonZeroAcc(uint88) ✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint96,uint96) ✅
helper_deployInitiative() ✅
property_sum_of_lqty_global_user_matches() ✅
property_sum_of_votes_in_bribes_match() ✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint88) ✅
targetArtifactSelectors() ✅
property_sum_of_lqty_initiative_user_matches() ✅
initiative_depositBribe(uint128,uint128,uint16,uint8) ✅
property_GV01() ✅
property_viewCalculateVotingThreshold() ✅
governance_registerInitiative(uint8) ✅
governance_withdrawLQTY(uint88) ✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8) ✅
property_BI07() ✅
governance_resetAllocations_user_2() ✅
targetArtifacts() ✅
governance_allocateLQTY(int88[],int88[]) ✅
property_sum_of_initatives_matches_total_votes_bounded() ✅
property_BI04() ✅
targetSelectors() ✅
governance_depositLQTY(uint88) ✅
check_warmup_unregisterable_consistency(uint8) ✅
property_ensure_user_alloc_cannot_dos() ✅
property_BI08() ✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion() ✅
property_shouldNeverRevertgetLatestVotingThreshold() ✅
governance_claimForInitiativeDoesntRevert(uint8) ✅
property_BI03() ✅
excludeArtifacts() ✅
check_claim_soundness() ✅
property_shouldNeverRevertsecondsWithinEpoch() ✅
failed() ✅
property_sum_of_user_voting_weights_bounded() ✅
property_BI01() ✅
property_shouldNeverRevertepochStart(uint8) ✅
property_BI09() ✅
property_shouldNeverRevertSnapshotAndState(uint8) ✅
property_shouldNeverRevertlqtyToVotes() ✅
governance_snapshotVotesForInitiative(address) ✅
governance_deployUserProxy() ✅
governance_depositLQTY_2(uint88) ✅
property_allocations_are_never_dangerously_high() ✅
property_alloc_deposit_reset_is_idempotent(uint8,uint96,uint96,uint88) ✅
property_shouldNeverRevertgetTotalVotesAndState() ✅
clamped_claimBribes(uint8) ✅
property_shouldNeverRevertepoch() ✅
governance_claimForInitiative(uint8) ✅
property_GV_09() ✅
excludeContracts() ✅
governance_claimForInitiativeFuzzTest(uint8) ✅
property_user_ts_is_always_greater_than_start() ✅
property_viewTotalVotesAndStateEquivalency() ✅
check_skip_consistecy(uint8) ✅
governance_unregisterInitiative(uint8) ✅
governance_claimFromStakingV1(uint8) ✅
IS_TEST() ✅
initiative_claimBribes(uint16,uint16,uint16,uint8) ✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address) ✅
property_sum_of_initatives_matches_total_votes_strict() ❌
AssertionFailed(..) ✅

Broken Properties

Broken property:

check_unregisterable_consistecy

Sequence

// forge test --match-test test_check_unregisterable_consistecy_ -vv 
 function test_check_unregisterable_consistecy_() public {

     vm.roll(block.number + 46536);
     vm.warp(block.timestamp + 577015);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 1362);
     vm.warp(block.timestamp + 332369);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(262322195659734805072413361);

     vm.roll(block.number + 33497);
     vm.warp(block.timestamp + 65536);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 43905);
     vm.warp(block.timestamp + 58);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 55752);
     vm.warp(block.timestamp + 178398);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertSnapshotAndState(236);

     vm.roll(block.number + 16814);
     vm.warp(block.timestamp + 3600);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative(37,0,50113);

     vm.roll(block.number + 47864);
     vm.warp(block.timestamp + 59984);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_resetAllocations();

     vm.roll(block.number + 47902);
     vm.warp(block.timestamp + 112444);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI03();

     vm.roll(block.number + 15392);
     vm.warp(block.timestamp + 322160);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_unregisterable_consistecy(31);

 }

Broken property:

property_sum_of_initatives_matches_total_votes_strict

Sequence

// forge test --match-test test_property_sum_of_initatives_matches_total_votes_strict_ -vv 
 function test_property_sum_of_initatives_matches_total_votes_strict_() public {

     vm.roll(block.number + 46536);
     vm.warp(block.timestamp + 577015);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 1362);
     vm.warp(block.timestamp + 332369);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(262322195659734805072413361);

     vm.roll(block.number + 33497);
     vm.warp(block.timestamp + 65536);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 43905);
     vm.warp(block.timestamp + 58);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 55752);
     vm.warp(block.timestamp + 178398);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertSnapshotAndState(236);

     vm.roll(block.number + 3751);
     vm.warp(block.timestamp + 149578);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI09();

     vm.roll(block.number + 50537);
     vm.warp(block.timestamp + 322370);
     vm.prank(0x0000000000000000000000000000000000020000);
    depositMustFailOnNonZeroAlloc(122);

     vm.roll(block.number + 55724);
     vm.warp(block.timestamp + 57804);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(130,93,0);

     vm.roll(block.number + 45819);
     vm.warp(block.timestamp + 322357);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeState(100);

     vm.roll(block.number + 21439);
     vm.warp(block.timestamp + 365091);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeFuzzTest(103);

     vm.roll(block.number + 2821);
     vm.warp(block.timestamp + 304335);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI09();

     vm.roll(block.number + 53011);
     vm.warp(block.timestamp + 407567);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_GV_09();

     vm.roll(block.number + 4847);
     vm.warp(block.timestamp + 471291);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 15505);
     vm.warp(block.timestamp + 262143);
     vm.prank(0x0000000000000000000000000000000000020000);
    initiative_depositBribe(264474546884491357117362731710371217215,254135392087517085278822988830747111655,215,17);

     vm.roll(block.number + 13);
     vm.warp(block.timestamp + 513169);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_registerInitiative(11);

     vm.roll(block.number + 60460);
     vm.warp(block.timestamp + 61359);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI09();

     vm.roll(block.number + 27250);
     vm.warp(block.timestamp + 400);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_claimable_solvency();

     vm.roll(block.number + 38703);
     vm.warp(block.timestamp + 73444);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_GV_09();

     vm.roll(block.number + 3162);
     vm.warp(block.timestamp + 523);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(70,49906617260552605762047230770,1000000);

     vm.roll(block.number + 27174);
     vm.warp(block.timestamp + 407567);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimFromStakingV1(252);

     vm.roll(block.number + 2821);
     vm.warp(block.timestamp + 472846);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_realized_claiming_solvency();

     vm.roll(block.number + 4094);
     vm.warp(block.timestamp + 357863);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI05();

     vm.roll(block.number + 48072);
     vm.warp(block.timestamp + 282472);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative(32,34961718036134411610099238296,133);

     vm.roll(block.number + 5016);
     vm.warp(block.timestamp + 604762);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 32958);
     vm.warp(block.timestamp + 322143);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_skip_consistecy(190);

     vm.roll(block.number + 51878);
     vm.warp(block.timestamp + 124202);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(194,63,44042324661291034963457523227);

     vm.roll(block.number + 10978);
     vm.warp(block.timestamp + 344203);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_lqty_global_user_matches();

     vm.roll(block.number + 50417);
     vm.warp(block.timestamp + 440284);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_GV_09();

     vm.roll(block.number + 4901);
     vm.warp(block.timestamp + 326329);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldGetTotalVotesAndState();

     vm.roll(block.number + 15504);
     vm.warp(block.timestamp + 577014);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetLatestVotingThreshold();

     vm.roll(block.number + 4841);
     vm.warp(block.timestamp + 482394);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI09();

     vm.roll(block.number + 57313);
     vm.warp(block.timestamp + 379005);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 48887);
     vm.warp(block.timestamp + 322198);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiative(92);

     vm.roll(block.number + 6295);
     vm.warp(block.timestamp + 57803);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI07();

     vm.roll(block.number + 13868);
     vm.warp(block.timestamp + 322069);
     vm.prank(0x0000000000000000000000000000000000030000);
    clamped_claimBribes(33);

     vm.roll(block.number + 15513);
     vm.warp(block.timestamp + 80212);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_alloc_deposit_reset_is_idempotent(200,1999999999999999999,9831763698359078767883274571,99380824833012099680917693);

     vm.roll(block.number + 3662);
     vm.warp(block.timestamp + 496936);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiative(0);

     vm.roll(block.number + 25985);
     vm.warp(block.timestamp + 153540);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_global_ts_is_always_greater_than_start();

     vm.roll(block.number + 65);
     vm.warp(block.timestamp + 94683);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 28997);
     vm.warp(block.timestamp + 534786);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(10000000000000000);

     vm.roll(block.number + 5216);
     vm.warp(block.timestamp + 128966);
     vm.prank(0x0000000000000000000000000000000000020000);
    initiative_depositBribe(94743225334330175067115104350172538975,339738377640345403697157401104375502017,63360,37);

     vm.roll(block.number + 3599);
     vm.warp(block.timestamp + 137558);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 88);
     vm.warp(block.timestamp + 586022);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeState(102);

     vm.roll(block.number + 24966);
     vm.warp(block.timestamp + 33);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 15504);
     vm.warp(block.timestamp + 385871);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI02();

     vm.roll(block.number + 1862);
     vm.warp(block.timestamp + 338920);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiative(170);

     vm.roll(block.number + 4987);
     vm.warp(block.timestamp + 102110);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 60268);
     vm.warp(block.timestamp + 322216);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_unregisterInitiative(182);

     vm.roll(block.number + 45693);
     vm.warp(block.timestamp + 352709);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 8907);
     vm.warp(block.timestamp + 417307);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 39518);
     vm.warp(block.timestamp + 486890);
     vm.prank(0x0000000000000000000000000000000000030000);
    helper_deployInitiative();

     vm.roll(block.number + 125);
     vm.warp(block.timestamp + 288562);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_alloc_deposit_reset_is_idempotent(86,34630418746493929544746664202,65565596280218207006265461316,499999999999999999999);

     vm.roll(block.number + 6666);
     vm.warp(block.timestamp + 472846);
     vm.prank(0x0000000000000000000000000000000000020000);
    clamped_claimBribes(134);

     vm.roll(block.number + 40000);
     vm.warp(block.timestamp + 359581);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 60450);
     vm.warp(block.timestamp + 488787);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(0);

     vm.roll(block.number + 2363);
     vm.warp(block.timestamp + 92959);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_user_initiative_allocations();

     vm.roll(block.number + 8192);
     vm.warp(block.timestamp + 193410);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI09();

     vm.roll(block.number + 3501);
     vm.warp(block.timestamp + 320326);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_registerInitiative(53);

     vm.roll(block.number + 98);
     vm.warp(block.timestamp + 481079);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_user_voting_weights_bounded();

     vm.roll(block.number + 16986);
     vm.warp(block.timestamp + 130097);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_registerInitiative(49);

     vm.roll(block.number + 55394);
     vm.warp(block.timestamp + 187040);
     vm.prank(0x0000000000000000000000000000000000020000);
    depositTsIsRational(96505857);

     vm.roll(block.number + 39520);
     vm.warp(block.timestamp + 566552);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiative(44);

     vm.roll(block.number + 39519);
     vm.warp(block.timestamp + 161);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_deployInitiative();

     vm.roll(block.number + 129);
     vm.warp(block.timestamp + 356013);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_initiative_ts_matches_user_when_non_zero();

     vm.roll(block.number + 208);
     vm.warp(block.timestamp + 143976);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_ts_is_always_greater_than_start();

     vm.roll(block.number + 184);
     vm.warp(block.timestamp + 264015);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI02();

     vm.roll(block.number + 38156);
     vm.warp(block.timestamp + 385871);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(220,44427865740410136309018159090,0);

     vm.roll(block.number + 13547);
     vm.warp(block.timestamp + 214);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(0,46019483024675071069875065407,1524785993);

     vm.roll(block.number + 11413);
     vm.warp(block.timestamp + 145412);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI04();

     vm.roll(block.number + 18571);
     vm.warp(block.timestamp + 522178);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiativeDoesntRevert(64);

     vm.roll(block.number + 4148);
     vm.warp(block.timestamp + 159);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_alloc_deposit_reset_is_idempotent(131,15815929122548744098354409702,209,933);

     vm.roll(block.number + 49388);
     vm.warp(block.timestamp + 385873);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_alloc_deposit_reset_is_idempotent(125,39999,12568864,293722316941937191872210671);

     vm.roll(block.number + 45627);
     vm.warp(block.timestamp + 262802);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_initiative_ts_matches_user_when_non_zero();

     vm.roll(block.number + 13869);
     vm.warp(block.timestamp + 38);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_votes_in_bribes_match();

     vm.roll(block.number + 8865);
     vm.warp(block.timestamp + 166300);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTYViaPermit(80973242180591189004751278);

     vm.roll(block.number + 27161);
     vm.warp(block.timestamp + 67);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_skip_consistecy(200);

     vm.roll(block.number + 15609);
     vm.warp(block.timestamp + 246182);
     vm.prank(0x0000000000000000000000000000000000010000);
    optimize_max_claim_underpay_assertion();

     vm.roll(block.number + 60474);
     vm.warp(block.timestamp + 242164);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI04();

     vm.roll(block.number + 5140);
     vm.warp(block.timestamp + 186939);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion_small();

     vm.roll(block.number + 60472);
     vm.warp(block.timestamp + 332175);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_initatives_matches_total_votes_strict();

 }

1 similar comment
@recon-getrecon-xyz Recon (getrecon.xyz)
Copy link

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

  • Fuzzer: ECHIDNA
  • Duration: 5h2m4s
  • Coverage: 45615
  • Failed: 2
  • Passed: 85

Results

Property Status
property_initiative_ts_matches_user_when_non_zero() ✅
check_unregisterable_consistecy(uint8) ❌
property_resetting_never_reverts() ✅
check_claimable_solvency() ✅
excludeSenders() ✅
property_shouldNeverRevertgetInitiativeState(uint8) ✅
check_realized_claiming_solvency() ✅
targetInterfaces() ✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8) ✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint96,uint96) ✅
property_BI02() ✅
property_computingGlobalPowerNeverReverts() ✅
governance_resetAllocations() ✅
property_global_ts_is_always_greater_than_start() ✅
governance_depositLQTYViaPermit(uint88) ✅
targetSenders() ✅
targetContracts() ✅
property_shouldGetTotalVotesAndState() ✅
property_BI10() ✅
property_shouldNeverRevertcalculateVotingThreshold() ✅
depositTsIsRational(uint88) ✅
helper_accrueBold(uint88) ✅
property_sum_of_user_voting_weights_strict() ✅
property_sum_of_user_initiative_allocations() ✅
depositMustFailOnNonZeroAlloc(uint88) ✅
property_summingInitiativesPowerNeverReverts() ✅
withdrwaMustFailOnNonZeroAcc(uint88) ✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint96,uint96) ✅
helper_deployInitiative() ✅
property_sum_of_lqty_global_user_matches() ✅
property_sum_of_votes_in_bribes_match() ✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint88) ✅
targetArtifactSelectors() ✅
property_sum_of_lqty_initiative_user_matches() ✅
initiative_depositBribe(uint128,uint128,uint16,uint8) ✅
property_GV01() ✅
property_viewCalculateVotingThreshold() ✅
governance_registerInitiative(uint8) ✅
governance_withdrawLQTY(uint88) ✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8) ✅
property_BI07() ✅
governance_resetAllocations_user_2() ✅
targetArtifacts() ✅
governance_allocateLQTY(int88[],int88[]) ✅
property_sum_of_initatives_matches_total_votes_bounded() ✅
property_BI04() ✅
targetSelectors() ✅
governance_depositLQTY(uint88) ✅
check_warmup_unregisterable_consistency(uint8) ✅
property_ensure_user_alloc_cannot_dos() ✅
property_BI08() ✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion() ✅
property_shouldNeverRevertgetLatestVotingThreshold() ✅
governance_claimForInitiativeDoesntRevert(uint8) ✅
property_BI03() ✅
excludeArtifacts() ✅
check_claim_soundness() ✅
property_shouldNeverRevertsecondsWithinEpoch() ✅
failed() ✅
property_sum_of_user_voting_weights_bounded() ✅
property_BI01() ✅
property_shouldNeverRevertepochStart(uint8) ✅
property_BI09() ✅
property_shouldNeverRevertSnapshotAndState(uint8) ✅
property_shouldNeverRevertlqtyToVotes() ✅
governance_snapshotVotesForInitiative(address) ✅
governance_deployUserProxy() ✅
governance_depositLQTY_2(uint88) ✅
property_allocations_are_never_dangerously_high() ✅
property_alloc_deposit_reset_is_idempotent(uint8,uint96,uint96,uint88) ✅
property_shouldNeverRevertgetTotalVotesAndState() ✅
clamped_claimBribes(uint8) ✅
property_shouldNeverRevertepoch() ✅
governance_claimForInitiative(uint8) ✅
property_GV_09() ✅
excludeContracts() ✅
governance_claimForInitiativeFuzzTest(uint8) ✅
property_user_ts_is_always_greater_than_start() ✅
property_viewTotalVotesAndStateEquivalency() ✅
check_skip_consistecy(uint8) ✅
governance_unregisterInitiative(uint8) ✅
governance_claimFromStakingV1(uint8) ✅
IS_TEST() ✅
initiative_claimBribes(uint16,uint16,uint16,uint8) ✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address) ✅
property_sum_of_initatives_matches_total_votes_strict() ❌
AssertionFailed(..) ✅

Broken Properties

Broken property:

check_unregisterable_consistecy

Sequence

// forge test --match-test test_check_unregisterable_consistecy_ -vv 
 function test_check_unregisterable_consistecy_() public {

     vm.roll(block.number + 46536);
     vm.warp(block.timestamp + 577015);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 1362);
     vm.warp(block.timestamp + 332369);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(262322195659734805072413361);

     vm.roll(block.number + 33497);
     vm.warp(block.timestamp + 65536);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 43905);
     vm.warp(block.timestamp + 58);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 55752);
     vm.warp(block.timestamp + 178398);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertSnapshotAndState(236);

     vm.roll(block.number + 16814);
     vm.warp(block.timestamp + 3600);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative(37,0,50113);

     vm.roll(block.number + 47864);
     vm.warp(block.timestamp + 59984);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_resetAllocations();

     vm.roll(block.number + 47902);
     vm.warp(block.timestamp + 112444);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI03();

     vm.roll(block.number + 15392);
     vm.warp(block.timestamp + 322160);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_unregisterable_consistecy(31);

 }

Broken property:

property_sum_of_initatives_matches_total_votes_strict

Sequence

// forge test --match-test test_property_sum_of_initatives_matches_total_votes_strict_ -vv 
 function test_property_sum_of_initatives_matches_total_votes_strict_() public {

     vm.roll(block.number + 46536);
     vm.warp(block.timestamp + 577015);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 1362);
     vm.warp(block.timestamp + 332369);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(262322195659734805072413361);

     vm.roll(block.number + 33497);
     vm.warp(block.timestamp + 65536);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 43905);
     vm.warp(block.timestamp + 58);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 55752);
     vm.warp(block.timestamp + 178398);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertSnapshotAndState(236);

     vm.roll(block.number + 3751);
     vm.warp(block.timestamp + 149578);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI09();

     vm.roll(block.number + 50537);
     vm.warp(block.timestamp + 322370);
     vm.prank(0x0000000000000000000000000000000000020000);
    depositMustFailOnNonZeroAlloc(122);

     vm.roll(block.number + 55724);
     vm.warp(block.timestamp + 57804);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(130,93,0);

     vm.roll(block.number + 45819);
     vm.warp(block.timestamp + 322357);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeState(100);

     vm.roll(block.number + 21439);
     vm.warp(block.timestamp + 365091);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeFuzzTest(103);

     vm.roll(block.number + 2821);
     vm.warp(block.timestamp + 304335);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI09();

     vm.roll(block.number + 53011);
     vm.warp(block.timestamp + 407567);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_GV_09();

     vm.roll(block.number + 4847);
     vm.warp(block.timestamp + 471291);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 15505);
     vm.warp(block.timestamp + 262143);
     vm.prank(0x0000000000000000000000000000000000020000);
    initiative_depositBribe(264474546884491357117362731710371217215,254135392087517085278822988830747111655,215,17);

     vm.roll(block.number + 13);
     vm.warp(block.timestamp + 513169);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_registerInitiative(11);

     vm.roll(block.number + 60460);
     vm.warp(block.timestamp + 61359);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI09();

     vm.roll(block.number + 27250);
     vm.warp(block.timestamp + 400);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_claimable_solvency();

     vm.roll(block.number + 38703);
     vm.warp(block.timestamp + 73444);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_GV_09();

     vm.roll(block.number + 3162);
     vm.warp(block.timestamp + 523);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(70,49906617260552605762047230770,1000000);

     vm.roll(block.number + 27174);
     vm.warp(block.timestamp + 407567);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimFromStakingV1(252);

     vm.roll(block.number + 2821);
     vm.warp(block.timestamp + 472846);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_realized_claiming_solvency();

     vm.roll(block.number + 4094);
     vm.warp(block.timestamp + 357863);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI05();

     vm.roll(block.number + 48072);
     vm.warp(block.timestamp + 282472);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative(32,34961718036134411610099238296,133);

     vm.roll(block.number + 5016);
     vm.warp(block.timestamp + 604762);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 32958);
     vm.warp(block.timestamp + 322143);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_skip_consistecy(190);

     vm.roll(block.number + 51878);
     vm.warp(block.timestamp + 124202);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(194,63,44042324661291034963457523227);

     vm.roll(block.number + 10978);
     vm.warp(block.timestamp + 344203);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_lqty_global_user_matches();

     vm.roll(block.number + 50417);
     vm.warp(block.timestamp + 440284);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_GV_09();

     vm.roll(block.number + 4901);
     vm.warp(block.timestamp + 326329);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldGetTotalVotesAndState();

     vm.roll(block.number + 15504);
     vm.warp(block.timestamp + 577014);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetLatestVotingThreshold();

     vm.roll(block.number + 4841);
     vm.warp(block.timestamp + 482394);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI09();

     vm.roll(block.number + 57313);
     vm.warp(block.timestamp + 379005);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 48887);
     vm.warp(block.timestamp + 322198);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiative(92);

     vm.roll(block.number + 6295);
     vm.warp(block.timestamp + 57803);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI07();

     vm.roll(block.number + 13868);
     vm.warp(block.timestamp + 322069);
     vm.prank(0x0000000000000000000000000000000000030000);
    clamped_claimBribes(33);

     vm.roll(block.number + 15513);
     vm.warp(block.timestamp + 80212);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_alloc_deposit_reset_is_idempotent(200,1999999999999999999,9831763698359078767883274571,99380824833012099680917693);

     vm.roll(block.number + 3662);
     vm.warp(block.timestamp + 496936);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiative(0);

     vm.roll(block.number + 25985);
     vm.warp(block.timestamp + 153540);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_global_ts_is_always_greater_than_start();

     vm.roll(block.number + 65);
     vm.warp(block.timestamp + 94683);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 28997);
     vm.warp(block.timestamp + 534786);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(10000000000000000);

     vm.roll(block.number + 5216);
     vm.warp(block.timestamp + 128966);
     vm.prank(0x0000000000000000000000000000000000020000);
    initiative_depositBribe(94743225334330175067115104350172538975,339738377640345403697157401104375502017,63360,37);

     vm.roll(block.number + 3599);
     vm.warp(block.timestamp + 137558);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 88);
     vm.warp(block.timestamp + 586022);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeState(102);

     vm.roll(block.number + 24966);
     vm.warp(block.timestamp + 33);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 15504);
     vm.warp(block.timestamp + 385871);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI02();

     vm.roll(block.number + 1862);
     vm.warp(block.timestamp + 338920);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiative(170);

     vm.roll(block.number + 4987);
     vm.warp(block.timestamp + 102110);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 60268);
     vm.warp(block.timestamp + 322216);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_unregisterInitiative(182);

     vm.roll(block.number + 45693);
     vm.warp(block.timestamp + 352709);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 8907);
     vm.warp(block.timestamp + 417307);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 39518);
     vm.warp(block.timestamp + 486890);
     vm.prank(0x0000000000000000000000000000000000030000);
    helper_deployInitiative();

     vm.roll(block.number + 125);
     vm.warp(block.timestamp + 288562);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_alloc_deposit_reset_is_idempotent(86,34630418746493929544746664202,65565596280218207006265461316,499999999999999999999);

     vm.roll(block.number + 6666);
     vm.warp(block.timestamp + 472846);
     vm.prank(0x0000000000000000000000000000000000020000);
    clamped_claimBribes(134);

     vm.roll(block.number + 40000);
     vm.warp(block.timestamp + 359581);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 60450);
     vm.warp(block.timestamp + 488787);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(0);

     vm.roll(block.number + 2363);
     vm.warp(block.timestamp + 92959);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_user_initiative_allocations();

     vm.roll(block.number + 8192);
     vm.warp(block.timestamp + 193410);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI09();

     vm.roll(block.number + 3501);
     vm.warp(block.timestamp + 320326);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_registerInitiative(53);

     vm.roll(block.number + 98);
     vm.warp(block.timestamp + 481079);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_user_voting_weights_bounded();

     vm.roll(block.number + 16986);
     vm.warp(block.timestamp + 130097);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_registerInitiative(49);

     vm.roll(block.number + 55394);
     vm.warp(block.timestamp + 187040);
     vm.prank(0x0000000000000000000000000000000000020000);
    depositTsIsRational(96505857);

     vm.roll(block.number + 39520);
     vm.warp(block.timestamp + 566552);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiative(44);

     vm.roll(block.number + 39519);
     vm.warp(block.timestamp + 161);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_deployInitiative();

     vm.roll(block.number + 129);
     vm.warp(block.timestamp + 356013);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_initiative_ts_matches_user_when_non_zero();

     vm.roll(block.number + 208);
     vm.warp(block.timestamp + 143976);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_ts_is_always_greater_than_start();

     vm.roll(block.number + 184);
     vm.warp(block.timestamp + 264015);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI02();

     vm.roll(block.number + 38156);
     vm.warp(block.timestamp + 385871);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(220,44427865740410136309018159090,0);

     vm.roll(block.number + 13547);
     vm.warp(block.timestamp + 214);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(0,46019483024675071069875065407,1524785993);

     vm.roll(block.number + 11413);
     vm.warp(block.timestamp + 145412);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI04();

     vm.roll(block.number + 18571);
     vm.warp(block.timestamp + 522178);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiativeDoesntRevert(64);

     vm.roll(block.number + 4148);
     vm.warp(block.timestamp + 159);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_alloc_deposit_reset_is_idempotent(131,15815929122548744098354409702,209,933);

     vm.roll(block.number + 49388);
     vm.warp(block.timestamp + 385873);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_alloc_deposit_reset_is_idempotent(125,39999,12568864,293722316941937191872210671);

     vm.roll(block.number + 45627);
     vm.warp(block.timestamp + 262802);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_initiative_ts_matches_user_when_non_zero();

     vm.roll(block.number + 13869);
     vm.warp(block.timestamp + 38);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_votes_in_bribes_match();

     vm.roll(block.number + 8865);
     vm.warp(block.timestamp + 166300);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTYViaPermit(80973242180591189004751278);

     vm.roll(block.number + 27161);
     vm.warp(block.timestamp + 67);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_skip_consistecy(200);

     vm.roll(block.number + 15609);
     vm.warp(block.timestamp + 246182);
     vm.prank(0x0000000000000000000000000000000000010000);
    optimize_max_claim_underpay_assertion();

     vm.roll(block.number + 60474);
     vm.warp(block.timestamp + 242164);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI04();

     vm.roll(block.number + 5140);
     vm.warp(block.timestamp + 186939);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion_small();

     vm.roll(block.number + 60472);
     vm.warp(block.timestamp + 332175);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_initatives_matches_total_votes_strict();

 }

@danielattilasimon danielattilasimon merged commit 132e41f into temp-invariant Nov 19, 2024
4 of 6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@GalloDaSballo @danielattilasimon