clash-lang / clash-compiler

Haskell to VHDL/Verilog/SystemVerilog compiler
https://clash-lang.org/
Other
1.43k stars 151 forks source link

Some types which derive Hashable instance don't derive Eq #1916

Closed phadej closed 2 years ago

phadej commented 3 years ago

I'm a maintainer of hashable and planning to make a "major" break by introducing class Eq a => Hashable a superclass constraint.

In my preliminary testing of how major breakage that would cause I found thatclash-lib and clash-prelude has some types which derive Hashable but don't derive Eq.

Looks like it's straight-forward fix, except Eq Term is defined elsewhere to be alpha equivalence. Yet, the Hashable contract says that equality should imply same hash values, so the Hashable Term instance is wrong.

So my question is:how you use (do you?) these Hashable instances (as unordered-containers pretty much needs Eq), and what you think about the change in general.

christiaanb commented 3 years ago

We use the hash to implement recompilation avoidance. We store the hash of all the top-level binders in a file alongside the generated HDL.

So yeah, false positives are somewhat bad: but a user can force recompilation with a flag. False negatives are also somewhat bad, as the compiler will recompute more than needed.

I guess the solution is to convert to debruijn levels as we traverse the Term and hash. So yeah, we can deal with an Eq superclass.

phadej commented 3 years ago

Thanks for a prompt reply. You may close this issue or leave it open until hashable-1.4.0.0 is released and dealt with.

martijnbastiaan commented 3 years ago

We use the hash to implement recompilation avoidance. We store the hash of all the top-level binders in a file alongside the generated HDL.

TBF we shouldn't use hashable for this at all. We should use a cryptographic hash instead, this gets us the guarantees we want.

leonschoorl commented 3 years ago

@martijnbastiaan What guarantees are those? It is my understanding (good) cryptographic hash makes it hard to construct collisions. Both by being complex enough to resist mathematical analysis and computationally intensive enough to resist brute-forcing. Not necessarily that the probability of collisions is lower (on random data).

martijnbastiaan commented 3 years ago

It is my understanding (good) cryptographic hash makes it hard to construct collisions.

Yes. It should be impossible to construct a collision for a cryptographic hash function. To be clear, theoretically it's always possible to create a collision, due to the pigeonhole principle but hash functions in this class are considered broken if a collision is actually found.

The guarantees I was referring to were the ones @christiaanb talked about: a proper hash should neither yield false positives nor false negatives in context of cache hashes.

martijnbastiaan commented 2 years ago

This has been fixed in master. Thanks for reporting!