Open
Description
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).