Remove CBMC validator functions

There are at least a couple of CBMC validator functions in the code base with names `*_is_valid_cbmc`. These functions typically do more assumptions than their non-CBMC versions and cannot be used as preconditions in E-SDK functions.

For example, `aws_cryptosdk_sig_ctx_is_valid_cbmc` was being used in #659 but had to be removed since including it as a precondition to `sign_header` would require CBMC libraries to be included as well. This is not an option.

The goal is to entirely remove these functions from the code base. To this end, we have to amend proofs where they are being used and then remove their definition (e.g., from cbmc_invariants.c).

Search the codebase for functions named *_is_valid_cbmc, starting with aws_cryptosdk_sig_ctx_is_valid_cbmc and the definition in cbmc_invariants.c. Inspect the proofs that use these validators and amend them before removing the definitions. Done means the CBMC validator functions are gone and the affected proofs no longer depend on them.

Written by the indexing model from the issue text.