Can't write contracts for a method defined inside more than one impl block

[carolynzech]

I tried this code:

struct NonZero<T>(T);

impl NonZero<u32> {
    #[kani::requires(true)]
    fn unchecked_mul(self, x: u32) {}
}

impl NonZero<i32> {
    #[kani::requires(true)]
    fn unchecked_mul(self, x: i32) {}
}

#[kani::proof_for_contract(NonZero::unchecked_mul)]
fn verify_unchecked_mul() {
    let x: NonZero<i32> = NonZero(-1);
    x.unchecked_mul(-2);
}

using the following command line invocation:

cargo kani -Z function-contracts

with Kani version: 0.56

I expected to see this happen: verification success

Instead, this happened: explanation

error: The function specified in the `proof_for_contract` attribute, `NonZero::unchecked_mul`, was not found.
       Make sure the function is reachable from the harness.
  --> src/lib.rs:63:1
   |
63 | #[kani::proof_for_contract(NonZero::unchecked_mul)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)

error: could not compile `playground` (lib) due to 1 previous error; 2 warnings emitted
error: Failed to execute cargo (exit status: 101). Found 1 compilation errors.

[carolynzech]

I did some debugging. The function that throws the error:

kani/kani-compiler/src/kani_middle/attributes.rs

Lines 479 to 488 in db1c5fe

	pub fn check_proof_for_contract(&self, reachable_functions: &HashSet<DefId>) {
	if let Some((symbol, function, span)) = self.interpret_for_contract_attribute() {
	if !reachable_functions.contains(&function) {
	let err_msg = format!(
	"The function specified in the `proof_for_contract` attribute, `{symbol}`, was not found.\
	\nMake sure the function is reachable from the harness."
	);
	self.tcx.dcx().span_err(span, err_msg);
	}
	}

calls interpret_for_contract_attribute:

kani/kani-compiler/src/kani_middle/attributes.rs

Lines 235 to 249 in db1c5fe

	pub(crate) fn interpret_for_contract_attribute(&self) -> Option<(Symbol, DefId, Span)> {
	self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| {
	let name = expect_key_string_value(self.tcx.sess, target).ok()?;
	self.resolve_from_mod(name.as_str())
	.map(|ok| (name, ok, target.span))
	.map_err(|resolve_err| {
	self.tcx.dcx().span_err(
	target.span,
	format!(
	"Failed to resolve checking function {} because {resolve_err}",
	name.as_str()
	),
	)
	})
	.ok()

which finds the DefId for the target NonZero::unchecked_mul. However, there are two unchecked_mul methods, so the function just returns the first one it finds (the unsigned implementation), but only the signed implementation is reachable from the harness, so we throw an error.

[carolynzech]

This example is based on the real NonZero implementation in the standard library. A closer rendition of how NonZero is actually instantiated would be:

struct NonZero<T>(T);

macro_rules! nonzero_integer {
    (
        Self = $Ty:ident,
        Primitive = $signedness:ident $Int:ty
    ) => {
        pub type $Ty = NonZero<$Int>;

        impl NonZero<$Int> {
            #[kani::requires(true)]
            fn unchecked_mul(self, x: $Int) {}
        }
    };

    (
        Self = $Ty:ident,
        Primitive = unsigned $Int:ty
    ) => {
        nonzero_integer! {
            Self = $Ty,
            Primitive = unsigned $Int
        }
    };

    (
        Self = $Ty:ident,
        Primitive = signed $Int:ty
    ) => {
        nonzero_integer! {
            Self = $Ty,
            Primitive = signed $Int
        }
    }
}

nonzero_integer! {
    Self = UnsignedNonZero,
    Primitive = unsigned u32
}

nonzero_integer! {
    Self = SignedNonZero,
    Primitive = signed i32
}

#[kani::proof_for_contract(NonZero::unchecked_mul)]
fn verify_unchecked_mul() {
    let x: NonZero<i32> = NonZero(-1);
    x.unchecked_mul(-2);
}

but this ends up expanding to the minimal example I originally posted.