integrate lennart's HMAC pure lemmas (2 not working: mkArgZ and spec_sha dependency)