Add proofs for top-level EVP function of HMAC

[pennyannn]

AWS-LC PR1324 adds support for EVP_PKEY_HMAC. Currently proofs for HMAC only covers up to functions HMAC_Init_ex, HMAC_Update, HMAC_Final and etc. We need to extend the proofs to cover the top-level EVP functions.