Implement validity checks for unsupported constructs

[celinval]

In Rust, producing an invalid value triggers immediate UB. Kani currently has partial and unstable support to detecting invalid value UB which was added in #3085.

This issue is to track implementation of missing checks listed bellow, which are currently encoded as an assert!(false):

• Intrinsics: copy_nonoverlapping, copy.
• Validity for enumerations with multiple variants.
• Validity for missing types such as: FnPtr, Dyn.
• Valid value checks does not check char surrogate values #3241

Note: Dyn* is not currently supported in Kani (#1784); thus, we left it out of the scope of this issue.

[celinval]

Note to self: Revisit how we are implementing validity for enumerations with VariantsShape::Multiple