chore: Update Certora Formal Verification specifications and CI #29
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| on: | |
| # Run when PRs are merged into main and touch relevant code paths | |
| pull_request: | |
| branches: | |
| - main | |
| paths: | |
| - 'src/contracts/**' | |
| - 'script/**' | |
| - 'certora/**' | |
| # Run on any pushes to certora/* branches | |
| push: | |
| branches: | |
| - 'certora/**' | |
| # Biweekly schedule (1st and 15th of each month at midnight UTC) | |
| schedule: | |
| - cron: '0 0 1,15 * *' | |
| # Manual trigger | |
| workflow_dispatch: | |
| jobs: | |
| # Compile the contracts and run verification | |
| compile_and_verify: | |
| name: Compile and verify | |
| # Run if it meets one of these conditions: | |
| # 1. It's a merged PR into main (with matching paths) | |
| # 2. It's a push to a certora/* branch | |
| # 3. It's a scheduled run | |
| # 4. It's a manually triggered run | |
| if: > | |
| (github.event_name == 'pull_request' && | |
| github.event.pull_request.merged == true) || | |
| (github.event_name == 'push' && | |
| startsWith(github.ref, 'refs/heads/certora/')) || | |
| github.event_name == 'schedule' || | |
| github.event_name == 'workflow_dispatch' | |
| runs-on: ubuntu-latest | |
| permissions: | |
| contents: read | |
| statuses: write | |
| pull-requests: write | |
| id-token: write | |
| steps: | |
| - uses: step-security/harden-runner@ec9f2d5744a09debf3a187a3f4f675c53b671911 | |
| with: | |
| egress-policy: audit | |
| # Checkout the repository with submodules | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 | |
| with: | |
| submodules: recursive | |
| # Use Main branch for scheduled runs, otherwise use the branch that triggered the workflow | |
| ref: ${{ github.event_name == 'schedule' && 'main' || github.ref }} | |
| # Apply patches to the code | |
| - name: Patch code | |
| run: ./certora/scripts/patches/patch.sh | |
| # Run Certora compilation and verification | |
| - name: Run Certora compilation and verification | |
| uses: Certora/certora-run-action@11979c68d2ffab0b1b2fe6c72ec9d7a38855822d | |
| with: | |
| # List of configuration files for different contracts to verify | |
| configurations: |- | |
| certora/confs/multichain/CrossChainRegistry.conf | |
| certora/confs/multichain/KeyRegistrar.conf | |
| certora/confs/multichain/OperatorTableUpdater.conf | |
| certora/confs/multichain/ECDSACertificateVerifier.conf | |
| certora/confs/multichain/BN254CertificateVerifier.conf | |
| certora/confs/core/AllocationManager.conf | |
| certora/confs/core/AllocationManagerOverslashing.conf | |
| certora/confs/core/AllocationManagerValidState.conf | |
| certora/confs/core/AllocationManagerSanity.conf | |
| certora/confs/core/DelegationManager.conf | |
| certora/confs/core/DelegationManagerValidState.conf | |
| certora/confs/core/StrategyManager.conf | |
| certora/confs/permissions/Pausable.conf | |
| certora/confs/pods/EigenPodManagerRules.conf | |
| certora/confs/strategies/StrategyBase.conf | |
| solc-versions: 0.8.30 | |
| job-name: "Verified Rules" | |
| certora-key: ${{ secrets.CERTORAKEY }} | |
| env: | |
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} |