ci.yaml

name: CI
on: [push]

jobs:
  foundry-test:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@master
        with:
          fetch-depth: 0
          submodules: recursive
      - uses: foundry-rs/foundry-toolchain@v1
        with:
          version: nightly
      - name: Install forge-std
        run: |
          forge install foundry-rs/forge-std --no-commit
          forge remappings > remappings.txt
      - name: Run non-Kontrol tests
        run: |
          forge test --no-match-path "src/test/kontrol/*" -vvv
      - name: Run snapshot without Kontrol tests
        run: forge snapshot --no-match-path "src/test/kontrol/*"

  formal-verification:
    runs-on: ubuntu-latest
    needs: foundry-test
    steps:
      - uses: actions/checkout@master
        with:
          fetch-depth: 0
          submodules: recursive

      # Install dependencies for K Framework
      - name: Install K Framework
        run: |
          curl -LO kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz
          tar -xvzf kframework
          cd kframework
          export PATH=$PATH:$(pwd)/bin
      # Verify KEVM setup
      - name: Install KEVM
        run: |
          curl -LO https://github.com/runtimeverification/evm-semantics/releases/download/v1.0/evm.tar.gz
          tar -xvzf evm.tar.gz
          cd evm
          export PATH=$PATH:$(pwd)/bin
          make deps  # Install KEVM dependencies
          make build # Build KEVM

      # Run the formal verification job
      - name: Formal Verification with KEVM
        run: |
          cd evm
          # Assuming `verification.k` exists and contains the formal specification
          krun verification.k