INVARIANT TEST by GalloDaSballo · Pull Request #83 · liquity/V2-gov

GalloDaSballo · 2024-11-24T08:55:34Z

This is just a way for our tool to detected pushes to main and paste the result of the Invariant Testing Run

Fixes CS-V2Gov-020.

As value now encodes timestamp, it would never be zero, we need to decode and then check.

Both LUSD and LQTY are already safe.

…aking

Needed for `vm.expectPartialRevert()`

The fetched state doesn't change much depending on fuzz inputs, so having a different seed each time won't result in drastically increased RPC usage. That is, once we fix the tests, because the Foundry action only saves the RPC cache if the tests are passing. (Why though)?

Fixes IR-02.

It was taking 20 minutes for a single test run.

fix: Remove safeTransfer from UserProxy

fix: Remove ForwardBribe contract

If you pass any amount higher than your stake, and LQTYStaking will internally truncate it to the maximum withdrawable amount.

recon-getrecon-xyz · 2025-01-13T13:48:48Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 5h48m24s
Coverage: 43567
Failed: 8
Passed: 80

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	❌
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
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 {

    offsetIsRational(1);

    check_warmup_unregisterable_consistency(0);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    vm.warp(block.timestamp + 604836);

    vm.roll(block.number + 1);

    governance_resetAllocations();

    check_unregisterable_consistecy(0);

 }

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    check_warmup_unregisterable_consistency(0);

    governance_depositLQTY_2(2);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,0,1);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

    check_warmup_unregisterable_consistency(0);

    governance_depositLQTY_2(2);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

     vm.roll(block.number + 1088);
     vm.warp(block.timestamp + 542442);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI10();

     vm.roll(block.number + 60289);
     vm.warp(block.timestamp + 20539);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(4370000);

    vm.warp(block.timestamp + 865761);

    vm.roll(block.number + 112243);

     vm.roll(block.number + 42264);
     vm.warp(block.timestamp + 322284);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI01();

     vm.roll(block.number + 44068);
     vm.warp(block.timestamp + 179668);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(46,59758112741496683744258210651293268891459357260859445081445093212486547368910,32892085976703057493429442155481922956792867770294738853359532131363189390811);

     vm.roll(block.number + 53429);
     vm.warp(block.timestamp + 226854);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI02();

     vm.roll(block.number + 14623);
     vm.warp(block.timestamp + 2);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_snapshotVotesForInitiative(0x0000000000000000000000000000000000030000);

     vm.roll(block.number + 58181);
     vm.warp(block.timestamp + 586021);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_computingGlobalPowerNeverReverts();

     vm.roll(block.number + 4901);
     vm.warp(block.timestamp + 336898);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_realized_claiming_solvency();

    vm.warp(block.timestamp + 478748);

    vm.roll(block.number + 51878);

     vm.roll(block.number + 44068);
     vm.warp(block.timestamp + 168836);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 25203);
     vm.warp(block.timestamp + 322176);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_viewCalculateVotingThreshold();

    vm.warp(block.timestamp + 784244);

    vm.roll(block.number + 78204);

     vm.roll(block.number + 11349);
     vm.warp(block.timestamp + 408775);
     vm.prank(0x0000000000000000000000000000000000010000);
    initiative_claimBribes(46940750882446099933503445504570747994449994777452419522159603995022003892459,115792089237316195423570985008687907853269984665640564019457584007913129639935,115792089237316195423570985008687907853269984665640564039457584007913129564896,68);

    vm.warp(block.timestamp + 405856);

    vm.roll(block.number + 40106);

     vm.roll(block.number + 33175);
     vm.warp(block.timestamp + 539433);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiativeFuzzTest(37);

     vm.roll(block.number + 24363);
     vm.warp(block.timestamp + 322343);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 25398);
     vm.warp(block.timestamp + 403427);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 52344);
     vm.warp(block.timestamp + 322338);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_realized_claiming_solvency();

     vm.roll(block.number + 46153);
     vm.warp(block.timestamp + 518401);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_skip_consistecy(119);

    vm.warp(block.timestamp + 322377);

    vm.roll(block.number + 89);

     vm.roll(block.number + 20129);
     vm.warp(block.timestamp + 577177);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion();

     vm.roll(block.number + 30391);
     vm.warp(block.timestamp + 541203);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000002fFffFffD);

     vm.roll(block.number + 24987);
     vm.warp(block.timestamp + 566553);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 4567);
     vm.warp(block.timestamp + 267436);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 8864);
     vm.warp(block.timestamp + 246073);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_warmup_unregisterable_consistency(173);

     vm.roll(block.number + 25540);
     vm.warp(block.timestamp + 23767);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_initiative_offset_matches_user_when_non_zero();

     vm.roll(block.number + 4970);
     vm.warp(block.timestamp + 562841);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI08();

     vm.roll(block.number + 14625);
     vm.warp(block.timestamp + 91);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(157);

     vm.roll(block.number + 27112);
     vm.warp(block.timestamp + 155616);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_viewTotalVotesAndStateEquivalency();

     vm.roll(block.number + 40599);
     vm.warp(block.timestamp + 414007);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

    vm.warp(block.timestamp + 67);

    vm.roll(block.number + 50947);

     vm.roll(block.number + 304);
     vm.warp(block.timestamp + 570946);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 31461);
     vm.warp(block.timestamp + 304);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_initatives_matches_total_votes_bounded();

     vm.roll(block.number + 25538);
     vm.warp(block.timestamp + 177728);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion();

     vm.roll(block.number + 24224);
     vm.warp(block.timestamp + 341154);
     vm.prank(0x0000000000000000000000000000000000020000);
    clamped_claimBribes(156);

     vm.roll(block.number + 57086);
     vm.warp(block.timestamp + 80);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_strict();

    vm.warp(block.timestamp + 90605);

    vm.roll(block.number + 9999);

     vm.roll(block.number + 25158);
     vm.warp(block.timestamp + 490183);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_unregisterable_consistecy(43);

     vm.roll(block.number + 42);
     vm.warp(block.timestamp + 385974);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 12155);
     vm.warp(block.timestamp + 322254);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_unregisterable_consistecy(33);

     vm.roll(block.number + 9966);
     vm.warp(block.timestamp + 222355);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeDoesntRevert(23);

     vm.roll(block.number + 59452);
     vm.warp(block.timestamp + 128965);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(31);

     vm.roll(block.number + 48651);
     vm.warp(block.timestamp + 463589);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 29342);
     vm.warp(block.timestamp + 458443);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldGetTotalVotesAndState();

    vm.warp(block.timestamp + 230919);

    vm.roll(block.number + 5985);

     vm.roll(block.number + 55646);
     vm.warp(block.timestamp + 463587);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI07();

     vm.roll(block.number + 15368);
     vm.warp(block.timestamp + 150273);
     vm.prank(0x0000000000000000000000000000000000010000);
    clamped_claimBribes(31);

     vm.roll(block.number + 49923);
     vm.warp(block.timestamp + 79);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI02();

     vm.roll(block.number + 50537);
     vm.warp(block.timestamp + 230918);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI03();

     vm.roll(block.number + 4896);
     vm.warp(block.timestamp + 95);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI01();

     vm.roll(block.number + 53438);
     vm.warp(block.timestamp + 297344);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 16926);
     vm.warp(block.timestamp + 320276);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiative(172);

    vm.warp(block.timestamp + 193409);

    vm.roll(block.number + 20123);

     vm.roll(block.number + 43283);
     vm.warp(block.timestamp + 468482);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_initiative_offset_matches_user_when_non_zero();

     vm.roll(block.number + 5021);
     vm.warp(block.timestamp + 326330);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 16616);
     vm.warp(block.timestamp + 21);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 31232);
     vm.warp(block.timestamp + 555653);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-01-13T19:10:05Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/0ce11d01-7ee3-48da-b36f-e7afa5be5865

recon-getrecon-xyz · 2025-01-13T19:17:05Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/82f38ddb-8d47-4212-a853-637ed5b8c16b

recon-getrecon-xyz · 2025-01-13T19:17:35Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/422a535b-8c8d-4fc0-a499-5c7deb341573

recon-getrecon-xyz · 2025-01-13T19:19:14Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/1aecacec-35b4-490b-b5ed-52baca0f35cd

recon-getrecon-xyz · 2025-01-13T22:20:01Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 3h6m7s
Coverage: 44133
Failed: 7
Passed: 81

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	✅
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address)	✅
property_sum_of_initatives_matches_total_votes_strict()	✅
AssertionFailed(..)	✅

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 604874);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

    vm.warp(block.timestamp + 65053);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 539766);
    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

    offsetIsRational(1);

    vm.warp(block.timestamp + 604914);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-01-13T22:29:17Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 3h8m31s
Coverage: 44134
Failed: 7
Passed: 81

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	✅
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address)	✅
property_sum_of_initatives_matches_total_votes_strict()	✅
AssertionFailed(..)	✅

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 188165);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 416745);
    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

    governance_depositLQTY(1);

    check_warmup_unregisterable_consistency(0);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    governance_depositLQTY(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 449571);
    offsetIsRational(1);

    vm.warp(block.timestamp + 155236);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-01-13T22:32:12Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 3h8m34s
Coverage: 43631
Failed: 8
Passed: 80

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	❌
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
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.warp(block.timestamp + 132218);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    check_warmup_unregisterable_consistency(0);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    vm.warp(block.timestamp + 472630);

    vm.roll(block.number + 1);

    governance_resetAllocations();

    check_unregisterable_consistecy(0);

 }

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 605233);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

    vm.warp(block.timestamp + 336734);

    vm.roll(block.number + 1);

    governance_depositLQTY(1);

    vm.warp(block.timestamp + 268094);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 32408);

    vm.roll(block.number + 1);

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 572414);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-01-14T07:43:08Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 12h21m52s
Coverage: 43534
Failed: 7
Passed: 81

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	✅
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address)	✅
property_sum_of_initatives_matches_total_votes_strict()	✅
AssertionFailed(..)	✅

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    check_warmup_unregisterable_consistency(0);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

     vm.roll(block.number + 5065);
     vm.warp(block.timestamp + 176489);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_claimable_solvency();

     vm.roll(block.number + 5792);
     vm.warp(block.timestamp + 42);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 31680);
     vm.warp(block.timestamp + 157408);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 44802);
     vm.warp(block.timestamp + 157408);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiativeFuzzTest(251);

     vm.roll(block.number + 37747);
     vm.warp(block.timestamp + 322377);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 39162);
     vm.warp(block.timestamp + 383589);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertepoch();

     vm.roll(block.number + 13535);
     vm.warp(block.timestamp + 364336);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_depositLQTY_2(30271982452169318454359169969229696728725359473106328336480899763061634663126);

     vm.roll(block.number + 40542);
     vm.warp(block.timestamp + 75039);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 21599);
     vm.warp(block.timestamp + 322291);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_claimable_solvency();

    vm.warp(block.timestamp + 878303);

    vm.roll(block.number + 55865);

     vm.roll(block.number + 200);
     vm.warp(block.timestamp + 322365);
     vm.prank(0x0000000000000000000000000000000000030000);
    IS_TEST();

     vm.roll(block.number + 20129);
     vm.warp(block.timestamp + 171500);
     vm.prank(0x0000000000000000000000000000000000030000);
    clamped_claimBribes(223);

     vm.roll(block.number + 257);
     vm.warp(block.timestamp + 6);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_skip_consistecy(1);

     vm.roll(block.number + 44394);
     vm.warp(block.timestamp + 492633);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_warmup_unregisterable_consistency(244);

     vm.roll(block.number + 39209);
     vm.warp(block.timestamp + 322142);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative(120,54318004069326067303995936419509914555080158202328288664976155362672750182326,36661408324494480576580360917921683576629554177966215595708964783359695787409);

     vm.roll(block.number + 5792);
     vm.warp(block.timestamp + 86349);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 34823);
     vm.warp(block.timestamp + 322307);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_allocations_are_never_dangerously_high();

    vm.warp(block.timestamp + 898677);

    vm.roll(block.number + 67);

     vm.roll(block.number + 49415);
     vm.warp(block.timestamp + 306);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(66);

     vm.roll(block.number + 54721);
     vm.warp(block.timestamp + 321627);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI07();

     vm.prank(0x0000000000000000000000000000000000020000);
    check_claim_soundness();

    vm.warp(block.timestamp + 293990);

    vm.roll(block.number + 67);

     vm.roll(block.number + 2497);
     vm.warp(block.timestamp + 569382);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(37);

     vm.roll(block.number + 45261);
     vm.warp(block.timestamp + 78);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_lqty_global_user_matches();

     vm.roll(block.number + 18213);
     vm.warp(block.timestamp + 267435);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI03();

    vm.warp(block.timestamp + 494138);

    vm.roll(block.number + 44879);

     vm.roll(block.number + 50327);
     vm.warp(block.timestamp + 63697);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI02();

     vm.roll(block.number + 31313);
     vm.warp(block.timestamp + 144646);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_deployInitiative();

     vm.roll(block.number + 23721);
     vm.warp(block.timestamp + 449696);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_claim_soundness();

     vm.roll(block.number + 54809);
     vm.warp(block.timestamp + 178399);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x0000000000000000000000000000000000010000);

     vm.roll(block.number + 30505);
     vm.warp(block.timestamp + 458441);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_votes_in_bribes_match();

     vm.roll(block.number + 456);
     vm.warp(block.timestamp + 207834);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_user_offset_is_always_greater_than_start();

     vm.roll(block.number + 23721);
     vm.warp(block.timestamp + 236464);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_lqty_initiative_user_matches();

     vm.roll(block.number + 21601);
     vm.warp(block.timestamp + 89);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_snapshotVotesForInitiative(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 5017);
     vm.warp(block.timestamp + 555652);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV01();

    vm.warp(block.timestamp + 173595);

    vm.roll(block.number + 50536);

     vm.roll(block.number + 57919);
     vm.warp(block.timestamp + 568143);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_deployInitiative();

     vm.roll(block.number + 56920);
     vm.warp(block.timestamp + 247336);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI04();

    vm.warp(block.timestamp + 1170030);

    vm.roll(block.number + 20554);

     vm.roll(block.number + 32959);
     vm.warp(block.timestamp + 202688);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI10();

     vm.roll(block.number + 1001);
     vm.warp(block.timestamp + 590278);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_user_offset_is_always_greater_than_start();

    vm.warp(block.timestamp + 541305);

    vm.roll(block.number + 5);

     vm.roll(block.number + 6944);
     vm.warp(block.timestamp + 221593);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_initatives_matches_total_votes_strict();

     vm.roll(block.number + 35001);
     vm.warp(block.timestamp + 562425);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

    vm.warp(block.timestamp + 153418);

    vm.roll(block.number + 2819);

     vm.roll(block.number + 48651);
     vm.warp(block.timestamp + 179668);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiativeDoesntRevert(154);

    vm.warp(block.timestamp + 574795);

    vm.roll(block.number + 36279);

     vm.roll(block.number + 54329);
     vm.warp(block.timestamp + 344203);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI08();

     vm.roll(block.number + 46305);
     vm.warp(block.timestamp + 95);
     vm.prank(0x0000000000000000000000000000000000030000);
    helper_accrueBold(115792089237316195423570985008687907853269984665640564039457584007913129639735);

     vm.roll(block.number + 50882);
     vm.warp(block.timestamp + 490181);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_registerInitiative(221);

     vm.roll(block.number + 12338);
     vm.warp(block.timestamp + 246073);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiativeDoesntRevert(28);

    vm.warp(block.timestamp + 144647);

    vm.roll(block.number + 5023);

     vm.roll(block.number + 30505);
     vm.warp(block.timestamp + 547623);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 3906);
     vm.warp(block.timestamp + 249334);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_viewCalculateVotingThreshold();

    vm.warp(block.timestamp + 648706);

    vm.roll(block.number + 52039);

     vm.roll(block.number + 13626);
     vm.warp(block.timestamp + 254);
     vm.prank(0x0000000000000000000000000000000000010000);
    clamped_claimBribes(92);

     vm.roll(block.number + 25504);
     vm.warp(block.timestamp + 385873);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_GV_09();

     vm.roll(block.number + 13050);
     vm.warp(block.timestamp + 209930);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI01();

     vm.roll(block.number + 13707);
     vm.warp(block.timestamp + 590279);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_user_voting_weights_strict();

     vm.roll(block.number + 3601);
     vm.warp(block.timestamp + 2099);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY(1000000000000000000000);

    vm.warp(block.timestamp + 374306);

    vm.roll(block.number + 33825);

     vm.roll(block.number + 33823);
     vm.warp(block.timestamp + 445681);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(24191999);

     vm.roll(block.number + 68);
     vm.warp(block.timestamp + 179666);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI10();

     vm.roll(block.number + 31461);
     vm.warp(block.timestamp + 168836);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 17667);
     vm.warp(block.timestamp + 73040);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_initiative_allocations();

     vm.roll(block.number + 15090);
     vm.warp(block.timestamp + 45911);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertsnapshotVotesForInitiative(216);

     vm.roll(block.number + 49925);
     vm.warp(block.timestamp + 149580);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 122);
     vm.warp(block.timestamp + 54939);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 33825);
     vm.warp(block.timestamp + 322262);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewTotalVotesAndStateEquivalency();

     vm.roll(block.number + 37070);
     vm.warp(block.timestamp + 26295);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY_2(47728079488397370013867886287047876098169179848615796776542618999907481089859);

     vm.roll(block.number + 30784);
     vm.warp(block.timestamp + 155524);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeFuzzTest(0);

     vm.roll(block.number + 14467);
     vm.warp(block.timestamp + 221592);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_skip_consistecy(111);

     vm.roll(block.number + 33200);
     vm.warp(block.timestamp + 322333);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_initiative_offset_matches_user_when_non_zero();

     vm.roll(block.number + 232);
     vm.warp(block.timestamp + 337669);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI09();

     vm.roll(block.number + 4702);
     vm.warp(block.timestamp + 191304);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetTotalVotesAndState();

    vm.warp(block.timestamp + 21600);

    vm.roll(block.number + 19811);

     vm.roll(block.number + 26842);
     vm.warp(block.timestamp + 555653);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 51799);
     vm.warp(block.timestamp + 474988);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_initatives_matches_total_votes_bounded();

     vm.roll(block.number + 5215);
     vm.warp(block.timestamp + 322311);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 2512);
     vm.warp(block.timestamp + 41430);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI07();

    vm.warp(block.timestamp + 730714);

    vm.roll(block.number + 9163);

     vm.roll(block.number + 35678);
     vm.warp(block.timestamp + 262803);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_viewCalculateVotingThreshold();

     vm.roll(block.number + 304);
     vm.warp(block.timestamp + 82671);
     vm.prank(0x0000000000000000000000000000000000020000);
    offsetIsRational(621);

     vm.roll(block.number + 12493);
     vm.warp(block.timestamp + 32767);
     vm.prank(0x0000000000000000000000000000000000030000);
    offsetIsRational(51410465162090333642258627402894042234883010866795703786681236120536859592458);

    vm.warp(block.timestamp + 321376);

    vm.roll(block.number + 35680);

     vm.roll(block.number + 4957);
     vm.warp(block.timestamp + 351629);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_snapshotVotesForInitiative(0x537C8f3d3E18dF5517a58B3fB9D9143697996802);

     vm.roll(block.number + 23722);
     vm.warp(block.timestamp + 562840);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_computingGlobalPowerNeverReverts();

     vm.roll(block.number + 13706);
     vm.warp(block.timestamp + 276994);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 460796);

    vm.roll(block.number + 1);

     vm.roll(block.number + 1);
     vm.warp(block.timestamp + 144080);
    governance_depositLQTY(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-01-17T15:30:51Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/2a9e6c62-cb4f-4f71-9d71-a6ef554bea45

recon-getrecon-xyz · 2025-01-17T15:42:47Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 8m6s
Coverage: 43347
Failed: 6
Passed: 82

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	✅
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	✅
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address)	✅
property_sum_of_initatives_matches_total_votes_strict()	✅
AssertionFailed(..)	✅

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

// forge test --match-test  -vv

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

// forge test --match-test  -vv

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

// forge test --match-test  -vv

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

// forge test --match-test  -vv

recon-getrecon-xyz · 2025-01-23T20:51:24Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/5f7ab37c-8a41-4169-b828-d0ac4baae4c5

recon-getrecon-xyz · 2025-01-23T23:16:20Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 2h20m57s
Coverage: 43539
Failed: 7
Passed: 81

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	✅
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address)	✅
property_sum_of_initatives_matches_total_votes_strict()	✅
AssertionFailed(..)	✅

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    check_warmup_unregisterable_consistency(0);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

    check_warmup_unregisterable_consistency(0);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

    check_warmup_unregisterable_consistency(0);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-01-25T07:25:12Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/7b01090a-cdf0-498d-b824-2599c9b74751

recon-getrecon-xyz · 2025-01-25T07:28:01Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/f057b60e-b4d6-446c-b898-159ba95c549e

recon-getrecon-xyz · 2025-01-25T09:52:48Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 2h23m12s
Coverage: 44163
Failed: 7
Passed: 81

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	✅
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address)	✅
property_sum_of_initatives_matches_total_votes_strict()	✅
AssertionFailed(..)	✅

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 605285);

    vm.roll(block.number + 1);

    offsetIsRational(1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

    vm.warp(block.timestamp + 203958);

    vm.roll(block.number + 1);

    governance_depositLQTY_2(2);

    vm.warp(block.timestamp + 400852);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    offsetIsRational(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    offsetIsRational(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

    governance_depositLQTY(1);

    check_warmup_unregisterable_consistency(0);

    governance_allocateLQTY_clamped_single_initiative(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-01-25T17:18:20Z

Recon Job Completed

Job link

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 9h45m47s
Coverage: 43543
Failed: 7
Passed: 81

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	✅
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
property_shouldNeverRevertgetInitiativeState_arbitrary(address)	✅
property_sum_of_initatives_matches_total_votes_strict()	✅
AssertionFailed(..)	✅

Broken Properties

Broken property:

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property:

property_user_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 415303);

    vm.roll(block.number + 1);

     vm.roll(block.number + 38428);
     vm.warp(block.timestamp + 584678);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertepochStart(175);

     vm.roll(block.number + 17978);
     vm.warp(block.timestamp + 470918);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 27082);
     vm.warp(block.timestamp + 34999);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_depositLQTY(980434489862535122532839671621850136682886138603857338951075551449220982906);

    vm.warp(block.timestamp + 1206497);

    vm.roll(block.number + 89156);

     vm.roll(block.number + 5755);
     vm.warp(block.timestamp + 322256);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsnapshotVotesForInitiative(92);

     vm.roll(block.number + 4969);
     vm.warp(block.timestamp + 32);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 13049);
     vm.warp(block.timestamp + 463586);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 39966);
     vm.warp(block.timestamp + 326330);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY_2(65908770601948123404248239116764872052243205512450135194750736667335892885538);

     vm.roll(block.number + 5424);
     vm.warp(block.timestamp + 82670);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(120,23569449409106557262957233949368549182918544656316155486763670793983267687358,0);

     vm.roll(block.number + 46994);
     vm.warp(block.timestamp + 131072);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiativeDoesntRevert(12);

     vm.roll(block.number + 20705);
     vm.warp(block.timestamp + 221594);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI01();

     vm.roll(block.number + 14577);
     vm.warp(block.timestamp + 287375);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV_09();

     vm.roll(block.number + 13706);
     vm.warp(block.timestamp + 322199);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_snapshotVotesForInitiative(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 60082);
     vm.warp(block.timestamp + 31);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_accrueBold(115792089237316195423570985008687907853269984665639249934778214178769438099525);

     vm.roll(block.number + 4744);
     vm.warp(block.timestamp + 379005);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_allocateLQTY_clamped_single_initiative(177,78363234549508722316540008268595430344569895777225259017253654231236996731491,344202);

     vm.roll(block.number + 58560);
     vm.warp(block.timestamp + 296079);
     vm.prank(0x0000000000000000000000000000000000030000);
    withdrwaMustFailOnNonZeroAcc(3462088984370236793744539405394596614183654319743535522713895824900884737619);

     vm.roll(block.number + 15668);
     vm.warp(block.timestamp + 359031);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimFromStakingV1(166);

     vm.roll(block.number + 49415);
     vm.warp(block.timestamp + 119687);
     vm.prank(0x0000000000000000000000000000000000010000);
    initiative_claimBribes(50000000001,31559509245836018122417756822360695327197767626631073063211407275990916460884,101783926054423881238782776520702182300558147017617886449977999902561801294357,63);

     vm.roll(block.number + 1522);
     vm.warp(block.timestamp + 437952);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_initiative_allocations();

    vm.warp(block.timestamp + 677646);

    vm.roll(block.number + 57643);

     vm.roll(block.number + 31461);
     vm.warp(block.timestamp + 236464);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 40255);
     vm.warp(block.timestamp + 135921);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_unregisterable_consistecy(252);

     vm.roll(block.number + 10870);
     vm.warp(block.timestamp + 4177);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_user_offset_is_always_greater_than_start();

     vm.roll(block.number + 41166);
     vm.warp(block.timestamp + 78570);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI02();

     vm.roll(block.number + 5217);
     vm.warp(block.timestamp + 83001);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetLatestVotingThreshold();

     vm.roll(block.number + 28952);
     vm.warp(block.timestamp + 198172);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 4901);
     vm.warp(block.timestamp + 471566);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_user_offset_is_always_greater_than_start();

    vm.warp(block.timestamp + 507332);

    vm.roll(block.number + 304);

     vm.roll(block.number + 51036);
     vm.warp(block.timestamp + 207289);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(95);

     vm.roll(block.number + 215);
     vm.warp(block.timestamp + 137558);
     vm.prank(0x0000000000000000000000000000000000020000);
    failed();

     vm.roll(block.number + 200);
     vm.warp(block.timestamp + 31595);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 4928);
     vm.warp(block.timestamp + 100782);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI03();

     vm.roll(block.number + 40300);
     vm.warp(block.timestamp + 458696);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI10();

     vm.roll(block.number + 5983);
     vm.warp(block.timestamp + 195123);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV01();

    vm.warp(block.timestamp + 232);

    vm.roll(block.number + 35000);

     vm.roll(block.number + 5034);
     vm.warp(block.timestamp + 150273);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000002fFffFffD);

     vm.roll(block.number + 5425);
     vm.warp(block.timestamp + 30);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_lqty_global_user_matches();

    vm.warp(block.timestamp + 78498);

    vm.roll(block.number + 5009);

     vm.roll(block.number + 17911);
     vm.warp(block.timestamp + 448427);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

    vm.warp(block.timestamp + 474831);

    vm.roll(block.number + 33175);

     vm.roll(block.number + 19933);
     vm.warp(block.timestamp + 136778);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiative(146);

     vm.roll(block.number + 4718);
     vm.warp(block.timestamp + 445682);
     vm.prank(0x0000000000000000000000000000000000020000);
    initiative_claimBribes(7519399803948305637604261191783778306301874215410234874682620206984448630036,115792089237316195423570985008687907853269984665639249934778214178769438099525,110227598510015232952159290248299032460333140316117538596416580206512361598231,251);

    vm.warp(block.timestamp + 198174);

    vm.roll(block.number + 19034);

     vm.roll(block.number + 63);
     vm.warp(block.timestamp + 282374);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion();

    vm.warp(block.timestamp + 484091);

    vm.roll(block.number + 4234);

     vm.roll(block.number + 54720);
     vm.warp(block.timestamp + 360625);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI07();

     vm.roll(block.number + 3906);
     vm.warp(block.timestamp + 32562);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeFuzzTest(124);

     vm.roll(block.number + 1423);
     vm.warp(block.timestamp + 574631);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertSnapshotAndState(14);

    vm.warp(block.timestamp + 160);

    vm.roll(block.number + 5008);

     vm.prank(0x0000000000000000000000000000000000010000);
    helper_accrueBold(64935821119286490250636400323418451983660841281378349873548227573599974368889);

     vm.roll(block.number + 32500);
     vm.warp(block.timestamp + 206513);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_bounded();

     vm.roll(block.number + 53429);
     vm.warp(block.timestamp + 476992);
     vm.prank(0x0000000000000000000000000000000000030000);
    withdrwaMustFailOnNonZeroAcc(22434200055774865026805877043896449584815222637782454252055153387822823053661);

     vm.roll(block.number + 45819);
     vm.warp(block.timestamp + 231770);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_user_offset_is_always_greater_than_start();

     vm.roll(block.number + 4234);
     vm.warp(block.timestamp + 287844);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI08();

     vm.roll(block.number + 55506);
     vm.warp(block.timestamp + 474683);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 32958);
     vm.warp(block.timestamp + 562841);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

    vm.warp(block.timestamp + 289103);

    vm.roll(block.number + 48578);

     vm.roll(block.number + 2497);
     vm.warp(block.timestamp + 256841);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_bounded();

     vm.roll(block.number + 40541);
     vm.warp(block.timestamp + 243805);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_ensure_user_alloc_cannot_dos();

     vm.roll(block.number + 58055);
     vm.warp(block.timestamp + 298424);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 50415);
     vm.warp(block.timestamp + 151690);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_claimable_solvency();

    vm.warp(block.timestamp + 419859);

    vm.roll(block.number + 45818);

     vm.roll(block.number + 31523);
     vm.warp(block.timestamp + 322332);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV_09();

     vm.roll(block.number + 233);
     vm.warp(block.timestamp + 45382);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 15734);
     vm.warp(block.timestamp + 322312);
     vm.prank(0x0000000000000000000000000000000000020000);
    clamped_claimBribes(87);

     vm.roll(block.number + 60319);
     vm.warp(block.timestamp + 231772);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY(75039);

     vm.roll(block.number + 19812);
     vm.warp(block.timestamp + 16802);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_user_offset_is_always_greater_than_start();

 }

Broken property:

property_sum_of_lqty_initiative_user_matches

Sequence

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

    offsetIsRational(1);

    vm.warp(block.timestamp + 604967);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property:

withdrwaMustFailOnNonZeroAcc

Sequence

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

    governance_depositLQTY(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property:

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property:

depositMustFailOnNonZeroAlloc

Sequence

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

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property:

property_global_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 415303);

    vm.roll(block.number + 1);

     vm.roll(block.number + 38428);
     vm.warp(block.timestamp + 584678);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertepochStart(175);

     vm.roll(block.number + 17978);
     vm.warp(block.timestamp + 470918);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_summingInitiativesPowerNeverReverts();

     vm.roll(block.number + 27082);
     vm.warp(block.timestamp + 34999);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_depositLQTY(980434489862535122532839671621850136682886138603857338951075551449220982906);

    vm.warp(block.timestamp + 1206497);

    vm.roll(block.number + 89156);

     vm.roll(block.number + 5755);
     vm.warp(block.timestamp + 322256);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsnapshotVotesForInitiative(92);

     vm.roll(block.number + 4969);
     vm.warp(block.timestamp + 32);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 13049);
     vm.warp(block.timestamp + 463586);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 39966);
     vm.warp(block.timestamp + 326330);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY_2(65908770601948123404248239116764872052243205512450135194750736667335892885538);

     vm.roll(block.number + 5424);
     vm.warp(block.timestamp + 82670);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(120,23569449409106557262957233949368549182918544656316155486763670793983267687358,0);

     vm.roll(block.number + 46994);
     vm.warp(block.timestamp + 131072);
     vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiativeDoesntRevert(12);

     vm.roll(block.number + 20705);
     vm.warp(block.timestamp + 221594);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_BI01();

     vm.roll(block.number + 14577);
     vm.warp(block.timestamp + 287375);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV_09();

     vm.roll(block.number + 13706);
     vm.warp(block.timestamp + 322199);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_snapshotVotesForInitiative(0x00000000000000000000000000000001fffffffE);

     vm.roll(block.number + 60082);
     vm.warp(block.timestamp + 31);
     vm.prank(0x0000000000000000000000000000000000020000);
    helper_accrueBold(115792089237316195423570985008687907853269984665639249934778214178769438099525);

     vm.roll(block.number + 4744);
     vm.warp(block.timestamp + 379005);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_allocateLQTY_clamped_single_initiative(177,78363234549508722316540008268595430344569895777225259017253654231236996731491,344202);

     vm.roll(block.number + 58560);
     vm.warp(block.timestamp + 296079);
     vm.prank(0x0000000000000000000000000000000000030000);
    withdrwaMustFailOnNonZeroAcc(3462088984370236793744539405394596614183654319743535522713895824900884737619);

     vm.roll(block.number + 15668);
     vm.warp(block.timestamp + 359031);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimFromStakingV1(166);

     vm.roll(block.number + 49415);
     vm.warp(block.timestamp + 119687);
     vm.prank(0x0000000000000000000000000000000000010000);
    initiative_claimBribes(50000000001,31559509245836018122417756822360695327197767626631073063211407275990916460884,101783926054423881238782776520702182300558147017617886449977999902561801294357,63);

     vm.roll(block.number + 1522);
     vm.warp(block.timestamp + 437952);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_initiative_allocations();

    vm.warp(block.timestamp + 677646);

    vm.roll(block.number + 57643);

     vm.roll(block.number + 31461);
     vm.warp(block.timestamp + 236464);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertsecondsWithinEpoch();

     vm.roll(block.number + 40255);
     vm.warp(block.timestamp + 135921);
     vm.prank(0x0000000000000000000000000000000000030000);
    check_unregisterable_consistecy(252);

     vm.roll(block.number + 10870);
     vm.warp(block.timestamp + 4177);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_user_offset_is_always_greater_than_start();

     vm.roll(block.number + 41166);
     vm.warp(block.timestamp + 78570);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI02();

     vm.roll(block.number + 5217);
     vm.warp(block.timestamp + 83001);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetLatestVotingThreshold();

     vm.roll(block.number + 28952);
     vm.warp(block.timestamp + 198172);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 4901);
     vm.warp(block.timestamp + 471566);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_user_offset_is_always_greater_than_start();

    vm.warp(block.timestamp + 507332);

    vm.roll(block.number + 304);

     vm.roll(block.number + 51036);
     vm.warp(block.timestamp + 207289);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY(95);

     vm.roll(block.number + 215);
     vm.warp(block.timestamp + 137558);
     vm.prank(0x0000000000000000000000000000000000020000);
    failed();

     vm.roll(block.number + 200);
     vm.warp(block.timestamp + 31595);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

     vm.roll(block.number + 4928);
     vm.warp(block.timestamp + 100782);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI03();

     vm.roll(block.number + 40300);
     vm.warp(block.timestamp + 458696);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI10();

     vm.roll(block.number + 5983);
     vm.warp(block.timestamp + 195123);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV01();

    vm.warp(block.timestamp + 232);

    vm.roll(block.number + 35000);

     vm.roll(block.number + 5034);
     vm.warp(block.timestamp + 150273);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000002fFffFffD);

     vm.roll(block.number + 5425);
     vm.warp(block.timestamp + 30);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_lqty_global_user_matches();

    vm.warp(block.timestamp + 78498);

    vm.roll(block.number + 5009);

     vm.roll(block.number + 17911);
     vm.warp(block.timestamp + 448427);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

    vm.warp(block.timestamp + 474831);

    vm.roll(block.number + 33175);

     vm.roll(block.number + 19933);
     vm.warp(block.timestamp + 136778);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiative(146);

     vm.roll(block.number + 4718);
     vm.warp(block.timestamp + 445682);
     vm.prank(0x0000000000000000000000000000000000020000);
    initiative_claimBribes(7519399803948305637604261191783778306301874215410234874682620206984448630036,115792089237316195423570985008687907853269984665639249934778214178769438099525,110227598510015232952159290248299032460333140316117538596416580206512361598231,251);

    vm.warp(block.timestamp + 198174);

    vm.roll(block.number + 19034);

     vm.roll(block.number + 63);
     vm.warp(block.timestamp + 282374);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion();

    vm.warp(block.timestamp + 484091);

    vm.roll(block.number + 4234);

     vm.roll(block.number + 54720);
     vm.warp(block.timestamp + 360625);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI07();

     vm.roll(block.number + 3906);
     vm.warp(block.timestamp + 32562);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeFuzzTest(124);

     vm.roll(block.number + 1423);
     vm.warp(block.timestamp + 574631);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertSnapshotAndState(14);

    vm.warp(block.timestamp + 160);

    vm.roll(block.number + 5008);

     vm.prank(0x0000000000000000000000000000000000010000);
    helper_accrueBold(64935821119286490250636400323418451983660841281378349873548227573599974368889);

     vm.roll(block.number + 32500);
     vm.warp(block.timestamp + 206513);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_bounded();

     vm.roll(block.number + 53429);
     vm.warp(block.timestamp + 476992);
     vm.prank(0x0000000000000000000000000000000000030000);
    withdrwaMustFailOnNonZeroAcc(22434200055774865026805877043896449584815222637782454252055153387822823053661);

     vm.roll(block.number + 45819);
     vm.warp(block.timestamp + 231770);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_user_offset_is_always_greater_than_start();

     vm.roll(block.number + 4234);
     vm.warp(block.timestamp + 287844);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI08();

     vm.roll(block.number + 55506);
     vm.warp(block.timestamp + 474683);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetTotalVotesAndState();

     vm.roll(block.number + 32958);
     vm.warp(block.timestamp + 562841);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

    vm.warp(block.timestamp + 289103);

    vm.roll(block.number + 48578);

     vm.roll(block.number + 2497);
     vm.warp(block.timestamp + 256841);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_user_voting_weights_bounded();

     vm.roll(block.number + 40541);
     vm.warp(block.timestamp + 243805);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_ensure_user_alloc_cannot_dos();

     vm.roll(block.number + 58055);
     vm.warp(block.timestamp + 298424);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_allocations_are_never_dangerously_high();

     vm.roll(block.number + 50415);
     vm.warp(block.timestamp + 151690);
     vm.prank(0x0000000000000000000000000000000000020000);
    check_claimable_solvency();

    vm.warp(block.timestamp + 419859);

    vm.roll(block.number + 45818);

     vm.roll(block.number + 31523);
     vm.warp(block.timestamp + 322332);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_GV_09();

     vm.roll(block.number + 233);
     vm.warp(block.timestamp + 45382);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_global_offset_is_always_greater_than_start();

     vm.roll(block.number + 15734);
     vm.warp(block.timestamp + 322312);
     vm.prank(0x0000000000000000000000000000000000020000);
    clamped_claimBribes(87);

     vm.roll(block.number + 60319);
     vm.warp(block.timestamp + 231772);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_depositLQTY(75039);

    vm.warp(block.timestamp + 16802);

    vm.roll(block.number + 19812);

     vm.roll(block.number + 100);
     vm.warp(block.timestamp + 236027);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_BI07();

     vm.roll(block.number + 5375);
     vm.warp(block.timestamp + 867);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimForInitiativeDoesntRevert(141);

     vm.roll(block.number + 37096);
     vm.warp(block.timestamp + 65534);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_snapshotVotesForInitiative(0x00000000000000000000000000000002fFffFffD);

     vm.roll(block.number + 32547);
     vm.warp(block.timestamp + 317222);
     vm.prank(0x0000000000000000000000000000000000020000);
    governance_claimFromStakingV1(149);

     vm.roll(block.number + 5019);
     vm.warp(block.timestamp + 458442);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI09();

     vm.roll(block.number + 23706);
     vm.warp(block.timestamp + 216);
     vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiative(37);

     vm.roll(block.number + 15097);
     vm.warp(block.timestamp + 474049);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_viewCalculateVotingThreshold();

    vm.warp(block.timestamp + 644632);

    vm.roll(block.number + 96690);

     vm.roll(block.number + 33655);
     vm.warp(block.timestamp + 325679);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldGetTotalVotesAndState();

     vm.roll(block.number + 18959);
     vm.warp(block.timestamp + 322336);
     vm.prank(0x0000000000000000000000000000000000030000);
    property_sum_of_initatives_matches_total_votes_bounded();

    vm.warp(block.timestamp + 75039);

    vm.roll(block.number + 60452);

     vm.roll(block.number + 60440);
     vm.warp(block.timestamp + 321585);
     vm.prank(0x0000000000000000000000000000000000010000);
    check_realized_claiming_solvency();

     vm.roll(block.number + 38704);
     vm.warp(block.timestamp + 496528);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_user_voting_weights_bounded();

     vm.roll(block.number + 2924);
     vm.warp(block.timestamp + 385873);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeState(23);

    vm.warp(block.timestamp + 570946);

    vm.roll(block.number + 49837);

     vm.roll(block.number + 58783);
     vm.warp(block.timestamp + 322358);
     vm.prank(0x0000000000000000000000000000000000030000);
    initiative_depositBribe(115792089237316195423570985008687907853269984665640564039457584007913129639906,65536,115792089237316195423570985008687907853269984665640564039457584007913129564895,32);

    vm.warp(block.timestamp + 135334);

    vm.roll(block.number + 47079);

     vm.roll(block.number + 24964);
     vm.warp(block.timestamp + 320294);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_BI02();

    vm.warp(block.timestamp + 10);

    vm.roll(block.number + 15090);

     vm.roll(block.number + 4902);
     vm.warp(block.timestamp + 21600);
     vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

    vm.warp(block.timestamp + 875486);

    vm.roll(block.number + 112320);

     vm.roll(block.number + 19726);
     vm.warp(block.timestamp + 202688);
     vm.prank(0x0000000000000000000000000000000000020000);
    property_global_offset_is_always_greater_than_start();

 }

recon-getrecon-xyz · 2025-06-13T06:37:12Z

Recon Campaign Started

Recipe: Liquity10MLNCI/CDwithCorpusReuse | Job URL: https://getrecon.xyz/dashboard/jobs/a0a38b0c-8083-4699-b96f-a13fcdfaf11d

recon-getrecon-xyz · 2025-06-13T10:31:24Z

Recon Job Completed

Job link

Recon Recap for Campaign - [RECURRING]-Liquity10MLNCI/CDwithCorpusReuse

Fuzzer overview

Fuzzer: ECHIDNA
Duration: 3h51m8s
Coverage: 43329
Failed: 8
Passed: 80
Number of tests: 9747013

Results

Property	Status
initiative_claimBribes(uint256,uint256,uint256,uint8)	✅
check_unregisterable_consistecy(uint8)	❌
check_claimable_solvency()	✅
excludeSenders()	✅
property_shouldNeverRevertgetInitiativeState(uint8)	✅
check_realized_claiming_solvency()	✅
targetInterfaces()	✅
property_shouldNeverRevertgetInitiativeSnapshotAndState(uint8)	✅
helper_accrueBold(uint256)	✅
property_BI02()	✅
property_computingGlobalPowerNeverReverts()	✅
governance_resetAllocations()	✅
property_initiative_offset_matches_user_when_non_zero()	✅
targetSenders()	✅
targetContracts()	✅
property_shouldGetTotalVotesAndState()	✅
property_BI10()	✅
property_shouldNeverRevertcalculateVotingThreshold()	✅
governance_allocateLQTY_clamped_single_initiative(uint8,uint256,uint256)	✅
property_sum_of_user_voting_weights_strict()	✅
property_sum_of_user_initiative_allocations()	✅
property_summingInitiativesPowerNeverReverts()	✅
governance_withdrawLQTY_shouldRevertWhenClamped(uint256)	❌
property_user_offset_is_always_greater_than_start()	❌
helper_deployInitiative()	✅
property_sum_of_lqty_global_user_matches()	✅
property_sum_of_votes_in_bribes_match()	✅
governance_allocateLQTY_clamped_single_initiative_2nd_user(uint8,uint256,uint256)	✅
targetArtifactSelectors()	✅
property_sum_of_lqty_initiative_user_matches()	❌
property_GV01()	✅
property_viewCalculateVotingThreshold()	✅
governance_registerInitiative(uint8)	✅
initiative_depositBribe(uint256,uint256,uint256,uint8)	✅
property_shouldNeverRevertsnapshotVotesForInitiative(uint8)	✅
property_BI07()	✅
governance_resetAllocations_user_2()	✅
targetArtifacts()	✅
withdrwaMustFailOnNonZeroAcc(uint256)	❌
property_sum_of_initatives_matches_total_votes_bounded()	✅
property_BI04()	✅
targetSelectors()	✅
property_resetting_never_reverts(address[])	❌
governance_depositLQTY_2(uint256)	✅
governance_depositLQTY(uint256)	✅
check_warmup_unregisterable_consistency(uint8)	✅
property_ensure_user_alloc_cannot_dos()	✅
property_BI08()	✅
governance_withdrawLQTY(uint256)	✅
property_sum_of_initatives_matches_total_votes_insolvency_assertion()	✅
property_shouldNeverRevertgetLatestVotingThreshold()	✅
governance_claimForInitiativeDoesntRevert(uint8)	✅
property_BI03()	✅
excludeSelectors()	✅
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()	✅
depositMustFailOnNonZeroAlloc(uint256)	❌
offsetIsRational(uint256)	✅
property_allocations_are_never_dangerously_high()	✅
property_global_offset_is_always_greater_than_start()	❌
property_shouldNeverRevertgetTotalVotesAndState()	✅
clamped_claimBribes(uint8)	✅
property_shouldNeverRevertepoch()	✅
governance_claimForInitiative(uint8)	✅
property_GV_09()	✅
excludeContracts()	✅
governance_claimForInitiativeFuzzTest(uint8)	✅
property_alloc_deposit_reset_is_idempotent(uint8,uint256,uint256,uint256)	✅
property_viewTotalVotesAndStateEquivalency()	✅
check_skip_consistecy(uint8)	✅
governance_unregisterInitiative(uint8)	✅
governance_claimFromStakingV1(uint8)	✅
governance_allocateLQTY(int256[],int256[])	✅
IS_TEST()	✅
governance_depositLQTYViaPermit(uint256)	✅
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 + 42595);
    vm.warp(block.timestamp + 275394);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetLatestVotingThreshold();

    vm.roll(block.number + 59983);
    vm.warp(block.timestamp + 322247);
    vm.prank(0x0000000000000000000000000000000000020000);
    offsetIsRational(18698785559767234308485994349901935632654962443251371759342487047845933307045);

    vm.roll(block.number + 38100);
    vm.warp(block.timestamp + 172101);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_BI10();

    vm.roll(block.number + 15368);
    vm.warp(block.timestamp + 407328);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(241);

    vm.roll(block.number + 5237);
    vm.warp(block.timestamp + 271957);
    vm.prank(0x0000000000000000000000000000000000020000);
    governance_resetAllocations_user_2();

    vm.roll(block.number + 45261);
    vm.warp(block.timestamp + 117472);
    vm.prank(0x0000000000000000000000000000000000020000);
    targetContracts();

    vm.roll(block.number + 11826);
    vm.warp(block.timestamp + 73040);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(97);

    vm.roll(block.number + 30784);
    vm.warp(block.timestamp + 195123);
    vm.prank(0x0000000000000000000000000000000000020000);
    governance_depositLQTY_2(115792089237316195423570985008687907853269984665640564039457584007913129639935);

    vm.roll(block.number + 11942);
    vm.warp(block.timestamp + 512439);
    vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(85,115792089237316195423570985008687907853269984665640564039457584007913129639935,1524785992);

    vm.roll(block.number + 50499);
    vm.warp(block.timestamp + 318197);
    vm.prank(0x0000000000000000000000000000000000010000);
    targetArtifactSelectors();

    vm.roll(block.number + 4223);
    vm.warp(block.timestamp + 437838);
    vm.prank(0x0000000000000000000000000000000000030000);
    targetContracts();

    vm.roll(block.number + 59982);
    vm.warp(block.timestamp + 136393);
    vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(255,4370000,0);

    vm.roll(block.number + 32737);
    vm.warp(block.timestamp + 127251);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeState_arbitrary(0x00000000000000000000000000000001fffffffE);

    vm.roll(block.number + 18454);
    vm.warp(block.timestamp + 521319);
    vm.prank(0x0000000000000000000000000000000000010000);
    IS_TEST();

    vm.roll(block.number + 18429);
    vm.warp(block.timestamp + 136392);
    vm.prank(0x0000000000000000000000000000000000020000);
    governance_registerInitiative(108);

    vm.roll(block.number + 53451);
    vm.warp(block.timestamp + 277232);
    vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertgetTotalVotesAndState();

    vm.roll(block.number + 30304);
    vm.warp(block.timestamp + 318197);
    vm.prank(0x0000000000000000000000000000000000020000);
    initiative_depositBribe(51947116735080084123288890729153611860856303365792676951508838661187427065605,23510352913908745032819990714767880241661082260116859565621375405122723978667,8797956389523682348217936601978604271179078040531223405374994476878965457933,162);

    vm.roll(block.number + 58145);
    vm.warp(block.timestamp + 338920);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertepochStart(255);

    vm.roll(block.number + 38100);
    vm.warp(block.timestamp + 112444);
    vm.prank(0x0000000000000000000000000000000000030000);
    clamped_claimBribes(255);

    vm.roll(block.number + 2512);
    vm.warp(block.timestamp + 444463);
    vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertepoch();

    vm.roll(block.number + 53562);
    vm.warp(block.timestamp + 171757);
    vm.prank(0x0000000000000000000000000000000000030000);
    check_unregisterable_consistecy(255);

    vm.roll(block.number + 60267);
    vm.warp(block.timestamp + 275394);
    vm.prank(0x0000000000000000000000000000000000020000);
    governance_allocateLQTY_clamped_single_initiative_2nd_user(200,13845603416346869014951986205936422679918940718178656131090642547430951570076,66695979850015339545425757007667139188991030124806693142224082633231443829852);

    vm.roll(block.number + 2512);
    vm.warp(block.timestamp + 569114);
    vm.prank(0x0000000000000000000000000000000000010000);
    targetSelectors();

    vm.roll(block.number + 16089);
    vm.warp(block.timestamp + 31594);
    vm.prank(0x0000000000000000000000000000000000010000);
    governance_allocateLQTY_clamped_single_initiative(24,4370000,1524785992);

    vm.roll(block.number + 59552);
    vm.warp(block.timestamp + 4177);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_BI09();

    vm.roll(block.number + 3661);
    vm.warp(block.timestamp + 135921);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(30);

    vm.roll(block.number + 6721);
    vm.warp(block.timestamp + 254414);
    vm.prank(0x0000000000000000000000000000000000030000);
    governance_withdrawLQTY(80101211895139483777232000074637638464390133163462526346000704984451327727281);

    vm.roll(block.number + 44699);
    vm.warp(block.timestamp + 519802);
    vm.prank(0x0000000000000000000000000000000000010000);
    targetArtifacts();

    vm.roll(block.number + 800);
    vm.warp(block.timestamp + 45142);
    vm.prank(0x0000000000000000000000000000000000010000);
    check_warmup_unregisterable_consistency(255);

    vm.roll(block.number + 11349);
    vm.warp(block.timestamp + 127251);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertgetInitiativeSnapshotAndState(8);

    vm.roll(block.number + 11349);
    vm.warp(block.timestamp + 360624);
    vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertlqtyToVotes();

    vm.roll(block.number + 52862);
    vm.warp(block.timestamp + 16802);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertcalculateVotingThreshold();

    vm.roll(block.number + 20243);
    vm.warp(block.timestamp + 437838);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_BI10();

    vm.roll(block.number + 11942);
    vm.warp(block.timestamp + 420078);
    vm.prank(0x0000000000000000000000000000000000010000);
    excludeSelectors();

    vm.roll(block.number + 204);
    vm.warp(block.timestamp + 156190);
    vm.prank(0x0000000000000000000000000000000000020000);
    targetArtifactSelectors();

    vm.roll(block.number + 5054);
    vm.warp(block.timestamp + 376096);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertsecondsWithinEpoch();

    vm.roll(block.number + 59981);
    vm.warp(block.timestamp + 358061);
    vm.prank(0x0000000000000000000000000000000000030000);
    property_shouldNeverRevertepoch();

    vm.roll(block.number + 800);
    vm.warp(block.timestamp + 112444);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_shouldNeverRevertcalculateVotingThreshold();

    vm.roll(block.number + 47075);
    vm.warp(block.timestamp + 437838);
    vm.prank(0x0000000000000000000000000000000000030000);
    governance_allocateLQTY_clamped_single_initiative(255,0,4369999);

    vm.roll(block.number + 23978);
    vm.warp(block.timestamp + 463587);
    vm.prank(0x0000000000000000000000000000000000010000);
    governance_depositLQTYViaPermit(1524785991);

    vm.roll(block.number + 127);
    vm.warp(block.timestamp + 490446);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_shouldNeverRevertepochStart(178);

    vm.roll(block.number + 42101);
    vm.warp(block.timestamp + 407328);
    vm.prank(0x0000000000000000000000000000000000010000);
    targetSelectors();

    vm.roll(block.number + 53349);
    vm.warp(block.timestamp + 420078);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_allocations_are_never_dangerously_high();

    vm.roll(block.number + 32147);
    vm.warp(block.timestamp + 376096);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_initatives_matches_total_votes_insolvency_assertion();

    vm.roll(block.number + 30304);
    vm.warp(block.timestamp + 463587);
    vm.prank(0x0000000000000000000000000000000000010000);
    governance_claimForInitiativeDoesntRevert(80);

    vm.roll(block.number + 52338);
    vm.warp(block.timestamp + 525476);
    vm.prank(0x0000000000000000000000000000000000010000);
    excludeContracts();

    vm.roll(block.number + 40177);
    vm.warp(block.timestamp + 271957);
    vm.prank(0x0000000000000000000000000000000000020000);
    governance_deployUserProxy();

    vm.roll(block.number + 5053);
    vm.warp(block.timestamp + 507578);
    vm.prank(0x0000000000000000000000000000000000030000);
    governance_claimForInitiativeDoesntRevert(80);

    vm.roll(block.number + 40746);
    vm.warp(block.timestamp + 554465);
    vm.prank(0x0000000000000000000000000000000000010000);
    property_sum_of_user_voting_weights_bounded();

    vm.roll(block.number + 35248);
    vm.warp(block.timestamp + 215219);
    vm.prank(0x0000000000000000000000000000000000030000);
    initiative_claimBribes(115792089237316195423570985008687907853269984665640564039457584007913129639935,1524785991,7272840154226483828144575738959455141152329008074346212580476161947314974350,255);

    vm.roll(block.number + 46422);
    vm.warp(block.timestamp + 115085);
    vm.prank(0x0000000000000000000000000000000000020000);
    property_sum_of_initatives_matches_total_votes_strict();

 }

Broken property

governance_withdrawLQTY_shouldRevertWhenClamped

Sequence

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

    governance_withdrawLQTY_shouldRevertWhenClamped(0);

 }

Broken property

property_user_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 394807);

    vm.roll(block.number + 1);

    governance_depositLQTY(1);

    vm.warp(block.timestamp + 210080);

    vm.roll(block.number + 1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_user_offset_is_always_greater_than_start();

 }

Broken property

property_sum_of_lqty_initiative_user_matches

Sequence

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

    vm.warp(block.timestamp + 604868);

    vm.roll(block.number + 1);

    governance_depositLQTY(1);

    governance_allocateLQTY_clamped_single_initiative(0,0,1);

    property_sum_of_lqty_initiative_user_matches();

 }

Broken property

withdrwaMustFailOnNonZeroAcc

Sequence

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

    governance_depositLQTY(1);

    withdrwaMustFailOnNonZeroAcc(0);

 }

Broken property

property_resetting_never_reverts

Sequence

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

    property_resetting_never_reverts([0x0000000000000000000000000000000000000000]);

 }

Broken property

depositMustFailOnNonZeroAlloc

Sequence

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

    governance_depositLQTY(1);

    depositMustFailOnNonZeroAlloc(1);

 }

Broken property

property_global_offset_is_always_greater_than_start

Sequence

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

    vm.warp(block.timestamp + 605499);

    vm.roll(block.number + 1);

    governance_depositLQTY_2(2);

    governance_allocateLQTY_clamped_single_initiative_2nd_user(0,1,0);

    property_global_offset_is_always_greater_than_start();

 }

bingen · 2025-06-13T14:23:21Z

This is not maintained, so closing it for now.

danielattilasimon and others added 30 commits November 19, 2024 10:11

fix: unnecessary approval given to LQTYStaking

6ef567f

Fixes CS-V2Gov-020.

chore: remove unused import

a92385d

test: improved MockStakingV1

ee3e805

chore: remove unused imports

b4e5140

fix: Remove ForwardBribe contract

c2a95c8

fix: Move lqty allocation checks

2fa865d

As value now encodes timestamp, it would never be zero, we need to decode and then check.

fix: Remove safeTransfer from UserProxy

9804d92

Both LUSD and LQTY are already safe.

fix: Emit both amounts coming from LQTYStaking and total ones on unst…

b83fad5

…aking

test: mocked & forked UserProxy tests

32d322e

chore: update forge-std

992f6f8

Needed for `vm.expectPartialRevert()`

test: mocked & forked Governance tests

4c8055a

test: mocked & forked Governance attack tests

a0de52f

test: mocked & forked UniV4Donations tests

e38d05d

fix: Make LQTY staking claiming consistent across endpoints

24deef5

test: mocked & forked voting power tests

12bdf39

test: fix failing tests

8e6f374

Fixes IR-02.

test: clean up Governance setup in some test contracts

eaac7be

test: ensure all forked tests are prefixed with Forked

22ece8a

chore: fix typo in comment

4941886

ci: add color

0f49049

test: fix excessive vm.assume() rejection

7e9c169

ci: alternative attempt at color

613bf67

ci: remove unnecessary dependency on lint & build

7f3abac

ci: tone down fuzz runs

19c5621

It was taking 20 minutes for a single test run.

fix: Prevent NOPs on allacation and resetting

69fb063

Merge pull request #76 from liquity/cs-024

5c7e0e6

fix: Remove safeTransfer from UserProxy

Merge pull request #78 from liquity/cs-034

c1ebe7a

fix: Remove ForwardBribe contract

fix: Change revert strings for BribeInitiative

0a7eefa

fix: Compute real LQTY received on unstaking

f22ce5c

If you pass any amount higher than your stake, and LQTYStaking will internally truncate it to the maximum withdrawable amount.

Update README.md

7879894

Update README.md

ca90682

Update README.md

90a9266

Update README.md

68b7110

Update README.md

24f7202

Update README.md

8ca30e0

docs: README fixes

6485608

docs: minor README fix

d910db2

Update README - formatting

ba3bcbb

bingen closed this Jun 13, 2025

Conversation

GalloDaSballo commented Nov 24, 2024

Uh oh!

recon-getrecon-xyz bot commented Jan 13, 2025

Recon Job Completed

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Results

Broken Properties

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Uh oh!

recon-getrecon-xyz bot commented Jan 13, 2025

Recon Campaign Started

Uh oh!

recon-getrecon-xyz bot commented Jan 13, 2025

Recon Campaign Started

Uh oh!

recon-getrecon-xyz bot commented Jan 13, 2025

Recon Campaign Started

Uh oh!

recon-getrecon-xyz bot commented Jan 13, 2025

Recon Campaign Started

Uh oh!

recon-getrecon-xyz bot commented Jan 13, 2025

Recon Job Completed

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Results

Broken Properties

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Uh oh!

recon-getrecon-xyz bot commented Jan 13, 2025

Recon Job Completed

Recon Recap for liquity/V2-gov/main

Fuzzer overview

Results

Broken Properties

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Broken property:

Sequence

Uh oh!