ci.yaml

name: CI

on: [push]

jobs:
  foundry-test:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
        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@v4
        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 "Extracting K Framework..."
          mkdir -p kframework
          tar -xzf kframework.tar.gz -C kframework --strip-components=1

          echo "Adding K to PATH..."
          echo "$PWD/kframework/k-distribution/target/release/k/bin" >> $GITHUB_PATH

      - name: Install Dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y curl gcc git g++ cmake maven openjdk-11-jdk flex z3 libz3-dev libsecp256k1-dev

      - name: Install Kontrol with KUP
        env:
          REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }}
        run: |
          # Set up kup with authentication
          echo "Installing kup..."
          curl -H "Authorization: token $REPOSITORY_TOKEN" -sSL https://kframework.org/install | bash
          
          echo "Adding kup to PATH..."
          export PATH=$PATH:$HOME/.kup/bin
          echo "$HOME/.kup/bin" >> $GITHUB_PATH
          
          echo "Installing Kontrol..."
          GITHUB_TOKEN=$REPOSITORY_TOKEN kup install kontrol
          
          echo "Verifying Kontrol installation..."
          kontrol --version || { echo "Kontrol installation failed"; exit 1; }

      - name: Install Foundry
        uses: foundry-rs/foundry-toolchain@v1
        with:
          version: nightly

      - name: Build Contracts
        run: |
          forge build --build-info --force
          ls -la out/

      - name: Run Formal Verification with Kontrol
        run: |
          mkdir -p verification-results
          verified_count=0
          
          for spec in src/test/kontrol/*.k; do
            if [ -f "$spec" ]; then
              echo "Verifying $(basename "$spec")..."
              
              if kontrol prove "$spec" \
                 --contract-dir ./src/contracts \
                 --output-dir ./verification-results \
                 --verbose; then
                echo "✓ Verification successful for $spec"
                ((verified_count++))
              else
                echo "✗ Verification failed for $spec"
                cat "./verification-results/$(basename "$spec" .k).out" 2>/dev/null || echo "No output file found"
                exit 1
              fi
            fi
          done
          
          if [ $verified_count -eq 0 ]; then
            echo "No specification files found to verify"
            exit 1
          else
            echo "Successfully verified $verified_count specification(s)"
          fi

      - name: Upload Verification Results
        if: always()
        uses: actions/upload-artifact@v3
        with:
          name: kontrol-verification-results
          path: verification-results/
          retention-days: 5