fix: Make kani attribute nameres work with generic args having ::

[ShoyuVanilla]

I found this while working on model-checking/verify-rust-std#382.

When you try to add #[proof_for_contract(Rc::<MaybeUninit<T>, A>::assume_init)] to a proof for this function https://doc.rust-lang.org/1.90.0/src/alloc/rc.rs.html#1211, kani fails to resolve Rc::<MaybeUninit<T>, A>::assume_init, as it compares the last two parts of the path string,

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

Lines 783 to 797 in e0316ff

	fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str) -> bool {
	let parts: Vec<&str> = item_path.split("::").collect();
	if parts.len() < 2 {
	return false;
	}
	let actual_last_two =
	format!("{}{}{}{}", "::", parts[parts.len() - 2], "::", parts[parts.len() - 1]);
	let last_two = format!("{}{}{}", generic_args, "::", name);
	// The last two components of the item_path should be the same as ::{generic_args}::{name}
	last_two == actual_last_two
	}

But rustc's TyCtxt::def_path_str emits the path rc::Rc::<core::mem::MaybeUninit<T>, A>::assmue_init even if there's use core::mem::MaybeUninit in scope. So the last two parts of it is ::MaybeUninit<T>, A>::assmue_init, instead of being ::<core::mem::MaybeUninit<T>, A>::assmue_init, and the resolution fails.

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

[ShoyuVanilla]

This is to fix argument passings when it is prefixed with module paths like foo::bar::Baz::<..>

[ShoyuVanilla]

We strip whitespaces from the generic args here:

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

Lines 589 to 591 in e0316ff

	fn generic_args_to_string<T: ToTokens>(args: &T) -> String {
	args.to_token_stream().to_string().chars().filter(|c| !c.is_whitespace()).collect::<String>()
	}

So multiple args like <T, A> become <T,A>. This is necessary for matching those things.