echidna.yml

name: Run Echidna tests

on:
  push:
    paths:
      - ".github/workflows/echidna.yml"
      - "program-analysis/echidna/**/*.sol"
      - "program-analysis/echidna/**/*.yml"
    branches:
      - master
  pull_request:
    paths:
      - ".github/workflows/echidna.yml"
      - "program-analysis/echidna/**/*.sol"
      - "program-analysis/echidna/**/*.yml"
  schedule:
    # run CI every day even if no PRs/merges occur
    - cron: "0 12 * * *"

jobs:
  tests:
    name: ${{ matrix.name }}
    continue-on-error: ${{ matrix.flaky == true }}
    runs-on: ubuntu-22.04
    strategy:
      fail-fast: false
      matrix:
        include:
          - name: Exercise 1
            workdir: program-analysis/echidna/exercises/exercise1/
            files: solution.sol
            contract: TestToken
            outcome: failure
            expected: 'echidna_test_balance:\s*failed'
          - name: Exercise 2
            workdir: program-analysis/echidna/exercises/exercise2/
            files: solution.sol
            contract: TestToken
            outcome: failure
            expected: 'echidna_no_transfer:\s*failed'
          - name: Exercise 3
            workdir: program-analysis/echidna/exercises/exercise3/
            files: solution.sol
            contract: TestToken
            outcome: failure
            expected: 'echidna_test_balance:\s*failed'
          - name: Exercise 4
            workdir: program-analysis/echidna/exercises/exercise4/
            files: solution.sol
            config: config.yaml
            contract: TestToken
            outcome: failure
            expected: 'transfer(address,uint256):\s*failed'
          - name: Exercise 5
            workdir: dvdefi/
            files: .
            config: naivereceiver.yaml
            crytic-args: --hardhat-ignore-compile
            contract: NaiveReceiverEchidna
            outcome: failure
            expected: 'echidna_test_contract_balance:\s*failed'
          - name: Exercise 6
            workdir: dvdefi/
            files: .
            config: unstoppable.yaml
            crytic-args: --hardhat-ignore-compile
            contract: UnstoppableEchidna
            outcome: failure
            expected: 'echidna_testFlashLoan:\s*failed'
          - name: Exercise 7
            workdir: dvdefi/
            files: .
            config: sideentrance.yaml
            crytic-args: --hardhat-ignore-compile
            contract: SideEntranceEchidna
            outcome: failure
            expected: 'testPoolBalance():\s*failed'
          - name: TestToken
            workdir: program-analysis/echidna/example/
            files: testtoken.sol
            contract: TestToken
            outcome: failure
            expected: 'echidna_balance_under_1000:\s*failed'
          - name: Gas estimation
            workdir: program-analysis/echidna/example/
            files: gas.sol
            config: gas.yaml
            outcome: success
            expected: "f(42,123,"
            flaky: true
          - name: Multi
            workdir: program-analysis/echidna/example/
            files: multi.sol
            config: filter.yaml
            outcome: failure
            expected: 'echidna_state4:\s*failed'
          - name: Assert
            workdir: program-analysis/echidna/example/
            files: assert.sol
            config: assert.yaml
            outcome: failure
            expected: 'inc(uint256):\s*failed'
          - name: PopsicleBroken
            workdir: program-analysis/echidna/example/
            files: PopsicleBroken.sol
            solc-version: 0.8.4
            config: Popsicle.yaml
            contract: PopsicleBroken
            outcome: failure
            expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*failed'
          - name: PopsicleFixed
            workdir: program-analysis/echidna/example/
            files: PopsicleFixed.sol
            solc-version: 0.8.4
            config: Popsicle.yaml
            contract: PopsicleFixed
            outcome: success
            expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*passing'
          - name: TestDepositWithPermit
            workdir: program-analysis/echidna/example/
            files: TestDepositWithPermit.sol
            solc-version: 0.8.0
            config: testdeposit.yaml
            contract: TestDepositWithPermit
            outcome: success
            expected: 'testERC20PermitDeposit(uint256):\s*passing'
          - name: MultiABI
            workdir: program-analysis/echidna/example/
            files: allContracts.sol
            solc-version: 0.8.0
            config: allContracts.yaml
            contract: EchidnaTest
            outcome: failure
            expected: 'test_flag_is_false():\s*failed'

    steps:
      - name: Checkout repository
        uses: actions/checkout@v4

      - name: Checkout Damn Vulnerable DeFi solutions
        uses: actions/checkout@v4
        if: startsWith(matrix.workdir, 'dvdefi')
        with:
          repository: crytic/damn-vulnerable-defi-echidna
          ref: solutions
          path: ${{ matrix.workdir }}

      - name: Set up Nodejs
        uses: actions/setup-node@v3
        if: startsWith(matrix.workdir, 'dvdefi')
        with:
          node-version: 16

      - name: Install dependencies and compile
        if: startsWith(matrix.workdir, 'dvdefi')
        run: |
          yarn install --frozen-lockfile
          npx hardhat compile --force
        working-directory: ${{ matrix.workdir }}

      - name: Run Echidna
        uses: crytic/echidna-action@v2
        id: echidna
        continue-on-error: true
        with:
          files: ${{ matrix.files }}
          contract: ${{ matrix.contract }}
          config: ${{ matrix.config }}
          output-file: ${{ matrix.files }}.out
          solc-version: ${{ matrix.solc-version || '0.8.0' }}
          echidna-workdir: ${{ matrix.workdir }}
          echidna-version: edge
          crytic-args: ${{ matrix.crytic-args || '' }}

      - name: Verify that the exit code is correct
        run: |
          if [[ ${{ steps.echidna.outcome }} = ${{ matrix.outcome }} ]]; then
            echo "Outcome matches"
          else
            echo "Outcome mismatch. Expected ${{ matrix.outcome }} but got ${{ steps.echidna.outcome }}"
            exit 1
          fi

      - name: Verify that the output is correct
        run: |
          if grep -q "${{ matrix.expected }}" "${{ steps.echidna.outputs.output-file }}"; then
            echo "Output matches"
          else
            echo "Output mismatch. Expected something matching '${{ matrix.expected }}'. Got the following:"
            cat "${{ steps.echidna.outputs.output-file }}"
            exit 1
          fi