Simplify main agda module of certifier

[basetunnel]

This simplifies the setup of VerifiedCompilation.lagda and will help with future certifier changes.

• With RelationOf and certify functions it is now clear how passes are mapped to their corresponding translation relations and decision procedures/checkers
• Introduced Decider, Checker, Certifier synonyms (Decider was called MatchOrCE before)
• It adds the Trace A type, which represents the compiler trace without the duplicate terms (it now uses the output of previous passes as input of the next, see toTrace). We should probably dump this same structure from the Haskell side.
• Add VerifiedCompilation.NotImplemented, a trivial translation relation which can be used as placeholder for unfinished translation relations

[zliu41]

It adds the Trace A type, which represents the compiler trace without the duplicate terms (it now uses the output of previous passes as input of the next, see toTrace)

That's less flexible, since if we add a new compiler pass, we must update certifier in the same PR. How about allowing each AST in Trace to optionally provide the post-term?

[zliu41]

I added hints in #7575, which you should incorporate into your approach. You may want to wait till my PR is merged.

[basetunnel]

That's less flexible

That's intentional because the existing structure allows certain problems, like the compiler forgetting to dump a pass, dumping passes incorrectly (e.g. (PassName, t, t) instead of (PassName, t, pass t), dumping the order of passes incorrectly etc. The certifier wouldn't catch that, because there is nothing that enforces a relation between output of one pass and input of the next.

We're basically proving $R_1(t_1, t_2) \wedge R_2(t_3, t_4) \wedge \dots \wedge R_n(t_{2n - 1},t_{2n})$ for translation relations $R_i$, while we could prove the stronger $(R_1 \circ \dots \circ R_n)(t_1, t_n)$, which composes relations to state a theorem about the input and output of the entire pipeline.

We could alternatively do equality checking on outputs/inputs in the current trace, but it would slow down the certifier unnecessarily. The dumping mechanism is a trusted component, so I think they should be as correct-by-construction as possible.

since if we add a new compiler pass, we must update certifier in the same PR.

What about an additional constructor unknown : SimplifierTag? Any new pass could just dump (unknown, t, pass t), for and the certifier then defaults to the NotImplemented translation relation.

[zliu41]

What about an additional constructor unknown : SimplifierTag?

Sounds reasonable.