Implement dumping a compilation trace of the pir-pir pipeline for the Coq certifier

[jaccokrijnen]

This PR adds dumping of all intermediate PIR ASTs (the "compilation trace"), in a format that can be handled on the Coq side for the certifier. It adds the types CompilationTrace and PassMeta for structuring all information about performed passes.

I've added a plugin flag dump-cert which then dumps all of that information in .pir.ast and .pir.meta files (one for each pass).

• I've added a MonadState constraint to Compilling to build a CompilationTrace. This means all ASTs are kept in memory until everything is dumped at the same time. This could be changed to doing IO directly after a pass has finished, but I didn't notice any significant performance issues and I didn't want to hack in more unsafePerformIO like is done for logging with trace.

• I've used a bit of an ad-hoc pretty printing strategy which should probably change at some point. It basically implements a Show-like representation without record syntax so it easy to parse on the Coq side.

• The Inline pass tracks the eliminated (unconditionally inlined) variables, because this information is needed on the certifier side to decompose the pass in actual inlining + dead code elimination. It changes the type signature of inline to

      -> m (Term tyname name uni fun ann, ([name], [tyname]))
  

  which I don't like very much, but I haven't found a nicer way of doing it.

• Since some passes called the rename pass internally, I moved those calls out to Compiler.hs, which was easier than moving dumping code into those passes.

• plutus-ir needs bytestring as dependency to give an instance for ToCoq Bytestring. Alternatively, the ToCoq module could go to plutus-tx-plugin component.

[jaccokrijnen]

I'd like to assign @michaelpj , but I can't :)

[michaelpj]

Will look at the code in a bit!

This could be changed to doing IO directly after a pass has finished, but I didn't notice any significant performance issues and I didn't want to hack in more unsafePerformIO like is done for logging with trace.

I think it depends on how we want to view this. If we do want to think of it as accumulating all the ASTs and then dumping them together then this seems fine (e.g. if we want to dump them in some joint structure at the end). The alternative is something I want to do anyway which is to thread some more proper structured logging through, at which point we can log the ASTs fairly generically and then just dump them at the end by looking at the log events.

I've used a bit of an ad-hoc pretty printing strategy which should probably change at some point.

Maybe let's localise as much as possible in the plutus-ir-cert component?

It changes the type signature of inline to

If we're going to fit this into the pass abstraction we're going to need to generalise it a bit 🤔 Maybe we want to say that in general passes can produce some evidence which goes into the postcondition checker?

Since some passes called the rename pass internally, I moved those calls out to Compiler.hs

This is fixed in my other branch!

plutus-ir needs bytestring as dependency to give an instance for ToCoq Bytestring

No problem, bytestring is a very standard dep.

[jaccokrijnen]

Will look at the code in a bit!

This could be changed to doing IO directly after a pass has finished, but I didn't notice any significant performance issues and I didn't want to hack in more unsafePerformIO like is done for logging with trace.

I think it depends on how we want to view this. If we do want to think of it as accumulating all the ASTs and then dumping them together then this seems fine (e.g. if we want to dump them in some joint structure at the end). The alternative is something I want to do anyway which is to thread some more proper structured logging through, at which point we can log the ASTs fairly generically and then just dump them at the end by looking at the log events.

Either is fine. The only joint structure that is necessary is the ordering of dumped ASTs. I'm storing that in the filenames at the moment (e.g. 009_Module.pir.ast). So if we go via the structure logging route, it would still need some form of state like a counter or history of performed passes.

I've used a bit of an ad-hoc pretty printing strategy which should probably change at some point.

Maybe let's localise as much as possible in the plutus-ir-cert component?

I've moved all the dumping code in there. I've renamed cert and cert-stub directories to cert/tests and cert/tests-stub respectively (the existing extracted stuff from Coq). I've added cert/certifier for this dumping code and for future logic to produce the Coq proofs.

It changes the type signature of inline to

If we're going to fit this into the pass abstraction we're going to need to generalise it a bit 🤔 Maybe we want to say that in general passes can produce some evidence which goes into the postcondition checker?

That could work, perhaps in a MonadState?

[zliu41]

The PR needs to be refactored to work with the Pass abstraction (#5665). I think it's fine to simply make each pass return (Term tyname name uni fun a, PassMeta). No need to be more fancy than that.

[zliu41]

nit: you can use evalStateT

[zliu41]

There's already a notion of "compilation trace", and a plugin flag dump-compilation-trace. It refers to compilation trace from GHC Core to PIR. See #5482.

I suggest giving this a more specific name such as PirCompilationTrace or IntermediatePirs

[zliu41]

This will be easier to do with the Pass abstraction: Float-in would be a CompoundPass that consists of two Passes: renaming and float-in proper. This drive module does not need to know such details.

[zliu41]

This has been covered by Ana's work and is no longer needed.

[ana-pantilie]

This has been covered by Ana's work and is no longer needed.

That's not really true, my work is just on recording UPLC phases, and it's tied to the uplc executable.

I'm reopening this issue because when we will have a PIR certifier and will want to integrate the work into the plugin this discussion will come in handy.

Edit: just noticed this is a PR and not an issue...

[ana-pantilie]

Talked to @jaccokrijnen and the PR is quite outdated, so we can close it. But it's good to keep the discussion in mind for the future.