ci.yml

name: Format and Verify VOSTD (Main)

on:
  push:
    branches:
      - main
  pull_request:
    branches:
      - main
  workflow_dispatch:
    inputs:
      branch:
        description: "Branch to run the workflow on"
        required: true
        default: "main"

jobs:
  format-and-verify:
    runs-on: ubuntu-24.04
    env:
      CARGO_TERM_COLOR: always
      VERUS_REPOSITORY: https://github.com/asterinas/verus.git
      VERUS_BASE_COMMIT: bb61343fc97e4b3a97b1029f385ffb6bbb291da2
      VERUS_IRC11_PATCH: tools/patches/verus-irc11.patch
      VERUS_PATCH: tools/patches/verus-irc11-vstd.patch

    steps:
      - name: Checkout repository
        uses: actions/checkout@v7
        with:
          submodules: recursive

      - name: Install dependencies
        run: |
          sudo apt update -qq
          sudo apt install -y build-essential unzip pkg-config libssl-dev llvm

      - name: Get Rust toolchain version
        id: rust-toolchain
        run: |
          RUST_VERSION=$(grep 'channel' rust-toolchain.toml | sed -E 's/.*= *"(.*)"/\1/')
          if [ -z "$RUST_VERSION" ]; then
            echo "Failed to extract Rust version from rust-toolchain.toml"
            exit 1
          fi
          echo "RUST_VERSION=$RUST_VERSION" >> "$GITHUB_ENV"
          echo "Rust version: $RUST_VERSION"

      - name: Cache Rust toolchain
        uses: actions/cache@v6
        with:
          path: |
            ~/.rustup/toolchains
            ~/.rustup/update-hashes
            ~/.rustup/tmp
          key: ${{ runner.os }}-rust-toolchain-${{ env.RUST_VERSION }}

      - name: Cache Cargo dependencies
        uses: actions/cache@v6
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: |
            ${{ runner.os }}-cargo-

      - name: Record toolchain revisions
        id: verus
        run: |
          echo "Using pinned Asterinas Verus base: $VERUS_BASE_COMMIT"
          DV_COMMIT=$(git rev-parse HEAD:dv)
          echo "DV_COMMIT=$DV_COMMIT" >> "$GITHUB_ENV"
          echo "Using dv commit: $DV_COMMIT"

      - name: Cache dv build artifacts
        uses: actions/cache@v6
        with:
          path: dv/target
          key: ${{ runner.os }}-dv-${{ env.DV_COMMIT }}

      - name: Cache Verus
        id: cache-verus
        uses: actions/cache@v6
        with:
          path: tools/verus
          key: ${{ runner.os }}-verus-irc11-weak-memory-${{ env.VERUS_BASE_COMMIT }}-${{ hashFiles('tools/bootstrap-verus-irc11.sh', 'tools/patches/verus-irc11.patch', 'tools/patches/verus-irc11-vstd.patch') }}

      - name: Cache verusfmt
        id: cache-verusfmt
        uses: actions/cache@v6
        with:
          path: ~/.cargo/bin/verusfmt
          key: ${{ runner.os }}-verusfmt-${{ env.VERUS_BASE_COMMIT }}

      - name: Bootstrap Verus (if needed)
        run: |
          if [ "${{ steps.cache-verus.outputs.cache-hit }}" = "true" ]; then
            echo "Using cached Verus"
          else
            echo "Cache miss, bootstrapping rebased Verus IRC11..."
            rm -rf tools/verus
            git init tools/verus
            git -C tools/verus remote add origin "$VERUS_REPOSITORY"
            git -C tools/verus fetch --depth=1 origin "$VERUS_BASE_COMMIT"
            git -C tools/verus checkout --detach FETCH_HEAD
            git -C tools/verus apply "$GITHUB_WORKSPACE/$VERUS_IRC11_PATCH"
            git -C tools/verus apply --reverse --check "$GITHUB_WORKSPACE/$VERUS_IRC11_PATCH"
            bash tools/bootstrap-verus-irc11.sh
          fi

          if ! command -v verusfmt >/dev/null 2>&1; then
            echo "verusfmt not found, installing..."
            curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/latest/download/verusfmt-installer.sh | sh
          fi
          test "$(git -C tools/verus rev-parse HEAD)" = "$VERUS_BASE_COMMIT"
          test -f tools/verus/source/vstd/atomic_weak.rs
          test -f tools/verus/source/vstd/thread_view.rs
          verusfmt --version

      - name: Enable IRC11 alongside existing SC atomics
        run: |
          if git -C tools/verus apply --reverse --check "$GITHUB_WORKSPACE/$VERUS_PATCH"; then
            echo "IRC11 compatibility patch is already applied"
          else
            git -C tools/verus apply "$GITHUB_WORKSPACE/$VERUS_PATCH"
          fi

      - name: Run verification
        run: |
          set -o pipefail
          if ! make 2>&1 | tee verify_output.txt; then
            echo "❌ Verification failed"
            echo "VERIFY_FAILED=1" >> "$GITHUB_ENV"
            exit 1
          else
            echo "✅ Verification passed!"
          fi

      - name: Check for verification warnings
        if: always()
        run: |
          WARNINGS=(
            "note: automatically chose triggers for this expression:|auto-trigger notes"
            "warning: use of deprecated method \`vstd::set::Set::<A>::finite\`|deprecated Set::finite()"
            "warning: use of deprecated associated function \`vstd::set::Set::<A>::new_assuming_finite\`|deprecated Set::new_assuming_finite()"
          )

          FAILED=0
          for ITEM in "${WARNINGS[@]}"; do
            PATTERN="${ITEM%%|*}"
            LABEL="${ITEM##*|}"
            if grep -q "$PATTERN" verify_output.txt 2>/dev/null; then
              echo "❌ Found $LABEL"
              grep -n "$PATTERN" verify_output.txt
              FAILED=1
            else
              echo "✅ No $LABEL found"
            fi
          done

          if [[ "$FAILED" == "1" ]]; then
            echo "VERIFY_WARNINGS_FOUND=1" >> "$GITHUB_ENV"
            exit 1
          fi

      - name: Run format
        if: always()
        run: make fmt

      - name: Check for formatting changes
        if: always()
        run: |
          if [[ -n $(git status --porcelain) ]]; then
            echo "Code is not properly formatted. Run 'make fmt'."
            git diff
            echo "FMT_FAILED=1" >> "$GITHUB_ENV"
            exit 1
          fi

      - name: Publish summary
        if: always()
        run: |
          {
            echo "# CI Summary"
            if [[ "${FMT_FAILED:-0}" == "1" ]]; then
              echo "- Formatting: ❌ failed"
            else
              echo "- Formatting: ✅ passed"
            fi
            if [[ "${VERIFY_FAILED:-0}" == "1" ]]; then
              echo "- Verification: ❌ failed"
            else
              echo "- Verification: ✅ passed"
            fi
            if [[ "${VERIFY_WARNINGS_FOUND:-0}" == "1" ]]; then
              echo "- Verification warnings: ❌ found"
            else
              echo "- Verification warnings: ✅ none"
            fi
          } >> "$GITHUB_STEP_SUMMARY"