Add compiler certification component

[ana-pantilie]

Fixes #5941

This PR adds a certification component to our metatheory and integrates it into the Plutus plugin. The way this works is the following:

1. The UPLC compiler now keeps track of the new ASTs generated from the case-of-case program transformation
2. The Plutus plugin now receives this list of ASTs and uses the common interface UPLC between Haskell and Agda to convert the Haskell version of the ASTs into the raw Agda version of the ASTs
3. The Plutus plugin then calls into the Agda certifier which is compiled beforehand to Haskell
4. The Agda certifier receives the above ASTs and internalises them into the UPLC representation which we use throughout the metatheory
5. The next part is the part which is missing, meaning running the decision procedure to generate a proof
6. We can then print the proof to a file easily using the Agda -> Haskell FFI

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