Add a Hash interface

[marsella]

Many algorithms, like ECDSA, are generic over the hash function they use as long as it satisfies certain properties (e.g. appropriate-length hash output). However, right now there is no unifying interface for hash functions. We should write an interface so that other algorithms can be written generically.

Some useful things we'll want in it, from implementing ECDSA:

• An accessible hashlen (the length of the output)
• the Hash function itself
• I think most hash functions have a constraint on the maximum message size. There should probably be a type constraint as part of the interface that can be used to restrict inputs on functions that call the hash.

There may be other useful things to put in the interface, too.

• Implement an interface
• Instantiate it with the SHA2 functions as an example
• Consider instantiating with other useful hashes as well, or make follow-up issues to do so.
• Update ECDSA to use the interface (as an example. If this is too hard, make a follow-up issue.)
• Identify other algorithms that could use it and make follow-up issues.

[marsella]

Notes on the type constraint idea:

• Interfaces cannot contain generic / fill-in-the-blank constraints. They can contain constraints that must be true for all implementations of the interface
• A brief pass suggests that many hash functions use the specific constraint that a message must be no more than n bits, for some n. We might be clear to encode this upper bound as a type on the interface and then define the constraint at the interface level (instead of the implementation level).

[weaversa]

Notes on the type constraint idea:

• Interfaces cannot contain generic / fill-in-the-blank constraints. They can contain constraints that must be true for all implementations of the interface
• A brief pass suggests that many hash functions use the specific constraint that a message must be no more than n bits, for some n. We might be clear to encode this upper bound as a type on the interface and then define the constraint at the interface level (instead of the implementation level).

In a recent take we have the following in a parameter block:

  type UpperLimit : #
  hash : {a} (fin a, UpperLimit >= width a) => [a] -> [DigestSize]

This is workable, but I'd love to see an improvement. In the back of my head I've always thought it would be nice if Cryptol could accept type constraints at the parameter level, along with the current values and types (natural numbers).