Typeclass for simplifying working with labelled data

[qaphla]

This is a (very) rough draft of a general idea to avoid (mostly) needing to explicitly call get_label, by using a typeclass to manage label extraction from labelled data, particularly for when we come to doing large proofs that trace can_flow through several different objects.

I believe this makes proofs more focused on the core idea, and I don't see any obvious drawbacks (it seems like the typeclass resolution works fine in the testing I've done, but maybe there are examples where it wouldn't work so cleanly).
I think an actual implementation should probably be a bit more core, replacing the existing get_label handling everywhere, but it seemed best for a proof of concept to be lighter-weight.

One potential drawback I see here is that SMTPats don't appear to work very well on the test lemmas I defined here, because they don't bind the labelled instances (but maybe there's a way to work around that with the right patterns).
That said, since the definitions being used aren't opaque, we rapidly get back to the can_flow lemmas which have working SMTPats. This does probably use up additional fuel, though, due to the additional layer of indirection, so if possible it would be better to lift any key SMTPat lemmas that we use about can_flow to less_secret and hide the definitions.

One other possible application that I didn't explore here is to use this not only in the proofs, but also in constructing labels --- in principle, we could make join take arbitrary labellable data, rather than just labels, making it somewhat cleaner to write down "new random value x is secret to anyone who knows either data y or data z".

Feedback welcome, particularly on the core idea, but also on how this concept might be helpful more generally.

[TWal]

I like the idea! I think it's okay if there are no lemmas for these specific functions and we rely on the basic ones on can_flow (and keep the new definitions transparent to the SMT). We shouldn't need more fuel while doing that, I think fuel is only useful to unfold recursive functions.