Invalid Triggers via Subslicing

[ArquintL]

The following program results in a Viper encoding with invalid triggers.
In particular, the first two assert stmts have valid triggers while the latter two end up having invalid triggers.
It's however unclear to me why the end up being invalid as the difference (also in the encoding) is 1 vs i-1 and it seems that Viper does not like the subtraction.

package search

func foo() (r []int, i int) {
	r = make([]int, 10)
	i = 2

	// @ assert forall j int :: { r[1:][j] } 0 <= j && j < len(r[1:]) ==> &r[1:][j] == &r[1+j]
	// @ assert forall j int :: { &r[1:][j] } 0 <= j && j < len(r[1:]) ==> &r[1:][j] == &r[1+j]

	// @ assert forall j int :: { r[i-1:][j] } 0 <= j && j < len(r[i-1:]) ==> &r[i-1:][j] == &r[i-1+j]
	// @ assert forall j int :: { &r[i-1:][j] } 0 <= j && j < len(r[i-1:]) ==> &r[i-1:][j] == &r[i-1+j]
}

[jcp19]

No arithmetic operators are accepted in triggers at the Viper level. As far as I can tell, the slice encoding had a hack for this since the very beginning to allow for some additions to be legally used as subexpressions in triggers containing slicing operations (e.g., the definition of loc in https://github.com/viperproject/gobra/blob/7fa4f86226e6648bd2c42f90eccebe64b79ff561/src/main/scala/viper/gobra/translator/library/slices/SlicesImpl.scala). Such a hack was not introduced for subtraction.

I'm not a big fan of this design. I think we should experiment with a cleaner design where all arithmetic operations are converted into function calls. This would allow us to write arithmetic operations inside triggers and removed these kinds of special behaviours.