vault-bridge/.github/workflows/certora.yml.outdated at d863a967b3f4028ec0fbd6ca2684acaebed3f495 · agglayer/vault-bridge · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
name: Certora - Verification

on:
  pull_request:
    branches:
      - staging

env:
  FOUNDRY_PROFILE: ci
  CONFIGS: |
    certora/confs/GenericVaultBridgeToken.conf
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_invariants.spec --rule netCollectedYieldAccounted --rule netCollectedYieldLimited
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_invariants.spec --rule minimumReservePercentageLimit --rule reserveBacked
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_invariants.spec --rule vaultBridgeTokenSolvency --rule vaultBridgeTokenSolvency_simple
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_invariants.spec --rule assetsMoreThanSupply --rule noSupplyIfNoAssets
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_invariants.spec --rule zeroAllowanceOnAssets --rule zeroAllowanceOnShares
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_allowedChanges.spec
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_integrity.spec
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/GVBTBalances.spec
    certora/confs/GenericVaultBridgeToken.conf --verify GenericVaultBridgeToken:certora/specs/tokenMockBalances.spec
    certora/confs/GenericNativeConverter.conf
    certora/confs/base/MigrationManager.conf --rule onMsgReceived_doesntAlwaysRevert
jobs:
  check:
    runs-on: ubuntu-latest
    permissions:
      contents: read
      statuses: write
      pull-requests: write
      id-token: write
    steps:
      - name: checkout repository
        uses: actions/checkout@v4
        with:
          submodules: recursive

      - name: install foundry
        uses: foundry-rs/foundry-toolchain@v1

      - name: install bun
        uses: oven-sh/setup-bun@v2

      - name: bun install
        run: |
          forge soldeer install
          bun install || true

      - name: setup bridge repo
        run: |
          git clone https://github.com/0xPolygonHermez/zkevm-contracts.git
          cd zkevm-contracts/
          git checkout v10.1.0-rc.1
          npm install

      - name: Certora munge
        run: ./certora/scripts/munge.sh

      - name: run configs
        uses: Certora/certora-run-action@v2
        with:
          cli-release: beta
          configurations: ${{ env.CONFIGS }}
          solc-versions: 0.8.28 0.8.29
          solc-remove-version-prefix: "0."
          job-name: "Verified Rules"
          certora-key: ${{ secrets.CERTORAKEY }}
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}