DCE constructors

[VictorCMiraldo]

@0xd34df00d I took the liberty of rebasing your branch on top of the latest main and force-pushing it here to make the "files changed" tab a little easier

[0xd34df00d]

Yep, we would. Addressing that should be fairly easy though — we can add a list of names to keep as a parameter to removeDeadCtors. What do you think?

[VictorCMiraldo]

Yep, we would. Addressing that should be fairly easy though — we can add a list of names to keep as a parameter to removeDeadCtors. What do you think?

I'm a little concerned about a transformation that removes code automatically: it might change the code pirouette is executing without full consent of the user, and we might end up model-checking too different a contract. For instance, this could remove some redeemer constructors that would be used to reach a counter-example and the user wouldn't be aware because they forgot to add to the list of "don't remove". A way around that is to specify exactly what to remove, how about something like:

removeDeadCotrs :: M.Map String [String] -> ...

Then we can pass the type name and a subset of constructors to keep from that type. For instance, the transformation:

removeDeadCotrs (M.fromList [("ScriptPurpose", ["Spending"]), ("Action", ["A", "B"])])

Will remove all constructors from "ScriptPurpose" that are not in ["Spending"], and all constructors from "Action" that are not in ["A", "B"], but nothing else, really. If it detects any of these constructors as "not dead", it can warn us and replace it with a call to bottom @TypeInQuestion.

[VictorCMiraldo]

Also worth registering here, did you have a chance to check whether this transformation step improves the runtime in any larger example?

[0xd34df00d]

@VictorCMiraldo just did that — hardcoding sestConstructors stat > 14 as the stopping condition yields about 33 s without the pass. If all possible constructors are removed, then surely the run time goes down to less than a second. If I only allow removing [("ScriptPurpose", ["Rewarding", "Minting", "Certifying"])] (they do get removed), then the run time roughly stays the same.

The other (type, ctor) pairs that are seen as dead are

Action9467  Bid9468
Action9467  Hammer9469
Address6633 Address6634
Credential6625  PubKeyCredential6626
Credential6625  ScriptCredential6627
Data    B
Data    Constr
Data    I
Data    Map
ScriptContext7792   ScriptContext7793
ScriptPurpose7786   Spending7790
StakingCredential6629   StakingHash6630
StakingCredential6629   StakingPtr6631
StaticValParams7290 StaticValParams7291
TxInInfo6647    TxInInfo6648
TxInfo6680  TxInfo6681
TxOut6636   TxOut6637
TxOutRef6644    TxOutRef6645
ValParams7298   ValParams7299

(which indeed shows that we can't remove things blindly!)

Let me know what others are possible to remove. I think only some of Data could be, but, say, removing B alone doesn't help.

[VictorCMiraldo]

Interesting! I think that for the particular AuctionSpec example we have going, you can remove:

StakingCredential6629   StakingHash6630
StakingCredential6629   StakingPtr6631
Action9467  Hammer9469

The reasoning being that we don't use any staking things whatsoever, and the only predicate we're currently checking is only interested in the case where the Action is Bid. Any other constructors really can't be eliminated. If that doesn't make not even the slightest difference, I think we should perhaps park this PR and not merge it before chipping away at the more expensive performance perks. One such example is instead of removing constructors, change some of their types to rely on a (to-be-introduced) Set builtin, that is interpreted as a SMTLIB finite set. That won't be a trivial task, as we will also have to change functions that did some pattern matching on lists to also work over sets.

[0xd34df00d]

Oh that's cool! Merely removing Action's Hammer halves the run time, going down from 33-35 s to 17-19 s. Any of the StakingCredential's ctors doesn't give this effect.

Also, looks like our SMT translation doesn't handle ctor-less data types too well: removing both constructors of StakingCredential results in

FAIL
        Exception: user error (Unexpected result from the SMT solver:
          Expected: success
          Result: (error "Parse Error: <stdin>:2.8377: Unexpected token: ' )
        )

I'll take a look at that.

For the record, the full list of ctors to remove was

    toRemove = M.fromList [ ("ScriptPurpose", ["Rewarding", "Minting", "Certifying"])
                          , ("StakingCredential", ["StakingHash"])
                          , ("Action", ["Hammer"])
                          ]

[VictorCMiraldo]

Oh that's cool! Merely removing Action's Hammer halves the run time, going down from 33-35 s to 17-19 s. Any of the StakingCredential's ctors doesn't give this effect.

That's really interesting indeed. Can you check whether not removing Hammer but adding a isBid predicate to the precondition of the test in question would have any effect?

              ( [pir| \(res:Bool) (p:ValParams) (s:AuctionState) (a:Action) (ctx:ScriptContext)
                . and (isBid a) res |]
                  :==>: [pir| \(res:Bool) (p:ValParams) (s:AuctionState) (a:Action) (ctx:ScriptContext)
                        . False |]

I'd expect it to have a similar effect; but I think it is quite important that we say and (isBid a) res and not and res (isBid a), as we had before. They are semantically the same, but the symbolic engine does so much more work on the later, as it expands to if res then isBid a else False, which sets the engine off to find a combination of things that make the validator return True before making sure that isBid a.

[0xd34df00d]

That doesn't change the run time much for me. It drops from 33-35 s to about 31-33 s, but removing the ctors has way more effect.

Looks like it also implies that we'll need to interpret refinements on pirouette level instead of relying on the SMT being smart enough.

[0xd34df00d]

Closing as per discussion.

Just in case it'll ever be needed later, the branch is also archived as x-archive-dce-ctors.