Is there a generic hash function in TLA+?

[Thomas Gebert]

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

[Thomas Gebert]

I would also like to point out that I can work around this if there's a way to access individual elements of a string, which if memory serves there is not. 

[Ron Pressler]

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

[Thomas Gebert]

That's a valid point; I feel a bit silly for not realizing that I could have a function that takes in some value, and returns back a Seq of items in set {0,1}.  That'll make me avoid being tied to any particular implementation of a hash.  

I have a bit of a silly followup to that; how would I go about specifying that a function's domain can be *any* valid TLA object?  

[Ron Pressler]

It's not a silly question at all, but the answer is that you can't because such a function doesn't exist (in general in mathematics). The good news is that you really don't need such a function. You will likely have some set representing the domain of the objects you're interested in, even if it is some opaque, unknown set defined as a CONSTANT. Use that set as the hash function's domain. If there are several domains you're interested in, specify several hash functions.

Ron

[Thomas Gebert]

Fair enough; to start off I'll just work with the set of strings.  That'll be versatile enough.  Thanks for all your help!

PS While I'm still learning and probably can't fully appreciate them yet, I loved your TLA+ theory blog posts!