From c4d5c50700718c55dd029190ee5cfc988f0016c5 Mon Sep 17 00:00:00 2001 From: Gadi Auerbach Date: Tue, 5 Dec 2023 18:31:53 +0200 Subject: [PATCH 1/3] split tasks in CI --- .github/workflows/certora-review-voting-chain.yml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/.github/workflows/certora-review-voting-chain.yml b/.github/workflows/certora-review-voting-chain.yml index ba6caa5..0442f89 100644 --- a/.github/workflows/certora-review-voting-chain.yml +++ b/.github/workflows/certora-review-voting-chain.yml @@ -66,4 +66,13 @@ jobs: - verifyProposal_states.conf --rule proposalIdIsImmutable proposalHasNonzeroDuration proposalTimeStateTransitionCompliance proposalLegalStates method_reachability - verifyVoting_and_tally.conf --rule voteUpdatesTally - verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteSingleProofAsRepresentative_and_submitVote - - verifyVoting_and_tally.conf --rule voteTallyChangedOnlyByVoting onlyVoteCanChangeResult votingTallyCanOnlyIncrease strangerVoteUnchanged otherProposalUnchanged otherVoterUntouched cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote method_reachability + - verifyVoting_and_tally.conf --rule onlyVoteCanChangeResult + - verifyVoting_and_tally.conf --rule voteTallyChangedOnlyByVoting + - verifyVoting_and_tally.conf --rule votingTallyCanOnlyIncrease + - verifyVoting_and_tally.conf --rule strangerVoteUnchanged + - verifyVoting_and_tally.conf --rule strangerVoteUnchanged + - verifyVoting_and_tally.conf --rule otherProposalUnchanged + - verifyVoting_and_tally.conf --rule otherVoterUntouched + - verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVote_and_submitVoteAsRepresentative + - verifyVoting_and_tally.conf --rule cannot_vote_twice_with_submitVoteAsRepresentative_and_submitVote + - verifyVoting_and_tally.conf --rule method_reachability \ No newline at end of file From 88b3d2985b679c486ed01bf9b32362e60ea47c51 Mon Sep 17 00:00:00 2001 From: Gadi Auerbach Date: Tue, 5 Dec 2023 19:19:26 +0200 Subject: [PATCH 2/3] remove a duplicate task --- .github/workflows/certora-review-voting-chain.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/certora-review-voting-chain.yml b/.github/workflows/certora-review-voting-chain.yml index 0442f89..7bb61a8 100644 --- a/.github/workflows/certora-review-voting-chain.yml +++ b/.github/workflows/certora-review-voting-chain.yml @@ -69,7 +69,6 @@ jobs: - verifyVoting_and_tally.conf --rule onlyVoteCanChangeResult - verifyVoting_and_tally.conf --rule voteTallyChangedOnlyByVoting - verifyVoting_and_tally.conf --rule votingTallyCanOnlyIncrease - - verifyVoting_and_tally.conf --rule strangerVoteUnchanged - verifyVoting_and_tally.conf --rule strangerVoteUnchanged - verifyVoting_and_tally.conf --rule otherProposalUnchanged - verifyVoting_and_tally.conf --rule otherVoterUntouched From 29e09015c1b62271d36aeca875f0146dc2460981 Mon Sep 17 00:00:00 2001 From: Gadi Auerbach Date: Wed, 6 Dec 2023 10:53:34 +0200 Subject: [PATCH 3/3] split rules of verifyPower_summary --- .github/workflows/certora-review-voting-chain.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/certora-review-voting-chain.yml b/.github/workflows/certora-review-voting-chain.yml index 7bb61a8..b0dd432 100644 --- a/.github/workflows/certora-review-voting-chain.yml +++ b/.github/workflows/certora-review-voting-chain.yml @@ -54,7 +54,8 @@ jobs: - verifyLegality.conf --rule legalVote - verifyLegality.conf --rule votedPowerIsImmutable method_reachability - verifyMisc.conf - - verifyPower_summary.conf + - verifyPower_summary.conf --rule onlyThreeTokens + - verifyPower_summary.conf --rule method_reachability - verifyProposal_config.conf --rule createdProposalHasRoots - verifyProposal_config.conf --rule startedProposalHasConfig - verifyProposal_config.conf --rule proposalHasNonzeroDuration configIsImmutable newProposalUnusedId method_reachability