Remove unused msg parameter from any_where (rust-lang#2257)

Author: zhassan-aws

CHANGELOG

@@ -0,0 +1,21 @@
+# Changelog
+
+This file contains notable changes (e.g. breaking changes, major changes, etc.) in Kani releases.
+
+This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
+
+## [0.23.0]
+
+### **Breaking Changes**
+
+- The second parameter in the `kani::any_where` function (`_msg: &'static str`) was removed to make the function more ergonomic to use.
+We suggest moving the explanation for why the assumption is introduced into a comment.
+For example, the following code:
+```rust
+    let len: usize = kani::any_where(|x| *x < 5, "Restrict the length to a value less than 5");
+```
+should be replaced by:
+```rust
+    // Restrict the length to a value less than 5
+    let len: usize = kani::any_where(|x| *x < 5);
+```

Cargo.toml

@@ -14,7 +14,7 @@ repository = "https://github.com/model-checking/kani"
 documentation = "https://model-checking.github.io/kani/"
 homepage = "https://github.com/model-checking/kani"
 # N.B. Cargo.* is included automatically:
-include = ["/src", "/build.rs", "/rust-toolchain.toml", "/LICENSE-*", "/README.md"]
+include = ["/src", "/build.rs", "/rust-toolchain.toml", "/LICENSE-*", "/README.md", "/CHANGELOG"]
 
 [dependencies]
 anyhow = "1"

library/kani/src/lib.rs

@@ -112,23 +112,22 @@ pub fn any<T: Arbitrary>() -> T {
 /// This creates a symbolic *valid* value of type `T`.
 /// The value is constrained to be a value accepted by the predicate passed to the filter.
 /// You can assign the return value of this function to a variable that you want to make symbolic.
-/// The explanation field gives a mechanism to explain why the assumption is required for the proof.
 ///
 /// # Example:
 ///
 /// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
 /// under all possible `NonZeroU8` input values between 0 and 12.
 ///
 /// ```rust
-/// let inputA = kani::any_where::<std::num::NonZeroU8>(|x| *x < 12, "explanation");
+/// let inputA = kani::any_where::<std::num::NonZeroU8>(|x| *x < 12);
 /// fn_under_verification(inputA);
 /// ```
 ///
 /// Note: This is a safe construct and can only be used with types that implement the `Arbitrary`
 /// trait. The Arbitrary trait is used to build a symbolic value that represents all possible
 /// valid values for type `T`.
 #[inline(always)]
-pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F, _msg: &'static str) -> T {
+pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
     let result = T::any();
     assume(f(&result));
     result

scripts/ci/copyright-exclude

@@ -6,6 +6,7 @@
 .props
 .public.key
 Cargo.lock
+CHANGELOG
 LICENSE-APACHE
 LICENSE-MIT
 editorconfig

tests/kani/Assume/main.rs

@@ -10,6 +10,7 @@ fn main() {
 
 #[kani::proof]
 fn verify_any_where() {
-    let i: i32 = kani::any_where(|x| *x < 10, "Only single digit values are legal");
+    // Only single digit values are legal
+    let i: i32 = kani::any_where(|x| *x < 10);
     assert!(i < 20);
 }

tools/build-kani/src/main.rs

@@ -104,7 +104,7 @@ fn bundle_kani(dir: &Path) -> Result<()> {
     // 5. Record the exact toolchain we use
     std::fs::write(dir.join("rust-toolchain-version"), env!("RUSTUP_TOOLCHAIN"))?;
 
-    // 5. Include a licensing note
+    // 6. Include a licensing note
     cp(Path::new("tools/build-kani/license-notes.txt"), dir)?;
 
     Ok(())