# Kani
This document describes how to **locally** install and use Kani, along
with its experimental PropProof feature. Because of instability in
Kani internals, the GitHub action is the recommended option if you are
running in CI.

Kani is a software verification tool that complements testing by
proving the absence of certain classes of bugs like unwrap exceptions,
overflows, and assertion failures. See the [Kani
book](https://model-checking.github.io/kani/) for a full list of
capabilities and limitations.

## Installing Kani and PropProof
-  The install instructions for Kani can be [found
   here](https://model-checking.github.io/kani/install-guide.html). Once
   Kani is installed, you can run with `cargo kani` for projects or
   `kani` for individual Rust files.
- **[UNSTABLE]** To use PropProof, first download the source code
  from the Kani repository.
  ```bash
  git clone https://github.com/model-checking/kani.git --branch features/proptest propproof
  cd propproof; git submodule update --init
  ```

  Then, use `.cargo/config.toml` enable it in the local directory you
  want to run Kani in. This will override the `proptest` import in
  your repo.

  ```bash
  cd $YOUR_REPO_LOCAL_PATH
  mkdir '.cargo'
  echo "paths =[\"$PATH_TO_PROPPROOF\"]" > .cargo/config.toml
  ```

**Please Note**:
- `features/proptest` branch under Kani is likely not the final
  location for this code. If these instructions stop working, please
  consult the Kani documentation and file an issue on [the Kani
  repo](https://github.com/model-checking/kani.git).
- The cargo config file will force cargo to always use PropProof. To
  use `proptest`, delete the file.

## Running Kani
After installing Kani and PropProof, `cargo kani --tests` should
automatically run `proptest!` harnesses inside your crate. Use
`--harness` to run a specific harness, and `-p` for a specific
sub-crate.

If Kani returns with an error, you can use the concrete playback
feature using `--enable-unstable --concrete-playback print` and paste
in the code to your repository. Running this harness with `cargo test`
will replay the input found by Kani that produced this crash. Please
note that this feature is unstable and using `--concrete-playback
inplace` to automatically inject a replay harness is not supported
when using PropProof.

## Debugging CI Failure
```yaml
      - name: Verify with Kani
        uses: model-checking/kani-github-action@v0.xx
        with:
          enable-propproof: true
          args: |
            $KANI_ARGUMENTS
```

The above GitHub CI workflow is equivalent to `cargo kani
$KANI_ARGUMENTS` with PropProof installed. To replicate issues
locally, run `cargo kani` with the same arguments.