PropProof integration (#19)

Co-authored-by: Yoshiki Takashima <[email protected]>
Co-authored-by: Adrian Palacios <[email protected]>

Author: 3 people

.github/workflows/test-action.yml

@@ -16,3 +16,9 @@ jobs:
         uses: ./ # Uses the action in the root directory
         with:
           working-directory: tests/cargo-kani/simple-lib
+      - name: Test ProfProof within Kani Action
+        uses: ./
+        with:
+          working-directory: tests/cargo-kani/proptest-lib
+          args: --tests
+          enable-propproof: true

action.yml

@@ -22,6 +22,10 @@ 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"
@@ -42,6 +46,17 @@ runs:
         cargo install --version $KANI_VERSION --locked kani-verifier;
         cargo-kani setup;
 
+    - name: Install PropProof
+      if: ${{ inputs.enable-propproof }}
+      shell: bash
+      run: |
+        export PROPPROOF_PATH=$HOME/propproof
+        git clone https://github.com/model-checking/kani \
+        --branch features/proptest $PROPPROOF_PATH || true
+        git -C $PROPPROOF_PATH submodule update --init --recursive
+        echo "paths = [\"$PROPPROOF_PATH\"]" > $HOME/.cargo/config.toml
+      # || true is used to handle cases where the propproof folder is cached.
+
     - name: Run Kani
       shell: bash
       run: |

tests/cargo-kani/proptest-lib/.gitignore

@@ -0,0 +1 @@
+/target

tests/cargo-kani/proptest-lib/Cargo.toml

@@ -0,0 +1,13 @@
+## 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]

tests/cargo-kani/proptest-lib/src/lib.rs

@@ -0,0 +1,28 @@
+// 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::<u32>().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::<i32>().prop_map(|x| x * 2)) {
+                prop_assert_eq!(even_num % 2, 0, "even number");
+            }
+        }
+    }
+}