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):

• Add support to validity checks in the presence of copy_nonoverlapping, copy. #3762
• Validity for enumerations with multiple variants. #3761
• Implement validity check for FnPtr #3760
• Valid value checks does not check char surrogate values #3241
• Extend validity checks for references and Box #3759

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