make asserting contracts the default

kani-compiler/src/args.rs

@@ -36,6 +36,9 @@ pub enum ReachabilityType {
 /// with. Usually stored in and accessible via [`crate::kani_queries::QueryDb`].
 #[derive(Debug, Default, Clone, clap::Parser)]
 pub struct Arguments {
+    /// Option used to enable asserting function contracts.
+    #[clap(long)]
+    pub no_assert_contracts: bool,
     /// Option name used to enable assertion reachability checks.
     #[clap(long = "assertion-reach-checks")]
     pub check_assertion_reachability: bool,

kani-compiler/src/kani_middle/transform/contracts.rs

@@ -273,8 +273,8 @@ pub struct FunctionWithContractPass {
     check_fn: Option<InternalDefId>,
     /// Functions that should be stubbed by their contract.
     replace_fns: HashSet<InternalDefId>,
-    /// Should we interpret contracts as assertions? (true iff the contracts-as-assertions option is passed)
-    are_contracts_asserted: bool,
+    /// Should we interpret contracts as assertions? (true iff the no-assert-contracts option is not passed)
+    assert_contracts: bool,
     /// Functions annotated with contract attributes will contain contract closures even if they
     /// are not to be used in this harness.
     /// In order to avoid bringing unnecessary logic, we clear their body.
@@ -354,10 +354,7 @@ impl FunctionWithContractPass {
             FunctionWithContractPass {
                 check_fn,
                 replace_fns,
-                are_contracts_asserted: queries
-                    .args()
-                    .unstable_features
-                    .contains(&"contracts-as-assertions".to_string()),
+                assert_contracts: !queries.args().no_assert_contracts,
                 unused_closures: Default::default(),
                 run_contract_fn,
             }
@@ -461,7 +458,7 @@ impl FunctionWithContractPass {
                 }
             } else if self.replace_fns.contains(&fn_def_id) {
                 ContractMode::Replace
-            } else if self.are_contracts_asserted {
+            } else if self.assert_contracts {
                 ContractMode::Assert
             } else {
                 ContractMode::Original

kani-driver/src/args/mod.rs

@@ -309,6 +309,10 @@ pub struct VerificationArgs {
     )]
     pub synthesize_loop_contracts: bool,
 
+    /// Do not assert the function contracts of dependencies. Requires -Z function-contracts.
+    #[arg(long)]
+    pub no_assert_contracts: bool,
+
     //Harness Output into individual files
     #[arg(long, hide_short_help = true)]
     pub output_into_files: bool,
@@ -702,6 +706,17 @@ impl ValidateArgs for VerificationArgs {
                 ),
             ));
         }
+
+        if !self.is_function_contracts_enabled() && self.no_assert_contracts {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!(
+                    "The `--no-assert-contracts` option requires `-Z {}`.",
+                    UnstableFeature::FunctionContracts
+                ),
+            ));
+        }
+
         Ok(())
     }
 }
@@ -1000,4 +1015,11 @@ mod tests {
         let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
     }
+
+    #[test]
+    fn check_no_assert_contracts() {
+        let args = "kani input.rs --no-assert-contracts".split_whitespace();
+        let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
+        assert_eq!(err.kind(), ErrorKind::MissingRequiredArgument);
+    }
 }

kani-driver/src/call_cargo.rs

@@ -188,6 +188,9 @@ crate-type = ["lib"]
         if let Some(backend_arg) = self.backend_arg() {
             pkg_args.push(backend_arg);
         }
+        if self.args.no_assert_contracts {
+            pkg_args.push("--no-assert-contracts".into());
+        }
 
         let mut found_target = false;
         let packages = self.packages_to_verify(&self.args, &metadata)?;

kani-driver/src/call_single_file.rs

@@ -93,7 +93,7 @@ impl KaniSession {
         Ok(())
     }
 
-    /// Create a compiler option that represents the reachability mod.
+    /// Create a compiler option that represents the reachability mode.
     pub fn reachability_arg(&self) -> String {
         to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())])
     }
@@ -152,6 +152,10 @@ impl KaniSession {
             flags.push("--print-llbc".into());
         }
 
+        if self.args.no_assert_contracts {
+            flags.push("--no-assert-contracts".into());
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
 
         flags

kani_metadata/src/unstable.rs

@@ -85,8 +85,6 @@ pub enum UnstableFeature {
     FunctionContracts,
     /// Enable loop contracts [RFC 12](https://model-checking.github.io/kani/rfc/rfcs/0012-loop-contracts.html)
     LoopContracts,
-    /// Interpret function contracts as assertions. (Requires function-contracts option).
-    ContractsAsAssertions,
     /// Memory predicate APIs.
     MemPredicates,
     /// Automatically check that no invalid value is produced which is considered UB in Rust.

library/kani_macros/src/sysroot/contracts/mod.rs

@@ -117,9 +117,10 @@
 //! We register this closure as `#[kanitool::recursion_check = "__kani_recursion_..."]`.
 //!
 //! ## Assert closure
-//! Kani has an option to interpret contracts as assertions.
-//! To support that option, we generate a closure that asserts preconditions and postconditions.
-//! This option is especially useful for verifying that a function does not violate the contracts of its dependencies.
+//! By default, if we are not checking the function's contract or stubbing it,
+//! (i.e., if we are not using the check or replace closures),
+//! we use its assert closure, which asserts both preconditions and postconditions.
+//! This behavior is useful for verifying that a function does not violate the contracts of its dependencies.
 //! For example:
 //! ```ignore
 //!  #[kani::requires(x >= 0)]
@@ -130,7 +131,7 @@
 //!  #[kani::requires(x > 0)]
 //!  fn bar(x: i32) { }
 //! ```
-//! If we call foo(0), we would satisfy the check closure, since we satisfy foo's precondition.
+//! If we call foo(0), we would satisfy foo's check closure, since we satisfy foo's precondition.
 //! However, we would violate bar's precondition that x > 0.
 //! By using bar's assert closure instead of its original body, we can assert that callers of bar respect its contract
 //! and catch this issue.

tests/expected/function-contract/as-assertions/assert-postconditions.rs

@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions
+// kani-flags: -Zfunction-contracts
 
-// Test -Zcontracts-as-assertions for postconditions.
+// Test -Zfunction-contracts for asserting postconditions.
 
 #[kani::requires(*add_three_ptr < 100)]
 #[kani::modifies(add_three_ptr)]
@@ -22,7 +22,6 @@ fn add_one(add_one_ptr: &mut u32) {
     *add_one_ptr += 1;
 }
 
-// -Zcontracts-as-assertions introduces this failure; without it, add_two's and add_one's contracts are ignored.
 #[kani::proof_for_contract(add_three)]
 fn prove_add_three() {
     let mut i = kani::any();

tests/expected/function-contract/as-assertions/assert-preconditions.rs

@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions
+// kani-flags: -Zfunction-contracts
 
-// Test -Zcontracts-as-assertions for preconditions.
+// Test -Zfunction-contracts for asserting preconditions.
 
 #[kani::requires(*ptr < 100)]
 #[kani::ensures(|result| old(*ptr + 3) == *ptr)]

tests/expected/function-contract/as-assertions/loops.rs

@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions
+// kani-flags: -Zfunction-contracts
 
-// Check that the -Zcontracts-as-assertions option asserts preconditions and postconditions correctly
+// Check that the -Zfunction-contracts option asserts preconditions and postconditions correctly
 // when the body of the function has a loop.
 // This code is taken from function-contracts/gcd_success.rs
 

tests/expected/function-contract/as-assertions/precedence.rs

@@ -1,9 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions
+// kani-flags: -Zfunction-contracts
 
 // If a function is the target of a proof_for_contract or stub_verified, we should defer to the contract handling for those modes.
-// i.e., test that -Zcontracts-as-assertions does not override the contract handling for proof_for_contract and stub_verified.
 
 #[kani::modifies(add_three_ptr)]
 #[kani::requires(*add_three_ptr < 100)]

tests/kani/FunctionContracts/no-assert.rs

@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts --no-assert-contracts
+
+// Check that the -no-assert-contracts option disables the default behavior of asserting contracts of dependencies.
+
+#[kani::requires(*add_three_ptr < 100)]
+#[kani::modifies(add_three_ptr)]
+fn add_three(add_three_ptr: &mut u32) {
+    *add_three_ptr += 1;
+    add_two(add_three_ptr);
+}
+
+#[kani::ensures(|_| old(*add_two_ptr + 1) == *add_two_ptr)] // incorrect -- should be old(*add_two_ptr + 2)
+fn add_two(add_two_ptr: &mut u32) {
+    *add_two_ptr += 1;
+    add_one(add_two_ptr)
+}
+
+#[kani::ensures(|_| old(*add_one_ptr + 1) == *add_one_ptr)] // correct -- assertion should always succeed
+fn add_one(add_one_ptr: &mut u32) {
+    *add_one_ptr += 1;
+}
+
+// With --no-assert-contracts, add_two's and add_one's contracts are ignored, so verification should succeed.
+#[kani::proof_for_contract(add_three)]
+fn prove_add_three() {
+    let mut i = kani::any();
+    add_three(&mut i);
+}