Merge pull request bgd-labs#37 from bgd-labs/fix/fix-ci

fix: removed unused paths from certora ci
Certora · Nov 26, 2024 · 70865bf · 70865bf
2 parents 43fd72b + 7a10ada
commit 70865bf
Show file tree

Hide file tree

Showing 11 changed files with 75 additions and 29 deletions.
diff --git a/.github/workflows/comment.yml b/.github/workflows/comment.yml
@@ -0,0 +1,20 @@
+name: PR Comment
+
+on:
+  workflow_run:
+    workflows: [Test]
+    types:
+      - completed
+
+permissions:
+  actions: read
+  issues: write
+  checks: read
+  statuses: read
+  pull-requests: write
+
+jobs:
+  comment:
+    uses: bgd-labs/github-workflows/.github/workflows/comment.yml@main
+    secrets:
+      READ_ONLY_PAT: ${{ secrets.READ_ONLY_PAT }}
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -0,0 +1,48 @@
+name: Test
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  test:
+    name: Foundry build n test
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - uses: bgd-labs/action-rpc-env@main
+        with:
+          ALCHEMY_API_KEY: ${{ secrets.ALCHEMY_API_KEY }}
+
+      # we simply use foundry zk for all jobs in this repo
+      - name: Run Foundry setup
+        uses: bgd-labs/github-workflows/.github/actions/foundry-setup@main
+
+      - name: Run Forge tests
+        id: test
+        uses: bgd-labs/github-workflows/.github/actions/foundry-test@main
+
+      - name: Run Gas report
+        uses: bgd-labs/github-workflows/.github/actions/foundry-gas-report@main
+
+      - name: Run Lcov report
+        uses: bgd-labs/github-workflows/.github/actions/foundry-lcov-report@main
+
+      - name: Run Forge tests
+        uses: bgd-labs/github-workflows/.github/actions/comment-artifact@main
+
+      # we let failing tests pass so we can log them in the comment, still we want the ci to fail
+      - name: Post test
+        if: ${{ steps.test.outputs.testStatus != 0 }}
+        run: |
+          echo "tests failed"
+          exit 1
diff --git a/security/certora/confs/verifyVotingStrategy_unittests.conf b/security/certora/confs/verifyVotingStrategy_unittests.conf
@@ -13,9 +13,7 @@
         "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
         "aave-token-v3=lib/aave-token-v3/src",
         "forge-std=lib/forge-std/src",
-        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
         "openzeppelin-contracts=lib/aave-delivery-infrastructure/lib/openzeppelin-contracts",
-        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "VotingStrategy:security/certora/specs/VotingStrategy_unittests.spec",
@@ -24,4 +22,3 @@
     "solc": "solc8.19",
     "msg": "VotingStrategy tests"
 }
-
diff --git a/security/certora/confs/voting/verifyLegality.conf b/security/certora/confs/voting/verifyLegality.conf
@@ -20,9 +20,7 @@
         "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
         "aave-token-v3=lib/aave-token-v3/src",
         "forge-std=lib/forge-std/src",
-        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
         "openzeppelin-contracts=lib/openzeppelin-contracts",
-        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "VotingMachineHarness:security/certora/specs/voting/legality.spec",

diff --git a/security/certora/confs/voting/verifyMisc.conf b/security/certora/confs/voting/verifyMisc.conf
@@ -20,9 +20,7 @@
         "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
         "aave-token-v3=lib/aave-token-v3/src",
         "forge-std=lib/forge-std/src",
-        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
         "openzeppelin-contracts=lib/openzeppelin-contracts",
-        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "VotingMachineHarnessTriple:security/certora/specs/voting/misc.spec",

diff --git a/security/certora/confs/voting/verifyPower_summary.conf b/security/certora/confs/voting/verifyPower_summary.conf
@@ -20,9 +20,7 @@
         "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
         "aave-token-v3=lib/aave-token-v3/src",
         "forge-std=lib/forge-std/src",
-        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
         "openzeppelin-contracts=lib/openzeppelin-contracts",
-        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "VotingMachineHarnessTriple:security/certora/specs/voting/power_summary.spec",

diff --git a/security/certora/confs/voting/verifyProposal_config.conf b/security/certora/confs/voting/verifyProposal_config.conf
@@ -20,9 +20,7 @@
         "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
         "aave-token-v3=lib/aave-token-v3/src",
         "forge-std=lib/forge-std/src",
-        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
         "openzeppelin-contracts=lib/openzeppelin-contracts",
-        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "VotingMachineHarness:security/certora/specs/voting/proposal_config.spec",

diff --git a/security/certora/confs/voting/verifyProposal_states.conf b/security/certora/confs/voting/verifyProposal_states.conf
@@ -20,9 +20,7 @@
         "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
         "aave-token-v3=lib/aave-token-v3/src",
         "forge-std=lib/forge-std/src",
-        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
         "openzeppelin-contracts=lib/openzeppelin-contracts",
-        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "VotingMachineHarness:security/certora/specs/voting/proposal_states.spec",

diff --git a/security/certora/confs/voting/verifyVoting_and_tally.conf b/security/certora/confs/voting/verifyVoting_and_tally.conf
@@ -20,9 +20,7 @@
         "aave-token-v2=lib/aave-token-v3/lib/aave-token-v2/contracts",
         "aave-token-v3=lib/aave-token-v3/src",
         "forge-std=lib/forge-std/src",
-        "hyperlane-monorepo=lib/aave-delivery-infrastructure/lib/hyperlane-monorepo/solidity",
         "openzeppelin-contracts=lib/openzeppelin-contracts",
-        "solidity-examples=lib/aave-delivery-infrastructure/lib/solidity-examples/contracts",
         "solidity-utils=lib/solidity-utils/src"
     ],
     "verify": "VotingMachineHarness:security/certora/specs/voting/voting_and_tally.spec",

diff --git a/security/certora/specs/Governance.spec b/security/certora/specs/Governance.spec
@@ -100,6 +100,9 @@ definition state_changing_function(method f) returns bool =
 definition initializeSig(method f) returns bool = 
             f.selector == sig:initialize(address,address,address, IGovernanceCore.SetVotingConfigInput[],address[],uint256,uint256).selector;
 
+definition initializeWithRevisionSig(method f) returns bool = 
+            f.selector == sig:initializeWithRevision(uint256).selector;
+
 definition isTerminalState(IGovernanceCore.State state) returns bool = 
             state == IGovernanceCore.State.Executed ||      // 4
             state == IGovernanceCore.State.Failed ||        // 5
@@ -459,7 +462,7 @@ rule single_state_transition_per_block_non_creator_witness
 // A unauthorized user (not an owner) cannot change voting parameters
 rule only_owner_can_set_voting_config(method f) filtered {
    f -> !f.isView &&
-   !initializeSig(f) }
+     !initializeSig(f) && !initializeWithRevisionSig(f)}
 {
   env e;
   calldataarg args;
@@ -535,7 +538,9 @@ rule guardian_can_cancel()
 // Only a guardian, an owner can cancel any proposal, a creator can cancel his own proposal 
 rule only_guardian_can_cancel(method f)filtered 
 { f -> !f.isView  && 
-  !initializeSig(f)
+    !initializeSig(f)
+    && !initializeWithRevisionSig(f) // this function can change the _votingConfigs[proposal.accessLevel].minPropositionPower
+                                     // thus invalidates the _isPropositionPowerEnough(...)
   }
 {
   env e1;