model-checking / kani-github-action Goto Github PK

Requested feature: PropProof integration (model-checking/kani#1608) should work inside action.
Use case: PROST, et. al.

Test case: https://github.com/YoshikiTakashima/simplified-prost-rs-timestamp

As of now, the version number of kani-github-action is tied 1:1 to the version number of Kani. This should be decoupled and the kani-github-action should pull in the latest version of Kani by default unless a specific version of Kani is pinned by the user.

With #26, the GitHub action now installs two Rust toolchains:

1. The stable toolchain (explicitly through the actions-rs/toolchain action)
2. Kani's integrated toolchain (through the cargo-kani setup step).

The action should instead install the toolchain needed by Kani directly. This can be done by parsing Kani's rust-toolchain.toml file.

I suggest that we restructure the action read me to the following:

Quick description about the action (not the repo). Include one sentence about Kani and a link to it.

Quick Start

Action Parameters

Currently, we only test a single small cago-kani example. Possible improvements

• Example that needs workspace
• Example that needs --tests
• example that has dependencies
• example where the rust version matters
• examples with different kani versions

The enable-propproof input to the action does not seem to be working correctly. Even in this repo's CI, the Run Kani step, which does not set enable-propproof to true:

is running the PropProof step:
https://github.com/model-checking/kani-github-action/actions/runs/4107392392/jobs/7148904069#step:3:111

Requested feature: What it says in the title
Use case: Users may wish to get the latest and greatest kani without needing to manually update after each release.

Right now, that's hardcoded in. Instead we should parse it from the toml

Requested feature: Support Kani's --output-format=terse option.
Use case: Ease of viewing the CI log.

Test case: Here are two views, one w/ terse and one w/out -- https://github.com/weaversa/aes-rust/actions/runs/3388002019/jobs/5629452264

Currently, we install Kani every time, but this takes bandwidth and can be flaky.
Instead, we should prebuild a docker and use that.

In a recent zerocopy PR, we had to stop testing our nightly-only features under Kani. The reason is that those features were recently updated to work with a more recent version of the nightly Rust toolchain, and so are now incompatible with older nightlies. Since the Kani GH action selects its own toolchain, it makes that action incompatible with our nightly-only features. At the moment, we don't use Kani to test any of those features, so we simply disabled those features when using Kani. In the future, though, this could become a problem for us if we want to use Kani to test nightly-only features.

It would be great if the Kani GH action allowed specifying which Rust toolchain to use.

Here's the code in question from our Kani GH action invocation in CI:

          # Use `--features __internal_use_only_features_that_work_on_stable`
          # because the Kani GitHub Action uses its own pinned nightly
          # toolchain. Sometimes, we make changes to our nightly features for
          # more recent toolchains, and so our nightly features become
          # incompatible with the toolchain that Kani uses. By only testing
          # stable features, we ensure that this doesn't cause problems in CI.
          args: "--package zerocopy --features __internal_use_only_features_that_work_on_stable --output-format=terse --randomize-layout --memory-safety-checks --overflow-checks --undefined-function-checks --unwinding-checks"

There should be a simple GitHub action that Kani users can use to verify their GitHub code

I tried to run my typical Github action for Kani. Historically, this has never caused any issues for the installation of crates. However, on my recent pushes, cargo seems to no longer be able to find optional registries: https://github.com/nyx-space/hifitime/actions/runs/4399579815/jobs/7704213779 . I am not sure what has happened.