From c05441bb5d141605a30f1ffe14bcba27507c0f18 Mon Sep 17 00:00:00 2001 From: PhysShell Date: Fri, 18 Sep 2026 07:25:37 +0000 Subject: [PATCH 1/4] Fix Kani version parsing in install script `kani --version` reports versions as: Kani Rust Verifier () so `awk '{print $2}'` extracts `Rust` instead of the version. Kani 0.33.0, which this repository uses as its pinned older-version test, already used this output format. Parse the version from the `Kani Rust Verifier` line explicitly and fail if it cannot be determined. Apply the same parsing to the two version checks in `test-action.yml`. --- .github/workflows/test-action.yml | 10 ++++++++-- src/install-kani.sh | 10 +++++++++- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/.github/workflows/test-action.yml b/.github/workflows/test-action.yml index 97e219a..bb5a15a 100644 --- a/.github/workflows/test-action.yml +++ b/.github/workflows/test-action.yml @@ -40,7 +40,10 @@ jobs: - name: Test "Run Kani with older version" run: | - installed_version=$(kani --version | awk '{print $2}') + installed_version=$( + kani --version | + sed -nE '1s/^Kani Rust Verifier ([^[:space:]]+).*/\1/p' + ) expected_version='0.33.0' if [[ "$installed_version" == "$expected_version" ]]; then @@ -57,7 +60,10 @@ jobs: - name: Test "Run Kani with latest version" run: | - installed_version=$(kani --version | awk '{print $2}') + installed_version=$( + kani --version | + sed -nE '1s/^Kani Rust Verifier ([^[:space:]]+).*/\1/p' + ) expected_version=$(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g') if [[ "$installed_version" == "$expected_version" ]]; then diff --git a/src/install-kani.sh b/src/install-kani.sh index 8b34f5f..35708dd 100755 --- a/src/install-kani.sh +++ b/src/install-kani.sh @@ -22,7 +22,15 @@ fi cargo-kani setup; # Get the current installed version of kani and check it against the latest version -installed_version=$(kani --version | awk '{print $2}') +installed_version=$( + kani --version | + sed -nE '1s/^Kani Rust Verifier ([^[:space:]]+).*/\1/p' +) + +if [ -z "$installed_version" ]; then + echo "::error::Could not determine installed Kani version" + exit 1 +fi if [ $? -eq 0 ]; then if [ "$1" == "latest" ]; then From bcc81d03e1d8465566ca0b570b2a39471ca8cc6f Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 20 Sep 2026 20:44:46 +0000 Subject: [PATCH 2/4] Also accept the pre-0.68.0 `--version` output format The custom `--version` handler is new in Kani 0.68.0: `args/mod.rs` sets `disable_version_flag = true` and `main.rs` calls `print_kani_version`. Through 0.67.0, `--version` was clap's derived flag from `#[command(version, name = "kani", ...)]` and printed kani `print_kani_version` existed back then too, but only the verification paths reached it, so it was a run banner rather than `--version` output. Checked 0.60, 0.63, 0.65, 0.66, 0.67 and 0.68: `disable_version_flag` appears only at 0.68.0. Parsing just the `Kani Rust Verifier` line therefore fails for every version up to 0.67.0, including the pinned 0.33.0 test case, which is what CI reported: [5/5] Successfully completed Kani first-time setup. ##[error]Could not determine installed Kani version `kani-version` accepts any published version, so accept both formats. Anchor on the program name instead of line 1, since `kani` prints first-time setup progress ahead of the banner when setup is incomplete. Drop the `if [ $? -eq 0 ]` guard around the comparison: `$?` there is the status of the preceding assignment, that is of the command substitution, so it never guarded the parse. The empty check above covers that now. Report both versions in the mismatch error, since the old message made this failure needlessly hard to diagnose, print the requested version instead of the unset `$VERSION` on the `latest` path, and re-anchor the `cargo search` grep, verified against `cargo search kani-verifier` output. --- .github/workflows/test-action.yml | 14 ++++++++----- src/install-kani.sh | 34 +++++++++++++++++-------------- 2 files changed, 28 insertions(+), 20 deletions(-) diff --git a/.github/workflows/test-action.yml b/.github/workflows/test-action.yml index bb5a15a..adbe4bd 100644 --- a/.github/workflows/test-action.yml +++ b/.github/workflows/test-action.yml @@ -40,9 +40,12 @@ jobs: - name: Test "Run Kani with older version" run: | + # Kani 0.67.0 and earlier print `kani `; 0.68.0 and later + # print `Kani Rust Verifier ()` plus a CBMC line. installed_version=$( - kani --version | - sed -nE '1s/^Kani Rust Verifier ([^[:space:]]+).*/\1/p' + kani --version | + sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' | + head -1 ) expected_version='0.33.0' @@ -61,10 +64,11 @@ jobs: - name: Test "Run Kani with latest version" run: | installed_version=$( - kani --version | - sed -nE '1s/^Kani Rust Verifier ([^[:space:]]+).*/\1/p' + kani --version | + sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' | + head -1 ) - expected_version=$(cargo search kani-verifier | grep -m 1 "kani" | awk '{print $3}' | sed 's/"//g') + expected_version=$(cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}' | sed 's/"//g') if [[ "$installed_version" == "$expected_version" ]]; then echo "The installed version ($installed_version) matches the latest version ($expected_version)" diff --git a/src/install-kani.sh b/src/install-kani.sh index 35708dd..0cd0acd 100755 --- a/src/install-kani.sh +++ b/src/install-kani.sh @@ -12,7 +12,7 @@ fi # Check exit status for error handling if [ $? -eq 0 ]; then - echo "Installed Kani $VERSION successfully" + echo "Installed Kani $1 successfully" else echo "::error::Could not install Kani. Please check if the provided version is correct" exit 1 @@ -21,27 +21,31 @@ fi # Setup kani in ci cargo-kani setup; -# Get the current installed version of kani and check it against the latest version +# Get the current installed version of kani and check it against the latest version. +# Two output formats have to be supported, since this action can install any +# published version: +# - Kani 0.68.0 and later print `Kani Rust Verifier ()`, +# followed by a `CBMC ` line. +# - Kani 0.67.0 and earlier used clap's default flag, printing `kani `. installed_version=$( kani --version | - sed -nE '1s/^Kani Rust Verifier ([^[:space:]]+).*/\1/p' + sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' | + head -1 ) if [ -z "$installed_version" ]; then - echo "::error::Could not determine installed Kani version" + echo "::error::Could not determine installed Kani version from \`kani --version\`" exit 1 fi -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}' | tr -d '"') - else - requested_version=$1 - fi +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}' | tr -d '"') +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 +if [ "$installed_version" != "$requested_version" ]; then + echo "::error::The version of Kani installed ($installed_version) was different than the one requested ($requested_version)" + exit 1 fi From a7155ef4fc2ef1f36359ed2c967519bdececcc4f Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 20 Sep 2026 20:49:34 +0000 Subject: [PATCH 3/4] Force color off when resolving the latest version `cargo search` output is colored in CI: the Rust toolchain action exports CARGO_TERM_COLOR=always via $GITHUB_ENV, which applies to every later step in the job, and cargo honors it even when stdout is a pipe. The line arrives as \e[1m\e[32mkani-verifier\e[0m = "0.68.0" # ... so `grep '^kani-verifier '` never matches, `requested_version` is empty, and the `latest` path fails the comparison it is meant to pass: The version of Kani installed (0.68.0) was different than the one requested () This is why 2534b7a dropped the anchor. Keep the anchor, which also avoids matching unrelated crates whose descriptions mention Kani, and set CARGO_TERM_COLOR=never for the lookup instead. Reproduced both the failure and the fix against `cargo search kani-verifier`. Fail loudly when the lookup yields nothing, rather than comparing against an empty string. Keeping the comparison on the `latest` path is deliberate: it is what catches `cargo install` leaving an older binary in place, for instance when a runner image already ships Kani. --- .github/workflows/test-action.yml | 4 +++- src/install-kani.sh | 10 ++++++++-- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/.github/workflows/test-action.yml b/.github/workflows/test-action.yml index adbe4bd..55cea8e 100644 --- a/.github/workflows/test-action.yml +++ b/.github/workflows/test-action.yml @@ -68,7 +68,9 @@ jobs: sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' | head -1 ) - expected_version=$(cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}' | sed 's/"//g') + # CARGO_TERM_COLOR=always leaks in from the Rust toolchain action, and + # its escape codes would defeat the anchor below. + expected_version=$(CARGO_TERM_COLOR=never cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}' | sed 's/"//g') if [[ "$installed_version" == "$expected_version" ]]; then echo "The installed version ($installed_version) matches the latest version ($expected_version)" diff --git a/src/install-kani.sh b/src/install-kani.sh index 0cd0acd..591de2d 100755 --- a/src/install-kani.sh +++ b/src/install-kani.sh @@ -39,8 +39,14 @@ if [ -z "$installed_version" ]; then fi 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}' | tr -d '"') + # Cargo search returns version number as string. Force color off: the Rust + # toolchain action exports CARGO_TERM_COLOR=always, and the escape codes it + # adds would otherwise defeat the anchor below. + requested_version=$(CARGO_TERM_COLOR=never cargo search kani-verifier | grep -m 1 "^kani-verifier " | awk '{print $3}' | tr -d '"') + if [ -z "$requested_version" ]; then + echo "::error::Could not determine the latest Kani version from \`cargo search\`" + exit 1 + fi else requested_version=$1 fi From 2c94d951cdd1b0f49f576e05401b760b9e72766d Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Sun, 20 Sep 2026 21:15:08 +0000 Subject: [PATCH 4/4] Retire the experimental PropProof integration PropProof relied on a cargo `paths` override pointing at `model-checking/kani` branch `features/proptest`, whose last commit is 2025-05-13. Its vendored proptest no longer compiles: recent nightly std added inherent `SIGN_MASK`, `EXP_MASK` and `MANTISSA_MASK` consts on f32 and f64, which collide with proptest's own `FloatLayout` trait consts. That fires `unstable_name_collisions`, a member of the `future_incompatible` group that `proptest/src/lib.rs` puts under `#![forbid(...)]`, so 16 sites in `proptest/src/num.rs` fail to build: error: an associated constant with this name may be added to the standard library in the future --> propproof/proptest/src/num.rs:607:21 | 607 | $typ::SIGN_MASK Fixing that belongs on the upstream branch, not here, and nothing has maintained it for over a year. Anyone passing `enable-propproof: true` today already fails this way, so remove the input, the two steps that set up the override, the workflow test, its fixture crate, and the README section rather than carry a lint workaround for a feature that no longer works. This drops a documented input. GitHub only warns on unknown inputs to a composite action, so existing workflows keep running; they lose a feature that is already broken for them. --- .github/workflows/test-action.yml | 7 ------ README.md | 9 +------- action.yml | 19 ---------------- tests/cargo-kani/proptest-lib/.gitignore | 1 - tests/cargo-kani/proptest-lib/Cargo.toml | 13 ----------- tests/cargo-kani/proptest-lib/src/lib.rs | 28 ------------------------ 6 files changed, 1 insertion(+), 76 deletions(-) delete mode 100644 tests/cargo-kani/proptest-lib/.gitignore delete mode 100644 tests/cargo-kani/proptest-lib/Cargo.toml delete mode 100644 tests/cargo-kani/proptest-lib/src/lib.rs diff --git a/.github/workflows/test-action.yml b/.github/workflows/test-action.yml index 55cea8e..55dee0d 100644 --- a/.github/workflows/test-action.yml +++ b/.github/workflows/test-action.yml @@ -78,10 +78,3 @@ jobs: 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: - working-directory: tests/cargo-kani/proptest-lib - args: --tests - enable-propproof: true diff --git a/README.md b/README.md index 92461e2..9971d6a 100644 --- a/README.md +++ b/README.md @@ -33,12 +33,6 @@ If omitted, the latest version of `Kani` hosted on [`Kani's crates.io page`](htt - **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: @@ -75,7 +69,7 @@ jobs: #### Example 3: Run Kani with args -Use latest version of Kani, to run `cargo-kani --tests` on a project with `propproof` harnesses. +Use latest version of Kani, to run `cargo-kani --tests` on a project. ```yaml jobs: @@ -86,7 +80,6 @@ jobs: uses: model-checking/kani-github-action@v1 with: args: '--tests' - enable-propproof: true ``` ## Security diff --git a/action.yml b/action.yml index 664f6ae..b417ac0 100644 --- a/action.yml +++ b/action.yml @@ -26,10 +26,6 @@ inputs: description: 'Arguments to pass to kani.' required: false default: '' - enable-propproof: - description: 'Experimental: Allow Kani to verify proptest harnesses using the PropProof feature' - required: false - default: false runs: using: "composite" @@ -41,21 +37,6 @@ runs: run: ${{ github.action_path }}/src/install-kani.sh ${{ inputs.kani-version }} shell: bash - - name: Install PropProof - if: ${{ inputs.enable-propproof == 'true' }} - uses: actions/checkout@v3 - with: - repository: model-checking/kani - ref: features/proptest - path: propproof - submodules: true - - - name: Add PropProof to config - if: ${{ inputs.enable-propproof == 'true' }} - shell: bash - run: | - echo "paths = [\"$GITHUB_WORKSPACE/propproof\"]" > $HOME/.cargo/config.toml - - name: Run Kani shell: bash run: | diff --git a/tests/cargo-kani/proptest-lib/.gitignore b/tests/cargo-kani/proptest-lib/.gitignore deleted file mode 100644 index c41cc9e..0000000 --- a/tests/cargo-kani/proptest-lib/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/target \ No newline at end of file diff --git a/tests/cargo-kani/proptest-lib/Cargo.toml b/tests/cargo-kani/proptest-lib/Cargo.toml deleted file mode 100644 index 38ba767..0000000 --- a/tests/cargo-kani/proptest-lib/Cargo.toml +++ /dev/null @@ -1,13 +0,0 @@ -## Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -[package] -name = "proptest-lib" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] -proptest = "1.0" - -[workspace] \ No newline at end of file diff --git a/tests/cargo-kani/proptest-lib/src/lib.rs b/tests/cargo-kani/proptest-lib/src/lib.rs deleted file mode 100644 index cf75a59..0000000 --- a/tests/cargo-kani/proptest-lib/src/lib.rs +++ /dev/null @@ -1,28 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Basic proptest examples. First one verifies, but the second one -//! does not. - -#[cfg(test)] -mod test { - use proptest::prelude::*; - proptest! { - /// Works fine. Shift has no overflow check. - fn works_fine(even_num in any::().prop_map(|x| x << 1)) { - prop_assert_eq!(even_num % 2, 0, "even number"); - } - } - - #[cfg(not(kani))] - mod expected { - proptest! { - /// Overflow by check in x * 2. TODO: Need to implement - /// expected fail tests. tracking issue: - /// https://github.com/model-checking/kani-github-action/issues/5 - fn fails(even_num in any::().prop_map(|x| x * 2)) { - prop_assert_eq!(even_num % 2, 0, "even number"); - } - } - } -}