Certifier: Add decision procedure for hoist-builtins pass

[basetunnel]

Fixes https://github.com/IntersectMBO/plutus-private/issues/2222

Also adds convenient pattern synonyms for nested lets.

[ana-pantilie]

Isn't this much more general than what is specified in the documentation above: 3. Only partially applied built-ins are lifted (always pure)?

There's also an issue regarding termination of the decision procedure:

N = (\x -> x . x) . (\x -> x . x)
=== match on line 177 ==>
N = \x -> x . x
L = \x -> x . x
=== match on line 166 ==>
N = x . x
L = \x -> x . x

Notice that L is pure so we end up calling dec-hoist on the substitution, where N = (\x -> x . x) . (\x -> x . x) again, which will loop.

I realize that N = (\x -> x . x) . (\x -> x . x) being untype-able won't ever come from a valid compiler trace, so I tried to come up with an example using the Z fixpoint combinator which we use, but my brain failed me 😄 . However, we shouldn't base termination of the decision procedure on whether the UPLC program has a valid type or not.

Stepping back, I think the easiest solution would be to restrict L to partial builtin applications (which would just be a restriction of the inductive definition we have for Pure). That would most definitely solve the termination issue.

[effectfully]

It's not untypeable? https://ideone.com/fSDlSy

[basetunnel]

Thanks for spotting that termination issue @ana-pantilie, I think it can also be fixed by changing the relation slightly, instead of specializing to built-ins.

Regarding the generalization, that was on purpose. I wanted to stay close to the way CSE is defined. Originally I hoped to reuse CSE for this pass, but it seemed more complex to generalize that existing relation/procedure. I'm also fine with specializing this one to partially applied built-ins. Do you have a preference?

[ana-pantilie]

@effectfully I think there's some confusion on the syntax I used, sorry. N = (\x -> x . x) . (\x -> x . x) would be f = (\x -> x x) (\x -> x x) in Haskell syntax (the omega combinator), which I don't think can be typed can it? I was using . as UPLC's application connective.

[ana-pantilie]

@basetunnel If you want to opt for a general version of the translation relation, I think that's fine, as long as we think carefully about whether it really preserves semantics or not. The version specialized to builtins seems very straightforward semantically and for the current UPLC compiler it's sufficient, so that's why I suggested it.

[effectfully]

I was using . as UPLC's application connective.

Ah, sorry.

Anyway, (\x -> x x) (\x -> x x) is maybe not typeable directly, but you should be able to get that exact term by creating omega same way we create Z and then applying the UPLC optimization pipeline afterwards.

Z is

(\f -> (\s -> s s) (\s -> f (\x -> s s x)))))

That's not very far from omega at all.