kani.yml

# This workflow is responsible for verifying the standard library with Kani.

name: Kani
on:
  workflow_dispatch:
  pull_request:
    branches: [ main ]
  push:
    paths:
      - 'library/**'
      - '.github/workflows/kani.yml'
      - 'scripts/run-kani.sh'

defaults:
  run:
    shell: bash

jobs:
  build:
    runs-on: ${{ matrix.os }}
    strategy:
      matrix:
        # Kani does not support windows.
        os: [ubuntu-latest, macos-latest]
        include:
          - os: ubuntu-latest
            base: ubuntu
          - os: macos-latest
            base: macos
    steps:
      - name: Checkout Library
        uses: actions/checkout@v4
        with:
          path: head
          submodules: true

      - name: Run Kani Script
        run: bash ./head/scripts/run-kani.sh --path ${{github.workspace}}/head

      - name: Run Kani Script with --kani-args and -p
        run: bash ./head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut

      - name: Run Kani Script without -p
        working-directory: ${{github.workspace}}/head
        run: bash ./scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut