Move certifier to plutus-metatheory and expose it as a library

[ana-pantilie]

As part of https://github.com/IntersectMBO/plutus-private/issues/1348, I'm moving the certifier to the plutus-metatheory package.

The reason behind this is that it doesn't make sense for plutus-tx-plugin to depend on plutus-executables, since it will call the certifier as a library function and not as some separate executable.

All of the certifier's Agda code lives in plutus-metatheory, so it would make sense for its Haskell code to live there as well. If we were to create a separate package for the certifier then we should move both the Haskell and the Agda code there, and I'm not sure if the effort is worth it (at least for now).

Note: I wanted to move all of the Haskell modules used for calling Haskell code from Agda into the FFI directory, however moving Raw.hs there resulted in some weird behavior from cabal. I have opened an issue about this: https://github.com/IntersectMBO/plutus-private/issues/1562

[zliu41]

So we'll need to release plutus-metatheory on CHaP (please open an issue), and we probably don't need most of the existing plutus-metatheory, do we? If so, perhaps a good idea to split it into smaller libraries, but not critical.

[ana-pantilie]

So we'll need to release plutus-metatheory on CHaP (please open an issue), and we probably don't need most of the existing plutus-metatheory, do we? If so, perhaps a good idea to split it into smaller libraries, but not critical.

@zliu41 What would be the benefit of splitting the metatheory up? Would it outweigh the effort required to figure out a way to do it?

The certifier depends on the formalization of UPLC which constitutes quite a large part of the metatheory.

Maybe we could split the plutus-metatheory package up into the UPLC syntax and various semantics.
I'm not very familiar with the semantics side, from a quick look I can see that we have a CEK formalization and a reduction semantics, a CC machine and a CK machine (I couldn't tell you much more though).

Anyway, in the future we'll need to rely on a semantics for the certifier as well, but it will be a new semantics. So conceptually we could split it up into UPLC syntax + one package for each semantics, and the certifier would depend only on the syntax + the "special" semantics for the certifier, but I don't know whether there are any current or future interdependencies.

There's also the question of build complexity: right now we rely on Setup.hs which does some preprocessing in order to build the metatheory, and things might get quite complicated if we split it up into multiple packages (or it might not, but we'll need to consider this).

[ana-pantilie]

Opened issue for releasing the metatheory: https://github.com/IntersectMBO/plutus-private/issues/1563.

[zliu41]

which constitutes quite a large part of the metatheory.

In that case no need to split. That said, we should consider a different name - "metatheory" specifically refers to the formalization of the Plutus Core language. If the certifier is now part of it, a different name would be more appropriate.

[ana-pantilie]

That said, we should consider a different name - "metatheory" specifically refers to the formalization of the Plutus Core language. If the certifier is now part of it, a different name would be more appropriate.

I'm pretty bad at naming things! 😄 Do you (or @ramsay-t) have any suggestions?

[zliu41]

I'm very bad too, but perhaps something like plutus-formal or plutus-fm