feat: introduce has_usage to improve bytes invariant

[TWal]

Builds on #66.

When doing proofs on protocols more complex than NSL or ISO-DH, I noticed that it was annoying to do proofs with get_usage, because we rarely are 100% certain that get_usage key == …. However, in what I've seen, we can always prove get_usage key == … \/ is_publishable tr key (more on that below).

Hence, this PR introduces

// used as: key `has_usage tr` usg
let has_usage tr key usg =
  get_usage key == usg \/
  (get_label tr key) `can_flow tr` public

and use it systematically in the pre and post-conditions to prove bytes_invariant.

I think that contrary to get_usage key == …, we can always prove has_usage tr key usg on a key:

• if key was encrypted using public-key encryption:
  • if key is encrypted by a honest principal that knows has_usage tr key usg, we can put this information in the public-key encryption predicate
  • if key is encrypted by the attacker, then it is publishable
• if key is obtained via a KEM, we have the same property for roughly the same reasons as in the case of public-key encryption
• if key is derived via key = kdf_expand prk info then get_usage prk == … allows to deduce get_usage key == …, and is_publishable tr prk allows to deduce is_publishable tr key, so has_usage tr prk … allows to deduce has_usage tr key …
• etc

The key properties of has_usage are:

• as with all predicates of DY*, it is monotonic in the trace
• if a key has two usages, then either the usages are equal, or the key is publishable
• if a key is publishable, then it has any usage

The proofs of NSL and ISO-DH were easy to update, and the proofs of HPKE were greatly simplified (because before we always had to reason like "either this has the correct usage, or this is publishable", which we don't need to do anymore).

This is still a draft, that I am posting to collect thoughts.
The next steps are:

• remove get_usage completely and define has_usage directly
• remove usage from the Rand constructor of bytes (discussed with @qaphla in feat: make labels erasable #54)
• fix the admits in the proofs of kdf_extract

[TWal]

In the previous commits, I:

• removed usage from the bytes constructor (as it was not too costly to do)
• simplified (i.e. almost nuked) the invariants around kdf_extract -- they were not realistic anyway (see Invariants on kdf_extract are too strict #62) and would need more thinking to do properly, I think it is out of scope for this PR and simplifying them help remove the admits

I did not define has_usage directly without defining get_usage first, although I think that would have helped for better invariants for kdf_extract, the new invariants still wouldn't have supported all the usages in #62 while adding some complexity, so we can leave it aside for now.

I will try to use this PR in MLS*, see if it works well and report back. Otherwise, aside from the //TODO comment I would think this is ready to go (although I will do another pass on the diff before un-drafting the PR).

[TWal]

I confirm this is allowing me to simplify proofs in MLS*, because I can now remove most of "or is publishable" statements in the intermediate security lemmas.

[qaphla]

This still looks overall like a reasonable approach to me (in general, even --- it feels like if we can avoid thinking about the corrupt case unless it's necessary, and just propagate it onwards for the most part, then we might also save effort in proofs).

I think the TODO should probably be addressed before this is finished, and either a change made or a note added that we can strengthen the postcondition of, for instance, mk_rand_has_usage --- I agree that it's probably not needed for what we're currently doing, but if we forget that it can be made stronger, it could lead to some difficulties in the future, if we need that extra strength.

[qaphla]

Seems to have been cleaned up --- I think there are still some syntactic mismatches between, for instance, the invariant lemma for pk_enc and that for pk_dec (publishable vs (get_label can_flow public), but not semantic ones that I noticed. That said, I'm not inclined to push for work on making these match right now, because now that the main label changes are in, I plan to update #51 to work in the new setting, which should make these more immediately equivalent.

[TWal]

Ah, good catch. I have fixed it while I'm at it, and will merge once the CI goes back green.