From 7a77d586e744b7d3f3e08d5c9a28825791ce0521 Mon Sep 17 00:00:00 2001 From: gustavo-grieco Date: Wed, 20 Aug 2025 18:35:31 +0200 Subject: [PATCH] added github action to perform verification on LowGasSafeMathEchidnaTest using echidna --- .../workflows/echidna_core_verification.yaml | 46 +++++++++++++++++++ .../echidna/echidna.verification.config.yml | 12 +++++ 2 files changed, 58 insertions(+) create mode 100644 .github/workflows/echidna_core_verification.yaml create mode 100644 src/core/contracts/test/echidna/echidna.verification.config.yml diff --git a/.github/workflows/echidna_core_verification.yaml b/.github/workflows/echidna_core_verification.yaml new file mode 100644 index 00000000..e69af735 --- /dev/null +++ b/.github/workflows/echidna_core_verification.yaml @@ -0,0 +1,46 @@ +name: Echidna Core Verification + +on: + push: + branches: + - integral-v1.2.2 + pull_request: + branches: + - integral-v1.2.2 + +jobs: + VerificationAsserts: + strategy: + matrix: + testName: + - LowGasSafeMathEchidnaTest + + runs-on: ubuntu-latest + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Use Node.js + uses: actions/setup-node@v3 + with: + node-version: 20 + cache: 'npm' + + - name: Install dependencies + run: npm run ci-install + + - name: Compile contracts + run: npm run compile + working-directory: ./src/core + + - name: Run ${{ matrix.testName }} + uses: crytic/echidna-action@v2 + with: + echidna-version: edge + solc-version: 0.8.20 + files: ./src/core/contracts/test/echidna/${{ matrix.testName }}.sol + contract: ${{ matrix.testName }} + crytic-args: --hardhat-ignore-compile + solc-args: --evm-version paris + config: ./src/core/contracts/test/echidna/echidna.verification.config.yml diff --git a/src/core/contracts/test/echidna/echidna.verification.config.yml b/src/core/contracts/test/echidna/echidna.verification.config.yml new file mode 100644 index 00000000..6ae22cd3 --- /dev/null +++ b/src/core/contracts/test/echidna/echidna.verification.config.yml @@ -0,0 +1,12 @@ +symExec: true +symExecTimeout: 600 +symExecMaxExplore: 100 +symExecMaxIters: 100 + +format: text +testMode: assertion + +maxTimeDelay: 0 +maxBlockDelay: 0 +workers: 0 +seqLen: 1