CBMC Proofs for HKDF

This is in relation to the HKDF tests and CBMC proofs. Looks like the CBMC tests written for HKDF are specific to the APIs introduced in v 1.1.1 of openssl which we donot use.

Note that our library supports HKDF for openssl versions 1.0.2+. We currently use the HKDF APIs introduced in v 1.1.0 which is significantly different from v 1.1.1 in that HKDF modes were introduced later, and for versions less than 1.1.0 we have our own implementation of [RFC 5869](https://tools.ietf.org/html/rfc5869) which we use. We definitely would like to have the proofs for all HKDF versions.

Start with the existing HKDF tests and CBMC proofs, then compare their API assumptions with the library's OpenSSL 1.0.2+ support. Account for the OpenSSL 1.1.0 HKDF APIs and the library's own implementation for older versions, using RFC 5869 as the behavioral reference. Done means proofs cover all supported HKDF versions and implementations.

Written by the indexing model from the issue text.