Support for inductively verifying contracts of recursive functions

[JustusAdam]

This adds support for verifying the contracts of recursive functions inductively.

The idea is quite simple. We use a global variable to track whether we're reentering a function and depending on that value we either continue with checking the contract or assume the hypothesis by using its replacement.

The precise mechanism that I implemented is explained in the documentation here

Resolves #2724

Open Question: to facilitate induction the return type of the function must implement kani::Arbitrary. Since we can't discriminate between recursive and non-recursive functions in the proc-macro this means that this applies to all functions with contracts, not just recursive ones. This may be an unacceptable restriction. We could consider making inductive verification explicit with an annotation like #[kani::inductive] or conversely make inductive the default and let users opt-out with #[kani::no_inductive]. This is now tracked in #2823

I had to remove the names of the functions in which the messages occur in the test cases, since they are now generated, hard to read names

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

[celinval]

BTW, I have the following pre-commit hook to avoid all the whitespace issues:

#!/usr/bin/env bash
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
set -e

# source: https://github.com/awslabs/git-secrets
git secrets --pre_commit_hook -- "$@"

TOP_DIR=$(git rev-parse --show-toplevel)

check_rust_style() {
    pushd ${TOP_DIR}
    ./scripts/kani-fmt.sh --check
    cargo clippy --all -- -D warnings
    popd
}

check_rust_style

[zhassan-aws]

Nice! A few comments/questions.

[JustusAdam]

Hmm, my formatting was wrong even though I ran kani-fmt.sh

[zhassan-aws]

Thanks @JustusAdam! It's great to be able to support recursive functions!

[JustusAdam]

Thanks @JustusAdam! It's great to be able to support recursive functions!

Thanks. Yeah I'll do that.