[tlaplus] Re: Is there a generic hash function in TLA+?

Unless what you're specifying is at the level of the hash function itself, you might be thinking about this at too-low a level. If the algorithm you're specifying should work with any hash function, make that a part of your specification: ∃ hash ∈ [Source → Bits].... If there are other requirements on the hash, add them to the quantifier. You could also define an override in Java, but then your specification means you rely on that particular hash function.

Ron

On Thursday, December 19, 2019 at 5:17:37 PM UTC, Thomas Gebert wrote:

Hello!

I am currently trying to spec out an algorithm that needs a hash algorithm (in this case I have to do things with the bits of the hash, so I can't rely on simple equivalence). It doesn't have to be a cryptographically secure hash, or even a particularly collision-free hash; I just need something that takes in an input, and returns back a consistent number with a consistent input (I'm happy translating the number myself to a binary sequence).

Now, I thought about writing a very simple operator to do it with a big if-else chain that simply loops-over a sequence and does a basic number-mapping, then adding the numbers and modding, but then I realized that that would *only* work with Sequences, which means strings wouldn't work.

I saw that there was a Stackoverflow post with someone implementing something in Java [0] , and that's what it comes to I'll to that (if someone would link me to how to add custom Java modules into a spec I would be grateful), but I was wondering if I'm overcomplicating this, and maybe there's something built-in now?

[0] https://stackoverflow.com/questions/53908653/use-module-overloading-to-implement-a-hash-function-in-tla