In
https://groups.google.com/u/1/g/tlaplus/c/jnlmYhh4jmo/m/HTGFDZimCAAJ, when asked about a generic hash function in TLA, Ron Pressler wrote:
> 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.
Which is a lovely high-level way to specify that such a function exists. I'm facing something similar in a toy spec I'm trying to write for a transpiler, where I can say there exists such a function mapping instructions on architecture A to those on Architecture B, something like ∃ TranslateFn ∈ [INSTRUCTIONS_A → INSTRUCTIONS_B]. Good so far.
I'd like to use that function in a TLC model, but just using the existential quantifier doesn't expose TranslateFn. So the next thing that looks right is TranslateFn == CHOOSE f ∈ [INSTRUCTIONS_A → INSTRUCTIONS_B] : TRUE , because I don't care what that function is, just that there is one and that I can use it.
But won't that ask TLC to (senselessly?) explore the whole space of possible mapping functions? If so, is there a way around that?
Cheers; still learning (slowly...)