Invariants on kdf_extract are too strict

[TWal]

Currently, we require that salt has usage KdfExtractSaltKey or ikm has usage KdfExtractIkmKey. This is too strict and would prevent proving reasonable protocols, such as X3DH which is concatenating 3 or 4 DH shared secrets in ikm and salt is all-zeros, or HPKE which uses kdf_extract as a hash function (hence neither of the inputs are cryptographic keys). For this reason, the current HPKE proof in DY* in not spec-compliant because these kdf_extract have been omitted.