Should

```
(* Invariant: a hash is size bytes long. *)
```

be

```
(* Invariant: a hash is hashbytes bytes long. *)
```

?

Or `hashbytes` should be named `hash_size` and the comment should be amended?