Provide safe and unsafe functions to generate symbolic values

[celinval]

The return value of rmc::nondet doesn't always respect the invariant of a type. This can be confusing for a user which may want to cover the search space for all valid values of a type or for all possible values (valid and invalid).

We should create two different functions for each use case and ideally a way for a user to specify invariant of their own types.

[celinval]

We decided to move ahead and split nondet into two different functions:

pub fn rmc::any<T>() -> T { .. }
pub unsafe fn rmc::any_raw<T>() -> { .. }

[celinval]

The final solution was the following:

We deprecated rmc::nondet and provided two different functions that can be used to generate symbolic values.

• rmc::any_raw: This is a unsafe function that doesn’t provide any guarantee that the generated value is valid. It is up to the user to ensure the value is valid before it’s usage. This function can also be used to verify code that gets values from unsafe sources and ensure the proper guardrails are provided.
• rmc::any: This is a safe function that can only be used with types that implement an Arbitrary trait which validates whether a value is valid or not. This function will generate a valid symbolic value. The RMC library will also provide invariant implementation for primitive types and commonly used types.

We also introduced two new traits:

• Invariant : Provides a function that returns whether a value of the given type is valid or not.
• Arbitrary: Provides an any() method to generate a symbolic variable.

Finally, we implemented the Arbitrary trait for the Invariant trait type, allowing users to use Arbitrary by just defining the Invariant trait.

Thanks @camshaft, @zhassan-aws and @danielsn, for the great suggestions.