Extend HMAC proof to cover state reuse

[SalusaSecondus]

In #58 we identified that the existing proofs only work when you start with a zeroized HMAC_CTX. Since a common use of this state object is to calculate HMAC multiple times using the same key and digest (and hopefully gain performance improvements), we should extend our proofs to cover when HMAC_CTX is reused and both the key and md passed to HMAC_Init_ex are NULL for subsequent calculations.