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/*"

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

      - name: Setup Python
        uses: actions/setup-python@v4
        with:
          python-version: '3.10'
          cache: 'pip'

      - name: Install Kontrol
        run: |
          python3 -m pip install --upgrade pip
          pip install kontrol

      - 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 Kontrol Verification
        run: |
          # Create results directory
          mkdir -p verification-results
          
          # Run verification for each specification
          for spec in src/test/kontrol/*.k; do
            if [ -f "$spec" ]; then
              echo "Verifying $(basename "$spec")..."
              
              kontrol prove "$spec" \
                --contract-dir ./src/contracts \
                --output-dir ./verification-results \
                --verbose || {
                  echo "Verification failed for $spec"
                  exit 1
                }
            fi
          done
          
          echo "Verification completed successfully!"

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