# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

name: 'Kani Rust Verifier'
description: 'Run the Kani Rust Verifier on a Rust Crate'
author: 'Kani Contributors'

branding:
  icon: 'cloud'
  color: 'orange'

inputs:
  command:
    description: 'Command to run.'
    required: false
    default: 'cargo-kani'
  working-directory:
    description: 'Directory to run kani on.'
    required: false
    default: '.'
  args:
    description: 'Arguments to pass to kani.'
    required: false
    default: ''
  enable-propproof:
    description: 'Experimental: Allow Kani to verify proptest harnesses using the PropProof feature'
    required: false
    default: false

runs:
  using: "composite"
  steps:
    - name: Install Rust
      uses: dtolnay/rust-toolchain@stable

    - name: Install Kani
      shell: bash
      run: |
        export KANI_VERSION="0.33.0";
        cargo install --version $KANI_VERSION --locked kani-verifier;
        cargo-kani setup;

    - name: Install PropProof
      if: ${{ inputs.enable-propproof == 'true' }}
      uses: actions/checkout@v3
      with:
        repository: model-checking/kani
        ref: features/proptest
        path: propproof
        submodules: true

    - name: Add PropProof to config
      if: ${{ inputs.enable-propproof == 'true' }}
      shell: bash
      run: |
        echo "paths = [\"$GITHUB_WORKSPACE/propproof\"]" > $HOME/.cargo/config.toml

    - name: Run Kani
      shell: bash
      run: |
        cd ${{ inputs.working-directory }};
        ${{ inputs.command }} ${{ inputs.args }}