Add verified compilation certification component

[ana-pantilie]

Fixes #5941

This PR implements the following:

• adds the top-level VerifiedCompilation component to the Agda code
• the UPLC compiler now generates a list of intermediate ASTs which are added to a state layer in the monad stack
• integrates the Agda certification component into the uplc executable as a --certify <file-name> option to uplc optimise; it was necessary to pull it out into a separate package called plutus-executables because of cyclic dependencies

Notes:

• I wasn't able to move library plutus-core-execlib to plutus-executables because plutus-benchmark and plutus-metatheory depend on the library
• the uplc/plc/pir executables are no longer supported on Windows because they now depend on the metatheory; is this a problem?

TODO in future PRs:

• tag ASTs with optimisation
• proper proof serialisation
• check whether the proofs can be reloaded into Agda properly
• add CI tests

Try it out

To try this out, try:

cabal exec uplc -- example -s fibonacci | cabal exec uplc -- optimise --certify certificate-fibonacci

where certificate-fibonacci is the name of the .agda file that will be created with the proof object.

~This is currently providing a negative result (the certificate is no), even though force-delay is clearly being applied! But now we have an example on which to start debugging.~ As pointed out by @ramsay-t , the result is correct because it's applying optimisations which currently haven't been specified in the certifier!

---

Pre-submit checklist:

• Branch
  • [ ] Tests are provided (if possible)
  • [ ] Commit sequence broadly makes sense
  • [ ] Key commits have useful messages
  • [ ] Changelog fragments have been written (if appropriate)
  • [ ] Relevant tickets are mentioned in commit messages
  • [ ] Formatting, PNG optimization, etc. are updated
• PR
  • [ ] (For external contributions) Corresponding issue exists and is linked in the description
  • [ ] Targeting master unless this is a cherry-pick backport
  • [ ] Self-reviewed the diff
  • [ ] Useful pull request description
  • [ ] Reviewer requested

[ana-pantilie]

ci/eval is failing but I have no idea why, if anyone does please let me know. Nevertheless, this should be ready for review now.

[bezirg]

the uplc/plc/pir executables are no longer supported on Windows because they now depend on the metatheory; is this a problem?

@ana-pantilie Not atm