Re-evaluate all validity functions

Most of the validity functions come from the ESDK-C version of our model, which not always work on s2n. We need to make them general and test on both ESDK-C and s2n proofs.

One function that needs a fix is:

aws-verification-model-for-libcrypto/source/dh_override.c

Lines 21 to 23 in fcf7252

    
           bool openssl_DH_is_valid(const DH *dh) { 
        
               return __CPROVER_w_ok(dh, sizeof(*dh)); 
        
           }

The call to __CPROVER_w_ok prevents this function from being used in an assume context, which is typically done for validity functions. If interested, see the (long) discussion @ diffblue/cbmc#5955.

Also, just to be consistent with all other function names, may be we should rename it to DH_is_valid.

	bool openssl_DH_is_valid(const DH *dh) {
	return __CPROVER_w_ok(dh, sizeof(*dh));
	}