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.

[zliu41]

@bezirg has unified the pir, plc and uplc executables into the plutus executable, which I think is the one you'd want to integrate with.

[ramsay-t]

The integration is great! The log/show information can be improved in the next iteration. The decision process is "working correctly" because it checks that all the changes are instances of implemented translation relations, and obviously the unimplemented ones aren't! We should make a log file with more granular information, and maybe adopt Jacco's approach of having a process for "accepting" unimplemented phases.

[effectfully]

Why do you need this check here?

[ana-pantilie]

If I recall correctly, it's to convert to the Agda representation of terms, the Haskell -> Agda intermediate module uses that:

plutus/plutus-metatheory/src/Untyped.hs

Line 36 in 4066409

conv :: Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm

.

[effectfully]

I don't get it. If it was for that function, you'd also need to check equality of uni and DefaultUni. What breaks if you remove the eqT check?

[ana-pantilie]

Good catch! I accidentally didn't use the fun type param in the SimplifierTrace type. Fixed now, thanks.

[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