tweag / pirouette

Language-generic workbench for building static analysis
MIT License
47 stars 2 forks source link

in `dev`: support as much of `PlutusIR` primitives as possible #88

Closed VictorCMiraldo closed 2 years ago

VictorCMiraldo commented 2 years ago

Currently, we can only run pirouette over its Pirouette.Language.Example, we should go ahead and implement all the necessary classes for PlutusIR; these are:

Additionally, we should also have a quasi-quoter for writing the proof obligations in PlutusIR; this can probably be reasonably easily done through some surgery on our example language syntax module; I reckon we can parameterize that AST and parser by a choice (and parser) for builtins and use that to quasi-quote PlutusIR terms.

VictorCMiraldo commented 2 years ago

@florentc , I updated this issue with some comments and more pointers

VictorCMiraldo commented 2 years ago

Another important aspect to this issue is the "as much of PlutusIR as possible"... The set of primitives is too large to be handled on a single go. I'd suggest we gather two client contracts of your choosing, produce their respective flat files and save them as golden tests. As long as we can handle those we're fine. We should slowly increase the set of our golden tests.

VictorCMiraldo commented 2 years ago

FWIW, Plutus primitives are here: https://github.com/input-output-hk/plutus/blob/master/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs

VictorCMiraldo commented 2 years ago

102 has the quasiquoter ready for PlutusIR and is able to typecheck two golden pir files.

VictorCMiraldo commented 2 years ago

With the merging of #113, I'll consider this closed. We will certainly be finding more examples that won't work and will require the addition of some builtin, but that's an issue for the future.