Implement GH action script.

[YoshikiTakashima]

Description of changes:

Adds a github actions script that runs Kani on user code

Resolved issues:

Resolves #1312

Call-outs:

• Blocked on Release Kani with GH packages. #1587 This action script relies on docker to work. Kani needs to publish Docker images as packages for this action to work. PR Added packages to release for ubuntu-20.04 only. #1595!

• Testing is a bit odd on this one. We expect our customers to integrate via marketplace, but we can't test that integration until this script is merged. See testing sections for details

• Integration method is through docker, which will require a package release. I think this is cleanest since it requires no build on customer end. Risk of breakage is less, we don't slow their CI pipeline with our install and build.

• Kani options is intended to be passed in via Cargo.toml section [package.metadata.kani.flags]. Also configuring this action is only possible through Cargo.toml I think maintaining 2 APIs will be a mess and YAML is not very good for wrangling certain parameters (e.g. cargo kani -p packageA -p packageb). It would be much easier to maintain if we only allow configuration trhough Cargol.toml.

Testing:

• How is this change tested? You can test this by pasting the action.yml into a cargo project that already uses Kani, then running the kani harnesses with it. Add a workflow referencing this action, and trigger it. Results should match that of running cargo kani on that project.

• Is this a refactor change? NO

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented. TBD Adding docs in the Kani book. 3d5b2af
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[YoshikiTakashima]

@tedinski Would you mind reviewing this. It's still blocked, but demand (as far as I can tell from Rust users around me) is very strong on this one.

[YoshikiTakashima]

Once this is merged, somebody with sufficient permissions will need to enable actions in the GH marketplace.

[YoshikiTakashima]

This issue is no longer blocked. Please do a second pass.

Also, to pin the image to the respective version, I had to make a hard-coded value in action.yml with a "update version" check every release. If anyone knows an auto-upgrading solution, please let me know.

[adpaco-aws]

Thanks @YoshikiTakashima !

One question: How hard would it be to extend this action with an include/exclude list of proofs to run?

In my experience, users may want to exclude a proof from being run in CI, either because it's too time-consuming or it no longer passes after changing the function under verification. That said, I think the right way to do that would be to add another attribute like "ignore" to the proofs themselves, so cargo kani can handle that instead.

[YoshikiTakashima]

@adpaco-aws As of now, any flag that works with rust can be used with [package.metadata.kani.flags]. So --harness will work, but I think it does not allow multiple harnesses to be specified at this point.

[danielsn]

LGTM, a few comments