Add contract support to intrinsics

[celinval]

Requested feature: Enable users to verify and stub compiler intrinsics with Kani contract
Use case: Intrinsics are functions implemented in the compiler. Today there are three possible intrinsics definitions:

1. Functions declared as an extern "rust-intrinsics" without any body.
2. Functions annotated with #[rustc_intrinsic] and annotated with #[rustc_intrinsic_must_be_overridden]. These functions have a dummy body that is ignored by the compiler. For StableMIR, 1 and 2 are handled the same way, i.e., they are intrinsics without a body.
3. Functions annotated with #[rustc_intrinsic] and not annotated with #[rustc_intrinsic_must_be_overridden]. These functions are marked as intrinsics, but they provide a fallback body.

Kani contract support for those are very limited. Users cannot annotate intrinsics from category 1 with Kani contract due to #3325. Users can add contracts to the other categories, but their contracts are ignored.