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

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);
```

Start with ensure_default_cmm_attempt_allocation from issue #656 and trace the assumptions made before allocating cmm, including ensure_cryptosdk_keyring_has_allocated_members and the __CPROVER_assume calls. Compare how other ensure_... functions establish sub-structure assumptions. Done means producing an agreed approach for moving or removing those assumptions.

Written by the indexing model from the issue text.