Provide a first complete formal model of various Leios variants

[WhatisRT]

Details

• Finish the details of the current simple Leios spec
• Implement alternative variants depending on interest: short, full, etc.
• Provide an executable specification for every variant
• Implement some functionalities Leios depends on, if desired

Definition of Done

Code type-checks and compiles in CI and is executable given the right setup

[ghost]

Thanks @WhatisRT! Let's discuss the details but I think it would be great to focus on Short Leios for the protocol part. The way I see it, it would be better to have FM specification work be integrated as part of broader objectives. Having a formally specified Leios is not an objective in and of itself, but a mean to an end