Decouple kani version from kani-github-action version

.github/workflows/test-action.yml

@@ -12,10 +12,61 @@ jobs:
       # you must check out the repository
       - name: Checkout
         uses: actions/checkout@v3
-      - name: Run Kani
+
+      - name: Run Kani with invalid version
+        id: set_error
+        uses: ./
+        with:
+          working-directory: tests/cargo-kani/simple-lib
+          kani-version: '0.1.10'
+        continue-on-error: true
+
+      - name: Ensure "Run Kani with invalid version" fails
+        id: get_error
+        run: |
+          # Check the outcome of "Run Kani with invalid version"
+          if [[ "${{ steps.set_error.outcome }}" == "failure" ]]; then
+            echo "Running Kani with invalid version "0.1.10" failed."
+          else
+            echo "::error::Running Kani with invalid version succeeded incorrectly or was skipped."
+            exit 1
+          fi
+
+      - name: Run Kani with older version
         uses: ./ # Uses the action in the root directory
         with:
           working-directory: tests/cargo-kani/simple-lib
+          kani-version: '0.33.0'
+
+      - name: Test "Run Kani with older version"
+        run: |
+          installed_version=$(kani --version | awk '{print $2}')
+          expected_version='0.33.0'
+
+          if [[ "$installed_version" == "$expected_version" ]]; then
+            echo "The installed version ($installed_version) matches the expected version ($expected_version)."
+          else
+            echo "::error::The installed version ($installed_version) does not match the expected version ($expected_version)."
+            exit 1
+          fi
+
+      - name: Run Kani with latest version
+        uses: ./ # Uses the action in the root directory
+        with:
+          working-directory: tests/cargo-kani/simple-lib
+
+      - name: Test "Run Kani with latest version"
+        run: |
+          installed_version=$(kani --version | awk '{print $2}')
+          expected_version=$(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g')
+
+          if [[ "$installed_version" == "$expected_version" ]]; then
+            echo "The installed version ($installed_version) matches the latest version ($expected_version)"
+          else
+            echo "::error::The installed version ($installed_version) does not match the latest version ($expected_version)."
+            exit 1
+          fi
+
       - name: Test ProfProof within Kani Action
         uses: ./
         with:

README.md

@@ -2,6 +2,93 @@
 
 This repository provides a GitHub Action for running the [Kani Rust Verifier](https://github.com/model-checking/kani) in CI.
 
+## Kani GitHub Action Parameters
+
+The following parameters can be used to configure and customize the behavior of this GitHub Action:
+
+**NOTE**: All the fields provided are optional and have default behaviors when not specified.
+
+`kani-version`
+
+- **Description**: The Kani version to use.
+- **Default**: `latest`
+- **Usage**: `latest` or `x.y.z` to mention which version Kani to use. [Cargo's version specific format is expected for specific versions](https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html).
+If omitted, the latest version of `Kani` hosted on [`Kani's crates.io page`](https://crates.io/crates/kani-verifier) will be installed and used.
+
+`command`
+
+- **Description**: The command to run Kani.
+- **Default**: `cargo-kani`
+- **Usage**: `cargo-kani` or `kani` or custom path to a `kani` binary. Subcommands need to be passed to the `args` field.
+
+`working-directory`
+
+- **Description**: The directory in which Kani should be run.
+- **Default**: `'.'`
+- **Usage**: `/path/to/project` or `.`
+
+`args`
+
+- **Description**: Additional arguments to pass to Kani.
+- **Default**: `''`
+- **Usage**: These arguments or subcommands will be appended to the Kani command.
+
+`enable-propproof`
+
+- **Description**: Experimental feature that allows Kani to verify [proptest harnesses](https://proptest-rs.github.io/proptest/proptest/index.html) using the PropProof feature.
+- **Default**: `false`
+- **Usage**: If set to `true`, Kani will enable the experimental PropProof feature for verifying proptest harnesses.
+
+## Example usage in a workflow YAML file:
+
+Here are a few examples of workflow YAML files for the Kani Github Action:
+
+#### Example 1: Default configuration
+
+Default config which uses the latest version of Kani to run `cargo-kani` on project in current directory.
+
+```yaml
+jobs:
+  kani:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Run Kani
+        uses: model-checking/kani-github-action@v1.0
+```
+
+#### Example 2: Use pinned version of Kani
+
+Use a specific version of Kani, version `0.35.0`, to run `cargo-kani`  on a project.
+
+```yaml
+jobs:
+  kani:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Run Kani
+        uses: model-checking/kani-github-action@v1.0
+        with:
+          kani-version: '0.35.0'
+          command: 'cargo-kani'
+          working-directory: './path/to/project'
+```
+
+#### Example 3: Run Kani with args
+
+Use latest version of Kani, to run `cargo-kani --tests` on a project with `propproof` harnesses.
+
+```yaml
+jobs:
+  kani:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Run Kani
+        uses: model-checking/kani-github-action@v1.0
+        with:
+          args: '--tests'
+          enable-propproof: true
+```
+
 ## Security
 
 See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
@@ -10,4 +97,3 @@ See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more inform
 
 This code is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
 See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT) for details.
-

action.yml

@@ -10,6 +10,10 @@ branding:
   color: 'orange'
 
 inputs:
+  kani-version:
+    description: 'Kani Version number'
+    required: false
+    default: 'latest'
   command:
     description: 'Command to run.'
     required: false
@@ -34,11 +38,8 @@ runs:
       uses: dtolnay/rust-toolchain@stable
 
     - name: Install Kani
+      run: ${{ github.action_path }}/src/install-kani.sh ${{ inputs.kani-version }}
       shell: bash
-      run: |
-        export KANI_VERSION="0.37.0";
-        cargo install --version $KANI_VERSION --locked kani-verifier;
-        cargo-kani setup;
 
     - name: Install PropProof
       if: ${{ inputs.enable-propproof == 'true' }}

src/install-kani.sh

@@ -0,0 +1,39 @@
+#!/bin/bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# If version is latest, install directly from cargo
+if [ "$1" == "latest" ]; then
+    cargo install --locked kani-verifier;
+else
+    VERSION=$1
+    cargo install --version $VERSION --locked kani-verifier;
+fi
+
+# Check exit status for error handling
+if [ $? -eq 0 ]; then
+    echo "Installed Kani $VERSION successfully"
+else
+    echo "::error::Could not install Kani. Please check if the provided version is correct"
+    exit 1
+fi
+
+# Setup kani in ci
+cargo-kani setup;
+
+# Get the current installed version of kani and check it against the latest version
+installed_version=$(kani --version | awk '{print $2}')
+
+if [$? -eq 0]; then
+    if [ "$1" == "latest" ]; then
+        # Cargo search returns version number as string
+        requested_version=$(cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}')
+    else
+        requested_version=$1
+    fi
+
+    if ["$installed_version" != "$requested_version"]; then
+        echo "::error::The version of Kani installed was different than the one requested"
+        exit 1
+    fi
+fi