tests: Change some proptest to kani proofs

Three proptests are executed as kani proofs in CI.
Make that explicit by marking them as kani proof.
This removes the dependency on propproof dependency when using kani.

.github/workflows/ci.yml

@@ -182,19 +182,8 @@ jobs:
       - name: Verify with Kani
         uses: model-checking/[email protected]
         with:
-          enable-propproof: true
           args: |
-            --tests -p prost-types --default-unwind 3 \
-            --harness "tests::check_timestamp_roundtrip_via_system_time" \
-            --harness "tests::check_duration_roundtrip" \
-            --harness "tests::check_duration_roundtrip_nanos"
-        # --default-unwind N roughly corresponds to how much effort
-        # Kani will spend trying to prove correctness of the
-        # program. Higher the number, more programs can be proven
-        # correct. However, Kani will require more time and memory. If
-        # Kani fails with "Failed Checks: unwinding assertion," this
-        # number may need to be raised for Kani to succeed.
-
+            -p prost-types
   no-std:
     runs-on: ubuntu-latest
     steps:

KANI.md

@@ -1,6 +1,5 @@
 # Kani
-This document describes how to **locally** install and use Kani, along
-with its experimental PropProof feature. Because of instability in
+This document describes how to **locally** install and use Kani. Because of instability in
 Kani internals, the GitHub action is the recommended option if you are
 running in CI.
 
@@ -10,60 +9,20 @@ 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
+## Installing Kani
 -  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
+After installing Kani, `cargo kani` should
+automatically run `kani::proof` 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/[email protected]
-        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.
+note that this feature is unstable.

prost-types/Cargo.toml

@@ -21,3 +21,6 @@ prost = { version = "0.13.1", path = "../prost", default-features = false, featu
 
 [dev-dependencies]
 proptest = "1"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

prost-types/src/duration.rs

@@ -173,69 +173,72 @@ impl FromStr for Duration {
         datetime::parse_duration(s).ok_or(DurationError::ParseFailure)
     }
 }
-#[cfg(test)]
-mod tests {
+
+#[cfg(kani)]
+mod proofs {
     use super::*;
 
     #[cfg(feature = "std")]
-    use proptest::prelude::*;
+    #[kani::proof]
+    fn check_duration_roundtrip() {
+        let seconds = kani::any();
+        let nanos = kani::any();
+        kani::assume(nanos < 1_000_000_000);
+        let std_duration = std::time::Duration::new(seconds, nanos);
+        let Ok(prost_duration) = Duration::try_from(std_duration) else {
+            // Test case not valid: duration out of range
+            return;
+        };
+        assert_eq!(
+            time::Duration::try_from(prost_duration).unwrap(),
+            std_duration
+        );
 
-    #[cfg(feature = "std")]
-    proptest! {
-        #[test]
-        fn check_duration_roundtrip(
-            seconds in u64::arbitrary(),
-            nanos in 0u32..1_000_000_000u32,
-        ) {
-            let std_duration = time::Duration::new(seconds, nanos);
-            let prost_duration = match Duration::try_from(std_duration) {
-                Ok(duration) => duration,
-                Err(_) => return Err(TestCaseError::reject("duration out of range")),
+        if std_duration != time::Duration::default() {
+            let neg_prost_duration = Duration {
+                seconds: -prost_duration.seconds,
+                nanos: -prost_duration.nanos,
             };
-            prop_assert_eq!(time::Duration::try_from(prost_duration).unwrap(), std_duration);
-
-            if std_duration != time::Duration::default() {
-                let neg_prost_duration = Duration {
-                    seconds: -prost_duration.seconds,
-                    nanos: -prost_duration.nanos,
-                };
-
-                prop_assert!(
-                    matches!(
-                        time::Duration::try_from(neg_prost_duration),
-                        Err(DurationError::NegativeDuration(d)) if d == std_duration,
-                    )
-                )
-            }
+
+            assert!(matches!(
+                time::Duration::try_from(neg_prost_duration),
+                Err(DurationError::NegativeDuration(d)) if d == std_duration,
+            ))
         }
+    }
+
+    #[cfg(feature = "std")]
+    #[kani::proof]
+    fn check_duration_roundtrip_nanos() {
+        let seconds = 0;
+        let nanos = kani::any();
+        let std_duration = std::time::Duration::new(seconds, nanos);
+        let Ok(prost_duration) = Duration::try_from(std_duration) else {
+            // Test case not valid: duration out of range
+            return;
+        };
+        assert_eq!(
+            time::Duration::try_from(prost_duration).unwrap(),
+            std_duration
+        );
 
-        #[test]
-        fn check_duration_roundtrip_nanos(
-            nanos in u32::arbitrary(),
-        ) {
-            let seconds = 0;
-            let std_duration = std::time::Duration::new(seconds, nanos);
-            let prost_duration = match Duration::try_from(std_duration) {
-                Ok(duration) => duration,
-                Err(_) => return Err(TestCaseError::reject("duration out of range")),
+        if std_duration != time::Duration::default() {
+            let neg_prost_duration = Duration {
+                seconds: -prost_duration.seconds,
+                nanos: -prost_duration.nanos,
             };
-            prop_assert_eq!(time::Duration::try_from(prost_duration).unwrap(), std_duration);
-
-            if std_duration != time::Duration::default() {
-                let neg_prost_duration = Duration {
-                    seconds: -prost_duration.seconds,
-                    nanos: -prost_duration.nanos,
-                };
-
-                prop_assert!(
-                    matches!(
-                        time::Duration::try_from(neg_prost_duration),
-                        Err(DurationError::NegativeDuration(d)) if d == std_duration,
-                    )
-                )
-            }
+
+            assert!(matches!(
+                time::Duration::try_from(neg_prost_duration),
+                Err(DurationError::NegativeDuration(d)) if d == std_duration,
+            ))
         }
     }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
 
     #[cfg(feature = "std")]
     #[test]

prost-types/src/timestamp.rs

@@ -231,6 +231,27 @@ impl fmt::Display for Timestamp {
         datetime::DateTime::from(*self).fmt(f)
     }
 }
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    #[cfg(feature = "std")]
+    #[kani::proof]
+    #[kani::unwind(3)]
+    fn check_timestamp_roundtrip_via_system_time() {
+        let seconds = kani::any();
+        let nanos = kani::any();
+
+        let mut timestamp = Timestamp { seconds, nanos };
+        timestamp.normalize();
+
+        if let Ok(system_time) = std::time::SystemTime::try_from(timestamp) {
+            assert_eq!(Timestamp::from(system_time), timestamp);
+        }
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -248,18 +269,6 @@ mod tests {
         ) {
             prop_assert_eq!(SystemTime::try_from(Timestamp::from(system_time)).unwrap(), system_time);
         }
-
-        #[test]
-        fn check_timestamp_roundtrip_via_system_time(
-            seconds in i64::arbitrary(),
-            nanos in i32::arbitrary(),
-        ) {
-            let mut timestamp = Timestamp { seconds, nanos };
-            timestamp.normalize();
-            if let Ok(system_time) = SystemTime::try_from(timestamp) {
-                prop_assert_eq!(Timestamp::from(system_time), timestamp);
-            }
-        }
     }
 
     #[cfg(feature = "std")]