use old in trigger for direct array assignments

[Pointerbender]

This PR experiments with addressing 2 things:

1. It implements the suggested work-around for Snap encoding of array assignments #877 together with a regression test (the test suite indicated no regressions locally).
2. The selection_sort.rs test case was updated to use this fix in order to remove the auxiliary set function (verify/pass/arrays/{merge,selection_sort}.rs timeout issue #819).

Some notes apply to the approach chosen to make selection_sort.rs verify:

• A "dummy" body_invariant!(a[0] <= a[i]); was added to the outer and inner loops in order to correctly trigger the quantifiers.
• A change was made in prusti-viper/src/encoder/foldunfold/mod.rs to prevent Prusti from running into an encoder error when the old expresion was only present in the trigger, but not in the quantifier body. Without this change, selection_sort.rs will complain about a fold-unfold error. Since access predicates are not needed when the old expression is only present in the trigger, this should be sound (but please do double check this during the peer review).
• Without the auxiliary set function, the verification time roughly doubled, but it is still well within the -Pverification_deadline=180 compiler parameter. Execution time now hovers around ~2 minutes on my PC.

If the chosen approach sounds good, then this PR can be merged. I'm still a bit suspicious about why the set function yields better performance, I could look into this deeper with some guidance (possibly in a separate PR if that makes more sense). For now I came up empty-handed for what could be causing this performance regression (if this happens to be related to how Viper gives hints to Z3 based on the Viper/Silver syntax, then my current experience may not be of much help, but am willing to learn more!).

Thanks!

p.s. Issue #877 can be left open for now in case we want to file a bug report with the Viper back-end developers to investigate the old trigger issue. I posted a ~30 lines example there that hopefully is small enough to investigate.

[vakaras]

I have opened a Silicon issue viperproject/silicon#603. Before we merge this PR, let's see what the Silicon developers think.

[vakaras]

Seems like this is a Viper backend bug and we could merge this workaround until it is fixed.

[Pointerbender]

Thanks for the feedback @vakaras! I will address the requested changes some time tomorrow :)

[Pointerbender]

(The requested changes are ready and have been pushed just now, fyi.)

[vakaras]

Great, thank you!

bors r+

[bors]

Build succeeded:

• all-tests (macos-latest)
• all-tests (ubuntu-latest)
• all-tests (windows-latest)
• clippy-check
• fmt-check
• purification-tests
• test-crates