Pre-label support for specific versions of sessions

[qaphla]

Once we have #9 underway, it seems like it makes sense to also add support for versions to pre-labels and thence also to labels. My sense is that this should work almost identically to how session identifiers do --- that is, just as P p is corrupt iff there exists some si such that S p si is corrupt, S p si should be corrupt iff there exists some vi such that V p si vi is corrupt.

Needed components:

• Change the type of pre_label (label should be able to stay the same)
• Update pre_can_flow and pre_is_corrupt accordingly, probably meaning we add a get_version function for pre-labels.
• Add a principal_state_version_label constructor function, along with its corresponding injectivity property.
• Prove the version equivalent of principal_flow_to_principal_state, showing that S p si flows to V p si vi
• Check if we need any other general lemmas about sessions/versions?

We also previously discussed (very briefly) whether it makes sense to have native support for non-binary joins and meets, even potentially covering infinitary ones. In this case, maybe P p and S p si could be turned into derived notions. Maybe that's more trouble than it's worth, though.

[TWal]

I think it would be a good idea to make a collection of the types of security properties we want to be able to express, and whether adding versions are a step toward achieving these goals.

For example I think S p si in not really expressive, it allows us to express that some state with state identifier si was compromised, but we have no information on the content of that state: it is a long-term key, an ephemeral key, the state machine of a protocol run? I would like to be able to express such properties, which we currently can't.

A while back I made an experiment toward being able to express such properties, I pushed it in the branch twal/general_labels (I recommend diffing with git diff main...twal/general_labels with the three dots, or using GitHub) if you are interesting in looking at that.