Add Twirp Wire Protocol v7

[mattmccormick]

This change adds a Twirp Wire Protocol (v7) TLA+ spec. The protocol is defined at https://twitchtv.github.io/twirp/docs/spec_v7.html

I am new to TLA+ and we use Twirp at work so I thought this would be a good learning exercise for me. I'm happy to receive any feedback on how to improve the spec. If it's deemed too simple for inclusion in the Examples that's ok as well.

[lemmy]

@mattmccormick Thanks for opening this pull request. Given that the spec is small, readers will probably wonder what insights writing this spec provided.

[mattmccormick]

@mattmccormick Thanks for opening this pull request. Given that the spec is small, readers will probably wonder what insights writing this spec provided.

For me personally, as a newbie to TLA+, some of the things I got stuck with longer than I would have liked were:

• how to get the "values" from a function. With CodeToStatus I wanted to be able to pull out the values like interacting with a dict in Python where I can do d.values(). Finally, I was able to do that by using the DOMAIN which provides the keys and then getting the set of all values corresponding to all keys in the domain.
• how to dynamically alter a function or if this is bad practice or not to do so. For instance, response is initiated to [status |-> ...] but then in Success, response' ends up having a body "key". SpecificError also modifies the primed response to add a "key" that does not always exist.
• in general, how to structure the spec and when to "pull out" actions. I'm still not entirely clear on the best case practices as compared to normal programming where I have intuition based on experience. In another spec I wrote, I seemed to struggle with pulling out actions that sometimes used prime variables and sometimes didn't. I found it confusing to interleave actions that set the primed variables and ones that don't especially if the ones that set the primed variables do not set all the primed variables - so only a subset
• I have imported this module into another module and by doing so, I tried to make this more general. That's why there are some formulas that aren't used here but are used in the other module.
• as mentioned in the comment, how much should actually be implemented in a TLA+ spec versus left out to avoid redundancy. I decided to try to add everything I saw in the written specification but perhaps this was overboard and it's a good learning point to try to keep TLA+ specs simpler.

[lemmy]

Quick question re 1) Were you aware of the CommunityModules and the Range operator specifically? We've been considering graduating some operators/modules from the CommunityModules into TLC, and Functions.tla seems like the most useful one.

[lemmy]

@mattmccormick Housekeeping, feel free to re-open if you still want this contributed.