Move an owned receiver into the replace closure so const fns with contracts compile

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

@@ -185,6 +185,15 @@ impl<'a> ContractConditionsHandler<'a> {
             .unwrap_or(false)
     }
 
+    /// Return whether the original function takes `self` by value (an owned
+    /// receiver), e.g. `fn into_inner(self)`.
+    pub fn has_owned_receiver(&self) -> bool {
+        let first_arg = self.annotated_fn.sig.inputs.first();
+        first_arg
+            .map(|arg| matches!(arg, FnArg::Receiver(syn::Receiver { reference: None, .. },)))
+            .unwrap_or(false)
+    }
+
     /// Generate argument re-definitions for arguments.
     ///
     /// This is used so Kani doesn't think that modifying a local argument value is a side effect,

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

@@ -528,6 +528,7 @@ mod replace;
 mod shared;
 
 const INTERNAL_RESULT_IDENT: &str = "result_kani_internal";
+const INTERNAL_SELF_IDENT: &str = "self_kani_internal";
 
 pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
     contract_main(attr, item, ContractConditionsType::Requires)

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

@@ -10,6 +10,7 @@ use syn::{Block, Stmt};
 
 use super::{
     ContractConditionsData, ContractConditionsHandler, ContractMode, INTERNAL_RESULT_IDENT,
+    INTERNAL_SELF_IDENT,
     helpers::*,
     shared::{build_ensures, split_for_remembers, try_as_result_assign},
 };
@@ -58,6 +59,10 @@ impl<'a> ContractConditionsHandler<'a> {
     fn split_replace(&self, mut stmts: Vec<Stmt>) -> (Vec<Stmt>, Vec<Stmt>) {
         // Pop the return result since we always re-add it.
         stmts.pop();
+        // Likewise the owned-receiver move (when present); re-added at the tail.
+        if stmts.last().is_some_and(is_replace_receiver_move) {
+            stmts.pop();
+        }
 
         let idx = stmts
             .iter()
@@ -81,6 +86,17 @@ impl<'a> ContractConditionsHandler<'a> {
     /// `use_nondet_result` will only be true if this is the first time we are
     /// generating a replace function.
     fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream {
+        // `self` cannot be re-bound like the arguments in `arg_redefinitions`
+        // (it is a keyword), so the replace closure would only borrow an owned
+        // receiver, leaving the annotated function's own scope to drop it, which
+        // `const fn`s whose receiver type has a destructor reject (E0493). Move
+        // it into the closure at the tail of the body, after every borrow of
+        // `self` (preconditions, remembers, modifies havocs, postconditions), so
+        // any drop lands outside const-checking.
+        let recv_move = self.has_owned_receiver().then(|| {
+            let self_repl = Ident::new(INTERNAL_SELF_IDENT, Span::call_site());
+            quote!(let #self_repl = self;)
+        });
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 let Self { attr_copy, .. } = self;
@@ -91,6 +107,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     #assert_bracketed
                     #(#before)*
                     #(#after)*
+                    #recv_move
                     #result
                 })
             }
@@ -107,6 +124,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#rest_of_before)*
                     #(#after)*
                     kani::assume(#ensures_bracketed);
+                    #recv_move
                     #result
                 })
             }
@@ -128,6 +146,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#before)*
                     #(#havoc_stmts)*
                     #(#after)*
+                    #recv_move
                     #result
                 })
             }
@@ -161,6 +180,30 @@ impl<'a> ContractConditionsHandler<'a> {
     }
 }
 
+/// Is this the owned-receiver move statement (`let self_kani_internal = self;`)
+/// that [`ContractConditionsHandler::expand_replace_body`] emits at the tail of a
+/// replace body so the receiver drops inside the closure (see that method).
+fn is_replace_receiver_move(stmt: &syn::Stmt) -> bool {
+    let syn::Stmt::Local(syn::Local {
+        pat: syn::Pat::Ident(syn::PatIdent { ident, .. }),
+        init: Some(syn::LocalInit { expr, diverge: None, .. }),
+        ..
+    }) = stmt
+    else {
+        return false;
+    };
+    // Match the exact statement `expand_replace_body` emits: a bind of
+    // `self_kani_internal` to the bare receiver `self`, and nothing else.
+    ident == INTERNAL_SELF_IDENT
+        && matches!(
+            expr.as_ref(),
+            syn::Expr::Path(p)
+                if p.qself.is_none()
+                    && p.path.segments.len() == 1
+                    && p.path.segments[0].ident == "self"
+        )
+}
+
 /// Is this statement `let result_kani_internal : <...> = kani::any_modifies();`.
 fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool {
     let Some(syn::LocalInit { diverge: None, expr: e, .. }) = try_as_result_assign(stmt) else {

tests/expected/function-contract/const_fn_owned_receiver_fail.expected

@@ -0,0 +1 @@
+VERIFICATION:- FAILED

tests/expected/function-contract/const_fn_owned_receiver_fail.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! A deliberately violated ensures on a `const fn` with an owned `Drop`
+//! receiver must still fail: the receiver-move in the replace body must not
+//! weaken checking. `Owned` wraps a `u32` (no `Box` deref in the ensures) so
+//! the only failing check is the false postcondition itself.
+
+struct Owned(u32);
+
+impl Drop for Owned {
+    fn drop(&mut self) {}
+}
+
+impl Owned {
+    #[kani::ensures(|result: &Owned| result.0 == old(self.0) + 1)]
+    const fn identity(self) -> Owned {
+        self
+    }
+}
+
+#[kani::proof_for_contract(Owned::identity)]
+fn harness() {
+    let v: u32 = kani::any_where(|v: &u32| *v < 100);
+    let _ = Owned(v).identity();
+}

tests/kani/FunctionContracts/const_fn_owned_receiver.rs

@@ -0,0 +1,54 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zstubbing
+
+//! A contract on a `const fn` that takes `self` by value must compile and
+//! verify when `Self` has a destructor. The replace stub used to leave `self`
+//! to drop in the annotated function's own scope, which `const fn`s reject
+//! (E0493); the other arguments are already covered by the #3667 reassignments.
+//!
+//! `Owned` has an explicit `Drop` (so it is a needs-drop receiver, like a field
+//! of `Box`), but wraps a `u32` so the replace-mode harness can havoc it. The
+//! body moves `self` into the return without dropping it, so it is itself
+//! const-legal; the only drop of `self` previously came from the contract.
+
+struct Owned(u32);
+
+impl Drop for Owned {
+    fn drop(&mut self) {}
+}
+
+impl kani::Arbitrary for Owned {
+    fn any() -> Self {
+        Owned(kani::any())
+    }
+}
+
+impl Owned {
+    #[kani::requires(self.0 < 100)]
+    #[kani::ensures(|result: &Owned| result.0 == old(self.0))]
+    const fn identity(self) -> Owned {
+        self
+    }
+}
+
+/// Check mode: compiles the full contract expansion (including the replace arm
+/// that previously hit E0493) and verifies the contract against the body.
+#[kani::proof_for_contract(Owned::identity)]
+fn check_owned_receiver_const_fn() {
+    let out = Owned(kani::any_where(|v: &u32| *v < 100)).identity();
+    assert!(out.0 < 100);
+}
+
+fn caller(o: Owned) -> Owned {
+    o.identity()
+}
+
+/// Replace mode: stubs `identity` with its contract, exercising the replace
+/// closure (with the tail receiver-move) end to end.
+#[kani::proof]
+#[kani::stub_verified(Owned::identity)]
+fn check_owned_receiver_replace() {
+    let out = caller(Owned(kani::any_where(|v: &u32| *v < 100)));
+    assert!(out.0 < 100);
+}