Investigate how to move assumptions out of `ensure_...` functions

[adpaco-aws]

Some ensure_... functions need to make assumptions about certain sub-structures before doing the regular "ensuring" process. We will investigate ways to move these assumptions somewhere else or remove them completely.

As an example, the function ensure_default_cmm_attempt_allocation from #656 where the following code is executed before allocating cmm:

    /* Assumptions required to init cmm */
    ensure_cryptosdk_keyring_has_allocated_members(keyring, vtable);
    __CPROVER_assume(aws_cryptosdk_keyring_is_valid(keyring));
    __CPROVER_assume(keyring->vtable != NULL);