Do not assert dependency contracts for calls made by contract clauses

Contracts of dependencies are asserted by default (#3802) as an aid for
detecting API misuse in user code. Calls made while evaluating
*contract clauses*, however, are specification-level plumbing: clause
expressions compute a predicate over pre-/post-states, and the
functions they call are best executed with their exact semantics.
Re-asserting dependency contracts inside every clause evaluation
multiplies verification cost - clauses of contract-dense code (e.g. the
Rust standard library in model-checking/verify-rust-std) routinely call
contracted functions like NonNull::as_ptr, paying the assert-closure
overhead per clause instance - without checking any user code.

Extend the clause-context dispatch introduced for check modes to assert
mode: calls to a contracted dependency that occur during clause
evaluation now execute the original body (mode 0). The body remains
fully inlined and UB-checked; only the requires/ensures assertions of
the *callee's* contract are skipped in this context.

The new regression test checks both halves: a clause calling a
contracted function with precondition-violating (but well-defined)
arguments verifies successfully, while the same misuse in user code is
still caught.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

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

@@ -453,20 +453,35 @@ impl FunctionWithContractPass {
 
         let span = mode_call.span(new_body.blocks());
         let mode_const = new_body.new_uint_operand(mode as _, UintTy::U8, span);
-        if matches!(mode, ContractMode::SimpleCheck | ContractMode::RecursiveCheck) {
-            // While the harness is checking the contract of this function,
-            // the function may also be called from *contract clauses* of
-            // other functions in the harness's call graph (e.g. a
-            // postcondition mentioning `NonNull::as_ptr` evaluated while
-            // `as_ptr` itself is under verification). Such calls must not be
-            // dispatched to the check closure: they would consume the single
-            // top-level contract check and run write-set instrumentation in
-            // the clause's context. Dispatch them to the original body
-            // instead (exact semantics; unlike dispatching to the contract
-            // replacement this does not require the return type to implement
-            // Arbitrary), by computing the mode at runtime as
-            // `mode * (1 - in_contract_clause())`, which yields
-            // `ORIGINAL` (0) during clause evaluation and `mode` otherwise.
+        if matches!(
+            mode,
+            ContractMode::SimpleCheck | ContractMode::RecursiveCheck | ContractMode::Assert
+        ) {
+            // Calls occurring during the evaluation of *contract clauses* of
+            // other functions are dispatched to the original body (mode 0,
+            // exact semantics) rather than the mode selected for normal
+            // calls, by computing the mode at runtime as
+            // `mode * (1 - in_contract_clause())`:
+            //
+            // * For check modes: while the harness is checking the contract
+            //   of this function, the function may also be called from
+            //   contract clauses of other functions in the harness's call
+            //   graph (e.g. a postcondition mentioning `NonNull::as_ptr`
+            //   evaluated while `as_ptr` itself is under verification). Such
+            //   calls must not be dispatched to the check closure: they
+            //   would consume the single top-level contract check and run
+            //   write-set instrumentation in the clause's context. (Unlike
+            //   dispatching to the contract replacement, the original body
+            //   does not require the return type to implement Arbitrary.)
+            //
+            // * For assert mode: asserting the contracts of dependencies
+            //   (the default since #3802) is an aid for detecting API misuse
+            //   in user code; re-asserting them for calls made by *contract
+            //   clauses* checks specification-level plumbing at a
+            //   multiplicative cost. Clause evaluation is meant to compute a
+            //   predicate over the pre-/post-states, and the functions it
+            //   calls are best executed with their exact semantics (their
+            //   bodies remain fully inlined and UB-checked either way).
             let in_clause_instance =
                 Instance::resolve(self.in_clause_fn.unwrap(), &GenericArgs(vec![])).unwrap();
             let in_clause_local = new_body.new_local(Ty::bool_ty(), span, Mutability::Mut);

tests/expected/function-contract/clause_context_no_assert.expected

@@ -0,0 +1,4 @@
+Failed Checks: x >= 10
+
+Verification failed for - check_misuse_still_caught
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/function-contract/clause_context_no_assert.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Contracts of dependencies are asserted by default (#3802) as an aid for
+//! detecting API misuse in user code. Calls made while evaluating *contract
+//! clauses*, however, execute the original body (exact semantics, still fully
+//! UB-checked) without re-asserting the callee's contract: clause expressions
+//! are specifications, and asserting specification-level plumbing multiplies
+//! verification cost without checking user code.
+//!
+//! `one`'s postcondition below calls `plus_one(0)`, which violates
+//! `plus_one`'s (overly strict) precondition but is well-defined: the clause
+//! must evaluate to true without a contract-assertion failure. The same
+//! misuse in *user code* (`check_misuse`) must still be caught.
+
+#[kani::requires(x >= 10)]
+fn plus_one(x: u8) -> u8 {
+    x.wrapping_add(1)
+}
+
+#[kani::ensures(|result| *result == plus_one(0))]
+fn one() -> u8 {
+    1
+}
+
+#[kani::proof]
+fn check_clause_call_not_asserted() {
+    let _ = one();
+}
+
+#[kani::proof]
+fn check_misuse_still_caught() {
+    let _ = plus_one(0);
+}