Improvements in maps

[jcp19]

This PR extends the TypeEncoding with a method triggerExpr that is now used to encode expressions that occur in triggers (instead of encoding them with expression). This allows us to select well-formed triggers whenever the expression encoding generates ill-formed triggers. With this, we solve a long-standing issue where triggers containing a a map (like m[i] or i in range(m)) are translated to invalid triggers at the Viper level.

Besides, this PR introduces two quality of life improvements

• like in Viper, we now support the idiom key in m, where m is a map, whereas before we would have had to write key in domain(m). The previous idiom is still supported.
• the assert method in ViperWriter has been simplified to not generate a call to assert whenever the condition is TrueLit. Instead, it simplifies to the expression. This makes the resulting Viper code look much cleaner.

In the future, we may re-organize the map encoding as done in #606.

TODO:

• doc
• use default encoding for the fallback case instead of having it in the type combiner
• test with the slayers/path package in SCION

[Felalolf]

Please do the changes, then you can merge