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

      # Download and Extract K Framework
      - name: Download K Framework
        env:
          REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }}
        run: |
          echo "Downloading K Framework..."
          curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz

          echo "Validating tarball..."
          file kframework.tar.gz || { echo "Download failed"; exit 1; }

          echo "Extracting K Framework..."
          mkdir -p kframework
          tar -xvzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; }
          ls -l kframework || { echo "Extraction directory not found"; exit 1; }

          echo "Setting up K Framework..."
          export PATH=$PATH:$(pwd)/kframework/bin

      # Download and Build KEVM
      - name: Install KEVM
        env:
            REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }}
        run: |
          echo "Downloading KEVM..."
          curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz
          
          echo "Extracting KEVM..."
          mkdir -p evm
          tar -xvzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; }
          ls -l evm || { echo "EVM directory not found"; exit 1; }
          
          echo "Building KEVM..."
          cd evm
          export PATH=$PATH:$(pwd)/bin

          echo "Listing KEVM directory contents..."

          if [ -f Makefile ]; then
            make help || make -pRrq : 2>/dev/null | grep -E '^[a-zA-Z_-]+:'
          else
            echo "No Makefile found in the evm directory."
            exit 1
          fi
          make deps
          make build

      # Run the Formal Verification Job
      - name: Formal Verification with KEVM
        run: |
          echo "Running formal verification..."
          cd evm
          krun verification.k || { echo "Formal verification failed"; exit 1; }