RFC: Function stubbing

[aaronbembenek-aws]

This is a tracking issue for the RFC function_stubbing.

The goal is to allow users to specify that some functions should be replaced by mock functions (stubs) during verification. Although the current focus is on functions, the hope is that this mechanism might in the future be extended to other features (like methods and types).

The need for stubs is twofold:

1. Users might need to stub functions containing features that Kani does not support, such as inline assembly.
2. Users might need to stub functions containing code that Kani supports in principle, but which in practice leads to bad verification performance.

There are questions to resolve:

1. What should be the user experience? How and where should users specify which stubs to use?
2. Should stubs be applied consistently across all harnesses or should they be specific to a harness (i.e., different harnesses can use different stubs)?