Experiment: Less duplication, more aggressive let simplification

[gsps]

This PR adds let-bindings in favor of duplicating code in two more places (match desugaring and assertions for ADT field selections). Conversely, it also adds an additional let-simplifications step in InoxEncoder, as encoded functions would so far not benefit from such simplifications and end up in queries to solvers.

[gsps]

The change doesn't seem to have any tremendous impact on performance. Integration tests run in roughly the same amount of time, while non-integration tests might be marginally slower.

It seems the sbt test step (i.e. non-integration tests) previously consistently took around 2m30s, while on the two CI runs here it took ~30s longer, but this is obviously not a great benchmark. I manually looked at the newly-introduced verification.simplify timer for the examples run in sbt test and there are only two occasions on which it takes more than 50ms. So I'm not sure where these slowdowns -- if they're real -- even come from.

@samarion Did we ever have a proper CI for verification times?

[samarion]

No, but I believe the main blocker is performance inconsistency within the SMT solvers. The solvers are typically fairly deterministic but rely on the input SMT-LIB to "seed" their heuristics. Since the Stainless transformation pipeline isn't 100% deterministic (because of non-deterministic ordering of identifier freshening), the performance can vary quite a bit for no good reason.

About these simplifications: I also worked on (and fiddled with) the simplifier infrastructure quite a bit and my main take-away was that making the input simpler for humans (as in less duplication and smaller ASTs) doesn't actually help the SMT solvers that much. IIRC, the only simplifications which really made a difference were

1. Reducing the exponential growth of unfoldings. There were two main transformations which helped for this, namely
   a. merging function calls which appear in multiple branches (see mergeFunctions in Inox), and
   b. dropping function calls from assertions which aren't in the VC context (but this also somewhat weakens the solving procedure).
2. Introducing domain-knowledge assertions, e.g. that function calls don't depend on ghost argument values (used in Stainless type encoding IIRC).

[gsps]

Thanks, that's very interesting! Viktor actually mentioned something like mergeFunctions the other day, so I shouldn't be surprised to discover that you actually foresaw this :-)

The changes in this PR remove some exponential growth, but at least the tweak for scrutinees probably doesn't apply to many of our (existing) test cases. I did stumble on the issue while working on imperative code, where a simple x.field match { ... } can grow quite dramatically due to Imperative + TypeEncoding + AssertionInjector. In that context it scraped ~8s off a 30s VC, so it seemed quite worthwhile.

Despite this PR not making a significant dent in our CI runtime, I'm still leaning toward merging it, if only to make everyone's life easier in reading the resulting TIP files.

There are, however, some reservations wrt. Streams, since let-binding intermediate expressions drops RecursiveTypes in some places (we drop them in computeType, @jad-hamza pointed out). This seems like a general source of brittleness in the Inox type-system, so I didn't intend to solve it on this PR.

[samarion]

We usually try not to simplify within the Deconstructor to make sure transformations are as predictable as possible. You could add the corresponding transformation within one of the various simplify procedures.

[gsps]

Okay, I'll see if I can find some simplification that's already applied anyways. I guess I'd still like to add an assertion in AnnotatedType that ensures we never end up with an empty list of annotations (which is impossible to spot in the pretty-printed tree!).

[samarion]

I guess an alternative would be to replicate part of the type inference logic from the type checker. In the long run, it probably makes more sense to move all the assertion checks there anyway.

[gsps]

You mean add the assertion check for ADTSelector in TypeChecker directly?

[samarion]

Well, all of the assertion checks injected in this class, really. It's not quite as good in terms of separation of concerns, but it makes sense to centralize all the checking.

Using let-bindings with type inference would also be reasonable and possibly not that difficult to implement. Actually, it would be great if we could add a simple locale type inference phrase to Stainless to compensate a bit for the lack of dependent types in Scala.

[vkuncak]

Astonishingly, this is almost merge-able, but I guess it's not clear if we want it?