Gate quantifiers behind an experimental feature (#4141)

This PR put Quantifiers under unstable features. User must use the flag
"-Z quantifiers" to enable it.

Resolves #4134

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

---------

Co-authored-by: Carolyn Zech <[email protected]>

Author: thanhnguyen-aws

kani_metadata/src/unstable.rs

@@ -99,6 +99,8 @@ pub enum UnstableFeature {
     /// Allow replacing certain items with stubs (mocks).
     /// See [RFC-0002](https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html)
     Stubbing,
+    /// Enable quantifiers [RFC 10](https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html)
+    Quantifiers,
     /// Automatically check that uninitialized memory is not used.
     UninitChecks,
     /// Enable an unstable option or subcommand.

library/kani_core/src/lib.rs

@@ -627,6 +627,11 @@ macro_rules! kani_intrinsics {
                 assert!(cond, "{}", msg);
             }
 
+            #[crate::kani::unstable_feature(
+                feature = "quantifiers",
+                issue = 2546,
+                reason = "experimental quantifiers"
+            )]
             #[inline(never)]
             #[kanitool::fn_marker = "ForallHook"]
             pub fn kani_forall<T, F>(lower_bound: T, upper_bound: T, predicate: F) -> bool
@@ -636,6 +641,11 @@ macro_rules! kani_intrinsics {
                 predicate(lower_bound)
             }
 
+            #[crate::kani::unstable_feature(
+                feature = "quantifiers",
+                issue = 2546,
+                reason = "experimental quantifiers"
+            )]
             #[inline(never)]
             #[kanitool::fn_marker = "ExistsHook"]
             pub fn kani_exists<T, F>(lower_bound: T, upper_bound: T, predicate: F) -> bool

tests/expected/quantifiers/assert_with_exists_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn exists_assert_harness() {

tests/expected/quantifiers/assert_with_exists_pass.rs

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn exists_assert_harness() {

tests/expected/quantifiers/assert_with_forall_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn forall_assert_harness() {

tests/expected/quantifiers/assert_with_forall_pass.rs

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn forall_assert_harness() {

tests/expected/quantifiers/assume_with_exists_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn exists_assume_harness() {

tests/expected/quantifiers/contracts_fail.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Z quantifiers
 
 /// Copy only first 7 elements and left the last one unchanged.
 #[kani::ensures(|ret| { unsafe{

tests/expected/quantifiers/quantifier_with_no_external_variable.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// kani-flags: -Z quantifiers
 /// Quantifier with no external variable in the closure
 
 #[kani::proof]

tests/kani/Quantifiers/array.rs

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn vec_assert_forall_harness() {