[MLS] Formal proof for PR 713 / "Improve parent hash guarantees"

[Théophile Wallez <[e-mail]>]

Hello All,

During the last interim, when discussing PR 713, people raised concerns 
that this PR might introduce bugs in MLS, because the parent-hash is a 
complex thing and contained many bugs in the past.

During the last days, I formalized a small part of MLS in F*, and proved 
that the invariants checked in the "Verifying Parent Hashes" section are 
actually invariants of the protocol.

Of course I can't just say "believe my I have a formal proof". I also 
can't just send my model as-is and expect everyone to decipher the F* 
code without explanations.
Richard therefore proposed to meet during one hour before the next 
interim, for the people interested, during which I will explain my 
model, hoping that afterwards:
- you will agree that my code faithfully models the parts of MLS dealing 
with parent-hashes,
- you will agree that the theorem I proved actually state that the new 
invariants are preserved.
The only prerequisite will be to be a bit familiar with functional 
programming (no need to know super fancy stuff, just algebraic datatypes 
/ pattern matching / recursion should be enough).

Richard will take care of setting up a Webex link.

Cheers,
Théophile.