Add certora prover to GitHub workflows

.github/workflows/certora-prover.yml

@@ -0,0 +1,64 @@
+name: Certora Prover
+
+on:
+  push:
+    branches:
+      - master
+      - release-v*
+      - formal-verification
+      - add-certora-prover-to-github-workflows
+  pull_request: {}
+  workflow_dispatch: {}
+
+jobs:
+  list-scripts:
+    runs-on: ubuntu-latest
+    outputs:
+      matrix: ${{ steps.set-matrix.outputs.matrix }}
+    steps:
+      - uses: actions/checkout@v2
+      - id: set-matrix
+        run: echo ::set-output name=matrix::$(ls certora/scripts/{,**}/*.sh | grep -v '\WnoCI\W' | jq -Rsc 'split("\n")[:-1]')
+  verify:
+    runs-on: ubuntu-latest
+    needs: list-scripts
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+      - name: Install forge dependencies
+        run: forge install
+      - name: Install python
+        uses: actions/setup-python@v2
+        with:
+          python-version: '3.10'
+          cache: 'pip'
+      - name: Install java
+        uses: actions/setup-java@v1
+        with:
+          java-version: '11'
+          java-package: 'jre'
+      - name: Install certora
+        run: pip install certora-cli
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.12/solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+          chmod +x /usr/local/bin/solc
+      - name: Verify rule ${{ matrix.params }}
+        run: |
+          touch certora/applyHarness.patch
+          make -C certora munged
+          bash ${{ matrix.params }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 4
+      matrix:
+        params: ${{ fromJson(needs.list-scripts.outputs.matrix) }}

certora/scripts/core/verifyDelegationManager.sh

@@ -3,7 +3,6 @@ then
     RULE="--rule $2"
 fi
 
-solc-select use 0.8.12
 
 certoraRun certora/harnesses/DelegationManagerHarness.sol \
     lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol lib/openzeppelin-contracts/contracts/mocks/ERC1271WalletMock.sol \

certora/scripts/libraries/verifyStructuredLinkedList.sh

@@ -3,7 +3,6 @@ then
     RULE="--rule $2"
 fi
 
-solc-select use 0.8.12
 
 certoraRun certora/harnesses/StructuredLinkedListHarness.sol \
     --verify StructuredLinkedListHarness:certora/specs/libraries/StructuredLinkedList.spec \
@@ -12,6 +11,5 @@ certoraRun certora/harnesses/StructuredLinkedListHarness.sol \
     --settings -optimisticFallback=true \
     $RULE \
     --rule_sanity \
-    # --staging master \
     --loop_iter 3 \
     --msg "StructuredLinkedList $1 $2" \

certora/scripts/permissions/verifyPausable.sh

@@ -3,7 +3,6 @@ then
     RULE="--rule $2"
 fi
 
-solc-select use 0.8.12
 
 certoraRun certora/harnesses/PausableHarness.sol \
     certora/munged/permissions/PauserRegistry.sol \

certora/scripts/strategies/verifyStrategyBase.sh

@@ -3,7 +3,6 @@ then
     RULE="--rule $2"
 fi
 
-solc-select use 0.8.12
 
 certoraRun certora/munged/strategies/StrategyBase.sol \
     lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol \

requirements.txt

@@ -0,0 +1 @@
+certora-cli==3.6.4

src/test/Delegation.t.sol

@@ -430,8 +430,7 @@ contract DelegationTests is EigenLayerTestHelper {
     }
 
     /// @notice This function checks that you can only delegate to an address that is already registered.
-    function testDelegateToInvalidOperator(address _staker, address _unregisteredOperator) public{
-
+    function testDelegateToInvalidOperator(address _staker, address _unregisteredOperator) public fuzzedAddress(_staker) {
         vm.startPrank(_staker);
         cheats.expectRevert(bytes("DelegationManager._delegate: operator has not yet registered as a delegate"));
         delegation.delegateTo(_unregisteredOperator);