Add missing functionalities to kani_core

[celinval]

• Add Arbitrary for array
• Add Arbitrary for tuples
• Add missing changes from modifies slices (Function Contracts: Modify Slices #3295)

Note that for adding any_array I had to cleanup the unnecessary usage of constant parameters from kani::any_raw.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[jaisnan]

Thanks for the cleanup, this might make unification easier as well. Approving as the added function-contracts in the verify_core seem to check for regressions in newly added capabilities as well.

[celinval]

Thanks for the cleanup, this might make unification easier as well. Approving as the added function-contracts in the verify_core seem to check for regressions in newly added capabilities as well.

BTW, I noticed that core crate contains a re-export of itself as core, so they can use core inside it. So we might be able to just use straight core:: for both versions (with and without core), so we may not need the $core argument to our macros.