Pirouette was built on the assumption that many Plutus contracts would be built with the StateMachine API. From our experience, this has not been the case. Plutus contracts are being built in very diverse formats. In order to have a chance at translating these diverse contracts into TLA+, we need a full-featured symbolic execution engine.
This PR is now a collection of all the children PRs that are needed to bring a symbolic execution engine into Pirouette. This is our progress so far:
[x] Symbolic Execution with SMT assistance of basic terms (no Higher-order, no polymorphism). (merged on: #52)
[ ] Add a sanityCheck predicate that captures the SMT translation assumptions and gets called every time a term is being translated when running pirouette in debug mode
[x] Create a simpler LanguageDef TestingLang and add more tests to pirouette, in particular, capture the specs of symbolic execution.
[x] Monomorphizing PlutusIR terms as a standalone transformation ( Merged on #54 )
[ ] Handle de Bruijn variables instead of hardcoding Var 1.
[ ] Defunctionalizing PlutusIR terms as a standalone transformation
[ ] Add a sanityCheck predicate to capture defunctionalizing assumptions.
[ ] Replace TLA+ defunctionalization by monomorphizing then defunctionalizing PlutusIR before translating to TLA+
VictorCMiraldo
commented
2 years ago
Pirouette was built on the assumption that many Plutus contracts would be built with the
StateMachineAPI. From our experience, this has not been the case. Plutus contracts are being built in very diverse formats. In order to have a chance at translating these diverse contracts into TLA+, we need a full-featured symbolic execution engine.This PR is now a collection of all the children PRs that are needed to bring a symbolic execution engine into Pirouette. This is our progress so far:
sanityCheckpredicate that captures the SMT translation assumptions and gets called every time a term is being translated when running pirouette in debug modeLanguageDef TestingLangand add more tests to pirouette, in particular, capture the specs of symbolic execution.Var 1.sanityCheckpredicate to capture defunctionalizing assumptions.