Modeling a Hash

[dominik...@gmail.com]

Hello,

I am attempting to model an algorithm that employed hashes to determine equality. I am looking for a way to model a has function so that

Hash(rec-1) = Hash(rec-2) <=> rec-1 = rec-2

e.g.

Hash([foo |-> "bar"]) = Hash([foo |-> "bar"]) but
Hash([foo |-> "bar"]) # Hash([foo |-> "baz"])

So far the only idea in my mind is to create an additional variable to manually track rec-1, rec-2 and their "hashes" (rec-3, ... rec-n can be created dynamically, so no constant).

However, since in most implementations a hash is an inherent property of a data record, an explicit modeling and manual tracking feels like communicating the wrong idea.

Any idea how I could alternatively model an inherent hash value in tla+?

Thanks and best, Dominik

[dominik...@gmail.com]

Apologies, I forgot to mention the Hash should be a String as the algorithm also depends on String concatenation.

Best, D

[Andrew Helwer]

Hey, Dominik! I've also taken a crack at this problem. There are three solutions I've come up with:

First, if the data structure you're hashing doesn't itself include a hash, you can just use the identity function. A hash of a record is just the record itself. Easy-peasy. However, this doesn't work when you're specifying recursive data structures that point to other elements with hashes.

Second, you can assign hashes from a pool of values as they are requested. You might have a variable SequenceNumber which is a number that is returned then incremented every time you call Hash(), plus you keep track of past assigned hashes and return those if you've already assigned a hash to the val. This runs into problems like being only able to calculate a single hash per step, since you have to modify a variable in order to assign the hash. Another drawback as that this looks "messy"; you have these extra variables which detract from understanding of the spec. This can to some degree be solved through hiding the hash function implementation in a separate "model check" spec which includes your main spec, as outlined here: https://stackoverflow.com/q/49600307/2852699

The final approach (which I haven't yet accomplished) is to use module overrides and actually write your hash function in Java using the built-in hashing capabilities of the language. See here: https://stackoverflow.com/q/53908653/2852699

Andrew

On Monday, February 18, 2019 at 12:55:36 PM UTC-8, Dominik Tornow wrote:

[dominik...@gmail.com]

Thank you Andrew for sharing your experience. I tend to prefer option 3, I guess it's time to dust off javac. I will update this thread in case I have a working solution.

Thanks again. D

[Markus Kuppe]

On 19.02.19 11:03, dominik...@gmail.com wrote:
> Thank you Andrew for sharing your experience. I tend to prefer option 3, I guess it's time to dust off javac. I will update this thread in case I have a working solution.

Hi Dominik,

you might want to read over my response [1] to Andrew's question on
StackOverflow. It shows how to create a TLC module overwrite.

Thanks
Markus

[1] https://stackoverflow.com/a/54757162/6291195

[dominik...@gmail.com]

Thank you Markus, that did the trick!