PlutusCore pretty-prints ill-typed PIR code

[VictorCMiraldo]

Area

Plutus Foundation Related to the GHC plugin, Haskell-to-Plutus compiler, on-chain code

Summary

When pretty printing some PlutusIR code, by default, the printer doesn't show the Unique part of the name which can result in a different program that might not even typecheck.

Steps to reproduce

We wrote ourselves a trivially simple validator (I'm happy to add the source here but I don't think its relevant in this case) then pretty printed the resulting PIR with:

pretty (getPir $$(PlutusTx.compile [|| mkValidator ||]))

This did yield the following bit of PlutusIR:

[ Counter_match
  [
    { [ { State_match Counter } st ] Counter }
    (lam
      ds
      Counter
      (lam
        ds
        [[(lam k (type) (lam v (type) [List [[Tuple2 k] v]])) (con bytestring)] [[(lam k (type) (lam v (type) [List [[Tuple2 k] v]])) (con bytestring)] (con integer)]]
        ds
      )
    )
  ]
]

If we erase all the types, it becomes more readable and the error is apparent:

[ Counter_match  [ [ State_match Counter st ]  (lam ds (lam ds ds)) ]]

The (lam ds (lam ds ds)) should return a Counter, but returns a Value instead. In fact, if we parse this program again
and try to typecheck it will not typecheck. The relevant PIR definitions for State and Counter are:

(datatypebind
                    (datatype
                      (tyvardecl State (fun (type) (type)))
                      (tyvardecl s (type))
                      State_match
                      (vardecl
                        State
                        (fun s (fun [[(lam k (type) (lam v (type) [List [[Tuple2 k] v]])) (con bytestring)] [[(lam k (type) (lam v (type) [List [[Tuple2 k] v]])) (con bytestring)] (con integer)]] [State s]))
                      )
                    )
                  )

(datatypebind
                    (datatype
                      (tyvardecl Counter (type))

                      Counter_match
                      (vardecl Counter (fun (con integer) Counter))
                    )
                  )

After looking around, I found the definition in PlutusCore.Name, and saw a name has a Unique component.
I then tried to load PlutusCore.Pretty.ConfigName but the module is hidden, so I couldn't pretty print a well-typed PIR
program.

Expected behavior

I'd expect that the pretty printer, even with default options, should not change the semantics of the
program and/or that this is documented and there is an accessible way of importing PlutusCore.Pretty.ConfigName.

[effectfully]

I agree, we should pretty-print names with uniques by default. The offending instances in this case are the ones at the bottom of PlutusIR.Core.Instance.Pretty. And while we're here, we should also always pretty-print uniques in golden tests.

@michaelpj @kwxm @bezirg anybody sees any reason not to replace literally all occurrences of prettyClassicDef with prettyClassicDebug?

[effectfully]

@VictorCMiraldo

and there is an accessible way of importing PlutusCore.Pretty.ConfigName

All of that stuff is available via PlutusCore.Pretty.

[effectfully]

anybody sees any reason not to replace literally all occurrences of prettyClassicDef with prettyClassicDebug?

I'd perhaps go as far as renaming pretty*Def to pretty*NoUniquesUnsafe or something like that.

[VictorCMiraldo]

All of that stuff is available via PlutusCore.Pretty

I see, thanks! Will use that for the time-being then!

[kwxm]

anybody sees any reason not to replace literally all occurrences of prettyClassicDef with prettyClassicDebug?

A minor problem is that if you print something out and re-parse it you get names like v_1231_5212 when it gets a new unique. However, it's been annoying me recently that I always have to remember to tell plc to print out uniques (and it's caught out a few other people as well), so I think it'd be better if we get them by default (which'll probably also require changing the plc options).

[michaelpj]

We have an issue for this: https://jira.iohk.io/browse/SCP-817

We should note that the pretty-printer and parser are 100% not intended for production use. You should use one of the binary formats if you care about that. Although we don't currently have a binary serializer for PIR, we probably should.

[VictorCMiraldo]

Thanks @michaelpj, I'll use a binary format when available.

[VictorCMiraldo]

@michaelpj

I understand you mentioned the PIR parser is not meant for production, which is why I'm hesitant in creating another issue for this. Still, I have two questions:

1. Should we create a separate issue for this even if the parser is not really meant to be used for production?
2. What's the best way to get, and then load, a PIR file in an external tool for further analysis?

The issue follows:

Parsing the following minimal.pir file fails. The file was produced by minimizing a large PIR file produced by prettyClassicDebug (getPir $$(PlutusTx.compile [|| mkValidator ||]))

1| (program
2| (let
3|  (nonrec)
4|  (termbind (strict) (vardecl v x) (abs a (type) a))
5|  (termbind (strict) (vardecl f x) (lam v t (con string "Input constraint")))
6|  main 
7| ))

It fails with:

test/minimal.pir:5:4:
  |
5 |   (termbind (strict) (vardecl f x) (lam v t (con string "Input constraint")))
  |    ^^^^^^^
unexpected "termbin"
expecting "abs", "builtin", "con", "error", "iwrap", "lam", "let", or "unwrap"

Then, if we erase line 4, it fails with:

test/minimal-minus-l4.pir:4:64:
  |
4 |   (termbind (strict) (vardecl f x) (lam v t (con string "Input constraint")))
  |                                                                ^
Invalid constant: "Input of type string

[michaelpj]

What's the best way to get, and then load, a PIR file in an external tool for further analysis?

There is none, sorry. As noted, we're missing a binary format instance for PIR, we should add one.

[michaelpj]

Oh that's not true, on master we have a Flat instance, so you could use that.

[VictorCMiraldo]

Oh that's not true, on master we have a Flat instance, so you could use that.

Amazing, thanks! :)

[effectfully]

Closing as duplicate of both #4808 and #4198.