ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:
    branches: [main]

env:
  CARGO_TERM_COLOR: always

jobs:
  test:
    name: Test
    runs-on: ubuntu-latest
    env:
      RUSTFLAGS: -Dwarnings
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - name: Cache Cargo dependencies
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            target/
          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: |
            ${{ runner.os }}-cargo-
      - name: Run tests
        run: cargo test --workspace

  clippy:
    name: Clippy
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          components: clippy
      - name: Cache Cargo dependencies
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            target/
          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: |
            ${{ runner.os }}-cargo-
      - name: Run clippy
        run: cargo clippy --workspace --all-targets -- -D warnings

  fmt:
    name: Format
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          components: rustfmt
      - name: Cache Cargo dependencies
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            target/
          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: |
            ${{ runner.os }}-cargo-
      - name: Check formatting
        run: cargo fmt --all -- --check

  verify:
    name: Z3 Verification
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - name: Cache Cargo dependencies
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            target/
          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: |
            ${{ runner.os }}-cargo-
      - name: Install Z3
        run: sudo apt-get update && sudo apt-get install -y libz3-dev
      - name: Run verification tests
        run: cargo test -p synth-verify --features z3-solver,arm
      - name: Run comprehensive verification
        run: cargo test -p synth-verify --test comprehensive_verification --features z3-solver,arm

  coverage:
    name: Code Coverage
    needs: [test]
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@nightly
      - name: Cache Cargo dependencies
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            target/
          key: ${{ runner.os }}-coverage-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: |
            ${{ runner.os }}-coverage-
      - name: Install cargo-llvm-cov
        uses: taiki-e/install-action@v2
        with:
          tool: cargo-llvm-cov
      - name: Generate coverage (LCOV)
        run: |
          cargo llvm-cov --workspace --lcov --output-path lcov.info \
            --exclude synth-verify --exclude synth-qemu \
            --exclude synth-backend-awsm --exclude synth-backend-wasker
      - name: Upload to Codecov
        uses: codecov/codecov-action@v4
        with:
          files: lcov.info
          fail_ci_if_error: false
        env:
          CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}

  kani:
    name: Kani Verification
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install Kani
        run: cargo install --locked kani-verifier && cargo kani setup
      - name: Run Kani proofs
        run: cargo kani -p synth-backend --tests
        timeout-minutes: 30
    continue-on-error: true

  rivet:
    name: Rivet Validation
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - name: Cache Cargo dependencies
        uses: actions/cache@v4
        with:
          path: |
            ~/.cargo/registry
            ~/.cargo/git
            ~/.cargo/bin
            target/
          key: ${{ runner.os }}-rivet-${{ hashFiles('**/Cargo.lock') }}
          restore-keys: |
            ${{ runner.os }}-rivet-
      - name: Install rivet
        run: cargo install --force --git https://github.com/pulseengine/rivet --branch main rivet-cli
      - name: Validate artifacts
        continue-on-error: true
        run: |
          sed -i '/^externals:/,$d' rivet.yaml
          rivet validate
      - name: Check coverage
        run: rivet coverage

  bazel:
    name: Bazel Build & Proofs
    runs-on: ubuntu-latest
    timeout-minutes: 45
    steps:
      - uses: actions/checkout@v4
      - name: Install Nix
        uses: cachix/install-nix-action@v30
        with:
          nix_path: nixpkgs=channel:nixos-unstable
      - name: Setup Bazel
        uses: bazel-contrib/setup-bazel@0.14.0
        with:
          bazelisk-cache: true
          disk-cache: ${{ github.workflow }}
          repository-cache: true
      - name: Build Rust via Bazel
        run: bazel build //crates:synth
      - name: Verify Rocq proofs
        run: bazel test //coq:verify_proofs