Contracts of the `plutus-use-cases` folder

[GuillaumeGen]

Pirouette should be able to handle all the contracts in the folder plutus-use-cases which use the StateMachine library. The branch https://github.com/GuillaumeGen/plutus/tree/gg/flat-generation allows to generate all the flat files.

The steps to handle such a contract are:

1. Generate a flat file,
2. Identify the transition function,
3. Put matching on the user input at the head of the term,
4. Write a skeleton for the file,
5. A simple wrong invariant is disproved by TLA+.

• [ ] Auction - Stage 1
• [ ] Future - Stage 1
• [x] GameStateMachine
• [ ] Governance - Stage 1
• [x] MultiSigStateMachine - Even stage 6
• [ ] PingPong - Stage 1
• [ ] Prism - Stage 2 The current pull-destr option does not work on it, because there is a state Revoked for which the output of the transition function is Nothing no matter the input. Since it creates a branch without a match on IDAction, preventing the permutation. Should be fixed with #12.
• [ ] StableCoin - Stage 2 The current pull-destr option does not work on it, because there is a "match on a match on a match" in this file, rather than a sequence of "match" as expected by the function. Should be fixed with #12.

One could add a step:

6. A refinement has been written, allowing us to catch errors introduced in the contact. But we do not intend to write such a refinement for the eight contracts.

[VictorCMiraldo]

As we're pivoting the overall project; I think this issue is outdated and will close it.