Module Base__.Hash_intf

Hash_intf.S is the interface which a hash function must support.

The functions of Hash_intf.S are only allowed to be used in specific sequence:

alloc, reset ?seed, fold_..*, get_hash_value, reset ?seed, fold_..*, get_hash_value, ...

(The optional seeds passed to each reset may differ.)

The chain of applications from reset to get_hash_value must be done in a single-threaded manner (you can't use fold_* on a state that's been used before). More precisely, alloc () creates a new family of states. All functions that take t and produce t return a new state from the same family.

At any point in time, at most one state in the family is "valid". The other states are "invalid".

• The state returned by alloc is invalid.
• The state returned by reset is valid (all of the other states become invalid).
• The fold_* family of functions requires a valid state and produces a valid state (thereby making the input state invalid).
• get_hash_value requires a valid state and makes it invalid.

These requirements are currently formally encoded in the Check_initialized_correctly module in bench/bench.ml.