ci.yml

# AxonOS Kernels — Continuous Integration
#
# Every job has an explicit timeout so a hanging tool cannot block the
# entire pipeline. Kani jobs run with `continue-on-error: true` so that a
# slow or hung BMC proof does not turn the whole CI red — they report
# their status independently and are inspected manually after every push.

name: ci

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

env:
  CARGO_TERM_COLOR: always
  RUST_BACKTRACE: 1

# Cancel in-flight runs on the same branch when a new push arrives.
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:

  # ── 1. Tests across three host operating systems ─────────────────────────
  test:
    name: test (${{ matrix.os }})
    runs-on: ${{ matrix.os }}
    timeout-minutes: 15
    strategy:
      fail-fast: false
      matrix:
        os: [ubuntu-latest, macos-latest, windows-latest]
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - uses: Swatinem/rust-cache@v2
      - name: cargo test --workspace
        run: cargo test --workspace --all-features

  # ── 2. Format check ───────────────────────────────────────────────────────
  fmt:
    name: rustfmt --check
    runs-on: ubuntu-latest
    timeout-minutes: 5
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          components: rustfmt
      - run: cargo fmt --all -- --check

  # ── 3. Clippy ─────────────────────────────────────────────────────────────
  clippy:
    name: clippy -D warnings
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          components: clippy
      - uses: Swatinem/rust-cache@v2
      - run: cargo clippy --workspace --all-targets --all-features -- -D warnings

  # ── 4. MSRV pin ───────────────────────────────────────────────────────────
  msrv:
    name: MSRV (1.75)
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@1.75
      - uses: Swatinem/rust-cache@v2
      - run: cargo check --workspace --all-features

  # ── 5. no_std builds on embedded targets ─────────────────────────────────
  no-std:
    name: no_std (${{ matrix.target }})
    runs-on: ubuntu-latest
    timeout-minutes: 15
    strategy:
      fail-fast: false
      matrix:
        target:
          - thumbv7em-none-eabihf
          - thumbv8m.main-none-eabihf
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          targets: ${{ matrix.target }}
      - uses: Swatinem/rust-cache@v2
      - name: cargo build --target ${{ matrix.target }}
        # Exclude firmware (it builds separately in its own job).
        run: |
          cargo build --release --target ${{ matrix.target }} \
            -p axonos-spsc \
            -p axonos-scheduler \
            -p axonos-capability \
            -p axonos-time \
            -p axonos-intent \
            -p axonos-kernel-core

  # ── 6. Documentation build ───────────────────────────────────────────────
  docs:
    name: docs -D rustdoc warnings
    runs-on: ubuntu-latest
    timeout-minutes: 10
    env:
      RUSTDOCFLAGS: "-D warnings"
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
      - uses: Swatinem/rust-cache@v2
      - run: cargo doc --workspace --no-deps --all-features

  # ── 7. Miri (undefined behaviour detection on the unsafe surface) ────────
  miri:
    name: miri (axonos-spsc)
    runs-on: ubuntu-latest
    timeout-minutes: 20
    continue-on-error: true
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@nightly
        with:
          components: miri
      - uses: Swatinem/rust-cache@v2
      - name: miri test axonos-spsc
        run: cargo miri test -p axonos-spsc

  # ── 8. Kani bounded model checking ───────────────────────────────────────
  # Each crate runs as an independent matrix job with its own timeout.
  # `continue-on-error: true` means a hung or failing Kani proof does NOT
  # fail the entire pipeline — the result is reported independently.
  # Inspect each kani job's log after a push to see what proved and what
  # timed out.
  #
  # To run locally:
  #   cargo install --locked kani-verifier
  #   cargo kani setup
  #   cd axonos-X/kani-proofs && cargo kani --default-unwind 16
  kani:
    name: kani (${{ matrix.crate }})
    runs-on: ubuntu-latest
    timeout-minutes: 35
    continue-on-error: true
    strategy:
      fail-fast: false
      matrix:
        crate:
          - axonos-spsc
          - axonos-scheduler
          - axonos-capability
          - axonos-time
          - axonos-intent
    steps:
      - uses: actions/checkout@v4
      - uses: model-checking/kani-github-action@v1
        with:
          working-directory: ${{ matrix.crate }}/kani-proofs
          args: "--default-unwind 16"

  # ── 9. Bare-metal firmware build (Cortex-M4F) ────────────────────────────
  # The firmware crate is excluded from the parent workspace and built
  # independently with its target-specific .cargo/config.toml.
  firmware:
    name: firmware (STM32F407)
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@stable
        with:
          targets: thumbv7em-none-eabihf
      - uses: Swatinem/rust-cache@v2
      - name: Build firmware
        working-directory: axonos-firmware-stm32f407
        # Explicit --target: relying on .cargo/config.toml has proven
        # fragile in some CI environments. Passing the target on the
        # command line is the canonical way.
        run: cargo build --release --target thumbv7em-none-eabihf

  # ── 10. cargo-deny (licence + advisory + bans audit) ─────────────────────
  # Pinned to v1: v2 has compatibility issues with cargo-deny 0.15+ where it
  # tries to invoke non-existent top-level subcommands. continue-on-error is
  # set because licence/advisory checks are informational at pre-1.0 stage.
  deny:
    name: cargo-deny
    runs-on: ubuntu-latest
    timeout-minutes: 10
    continue-on-error: true
    steps:
      - uses: actions/checkout@v4
      - uses: EmbarkStudios/cargo-deny-action@v1
        with:
          command: check bans licenses sources