Implement GH action script.

.github/workflows/release.yml

@@ -36,6 +36,11 @@ jobs:
             echo "Git tag ${{env.TAG_VERSION}} did not match crate version ${{env.CRATE_VERSION}}"
             exit 1
           fi
+          # Check the action script's tag.
+          if ! grep -F "image: docker://ghcr.io/model-checking/kani-ubuntu-20.04:${{ env.TAG_VERSION }}" action.yml; then
+            echo "Git tag ${{env.TAG_VERSION}} did not match version in action.yml"
+            exit 1;
+          fi
 
       - name: Create release
         id: create_release
@@ -138,3 +143,9 @@ jobs:
             org.opencontainers.image.source=${{ github.repositoryUrl }}
             org.opencontainers.image.version=${{ needs.Release.outputs.version }}
             org.opencontainers.image.licenses=Apache-2.0 OR MIT
+
+      - name: Check action and image is updated.
+          uses: ${{ env.OWNER_LC }}/kani@${{ needs.Release.outputs.version }})
+          with:
+            command: |
+              [[ "$(cargo kani --version)" == 'cargo-kani ${{ needs.Release.outputs.version }}' ]]

README.md

@@ -9,6 +9,13 @@ Kani verifies:
  * The absence of panics (e.g., `unwrap()` on `None` values)
  * The absence of some types of unexpected behavior (e.g., arithmetic overflows)
 
+## GitHub Action
+
+Use Kani in your CI with `model-checking/kani@VERSION`. See the
+[GitHub Action section in the Kani
+book](https://model-checking.github.io/kani/install-github-ci.html)
+for details.
+
 ## Installation
 
 To install the latest version of Kani, run:

action.yml

@@ -0,0 +1,25 @@
+# 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 --workspace'
+
+runs:
+  using: 'docker'
+  image: docker://ghcr.io/model-checking/kani-ubuntu-20.04:0.10.0
+  args:
+    - bash
+    - '-c'
+    - 'set -e; export HOME=/root USER=$(id -nu); source $HOME/.bashrc; ${{ inputs.command }}'
+

docs/src/SUMMARY.md

@@ -3,6 +3,7 @@
 - [Getting started](./getting-started.md)
   - [Installation](./install-guide.md)
     - [Building from source](./build-from-source.md)
+    - [GitHub CI Action](./install-github-ci.md)
   - [Using Kani](./usage.md)
   - [Verification results](./verification-results.md)
   - [Debugging verification failures](./debugging-verification-failures.md)

docs/src/install-github-ci.md

@@ -0,0 +1,54 @@
+# GitHub Action
+
+Kani offers a GitHub Action for running Kani in CI. As of now, only
+Ubuntu 20.04 with `x86_64-unknown-linux-gnu` is supported for Kani in
+CI.
+
+## Using Kani in your GitHub workflow
+Our GitHub Action is available in the GitHub Marketspace with the name
+`model-checking/kani`
+
+The following workflow snippet will checkout your repository and run
+`cargo kani` on it whenever a push or pull request occurs. Replace
+`VER.SION` with the version of Kani you want to run with.
+
+```yaml
+name: Kani CI
+on:
+  pull_request:
+  push:
+jobs:
+  run-kani:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: 'Checkout your code.'
+        uses: actions/checkout@v2
+
+      - name: 'Run Kani on your code.'
+        uses: model-checking/kani@vVER.SION
+```
+
+This will run `cargo kani --workspace` on the code you checked
+out. You can also provide a custom command for running Kani. For
+example, the below code runs 2 commands in sequence where the first
+command compiles the crate without running Kani, and the second runs
+Kani on specified packages.
+
+```
+      - name: 'Run Kani on your code.'
+        uses: model-checking/kani@vVER.SION
+        with:
+          command: |
+            cargo kani --only-codegen
+            cargo kani -p mypackage-a -p mypackage-b
+```
+
+## FAQ
+- **Kani takes too long for my CI**: Try running Kani on a
+  [schedule](https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule)
+  with desired frequency.
+- **Kani Silently Crashes with no logs**: Few possible reasons:
+  - Kani ran out of RAM. GitHub offers up to 7GB of RAM, but Kani may
+    use more. Run locally to confirm.
+  - GitHub terminates jobs longer than 6 hours.
+  - Otherwise, consider filing an issue [here](https://github.com/model-checking/kani/issues).

docs/src/install-guide.md

@@ -5,7 +5,9 @@ Kani offers an easy installation option on two platforms:
 * `x86_64-unknown-linux-gnu` (Most Linux distributions)
 * `x86_64-apple-darwin` (Intel Mac OS)
 
-Other platforms are either not yet supported or require instead that you [build from source](build-from-source.md).
+Other platforms are either not yet supported or require instead that
+you [build from source](build-from-source.md). To use Kani in your
+GitHub CI workflows, see [GitHub CI Action](./install-github-ci.md).
 
 ## Dependencies