Verify contracts/stubs for generic types with multiple inherent implementations

[carolynzech]

Extends Kani's contracts/stubbing logic to handle simple paths with generic arguments. I'll explain the changes commit-by-commit:

Commit 690ba97: Error for multiple implementations

Prior to this PR, given the code from #3773:

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);
}

When resolving the target, Kani would return the first unchecked_mul implementation that it found for NonZero. If that happens to be the u32 implementation, then we get an error later that the target NonZero::unchecked_mul isn't reachable from the harness, which is confusing because the harness does call unchecked_mul.

The real problem is that the target needs to specify which implementation it wants to verify, so now we throw this error:

Failed to resolve checking function NonZero::unchecked_mul because there are multiple implementations of unchecked_mul in struct `NonZero`. Found:
       NonZero::<u32>::unchecked_mul
       NonZero::<i32>::unchecked_mul
 |
 | #[kani::proof_for_contract(NonZero::unchecked_mul)]
 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 |
   = help: Replace NonZero::unchecked_mul with a specific implementation.

Commit 62b66de: Path resolution for simple paths with generic arguments

If the user took our suggestion and changed their proof for contract to be NonZero::<i32>::unchecked_mul, they would still get the same error. The syn::Path is this:

Path {
    leading_colon: None,
    segments: [
        PathSegment {
            ident: Ident(
                NonZero,
            ),
            arguments: PathArguments::AngleBracketed {
                colon2_token: Some(
                    PathSep,
                ),
                lt_token: Lt,
                args: [
                    GenericArgument::Type(
                        Type::Path {
                            qself: None,
                            path: Path {
                                leading_colon: None,
                                segments: [
                                    PathSegment {
                                        ident: Ident(
                                            i32,
                                        ),
                                        arguments: PathArguments::None,
                                    },
                                ],
                            },
                        },
                    ),
                ],
                gt_token: Gt,
            },
        },
        PathSep,
        PathSegment {
            ident: Ident(
                unchecked_mul,
            ),
            arguments: PathArguments::None,
        },
    ],

Kani's path resolution would skip over the PathArguments for the base type NonZero, so it would still try to find NonZero::unchecked_mul and run into the same problem. So, this commit adds a base_path_args field to our Path representation to store these arguments, which we use to select the specified implementation.

Resolves #3773

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

[zhassan-aws]

Nice, thanks!