Low sensitivity doesn't transfer when converting string to []byte

[henriman]

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19.

When converting a low string s to a byte slice ([]byte(s)), the resulting slice is not considered low.

Consider the following two examples. For both test00 and test01, neither postcondition can be established.

ensures low(res)
ensures acc(res) && forall i int :: { res[i] } 0 <= i && i < len(res) ==> low(res[i])
func test00() (res []byte) {
    res := []byte("test")
}

requires low(s)
ensures low(res)
ensures acc(res) && forall i int :: { res[i] } 0 <= i && i < len(res) ==> low(res[i])
func test01(s string) (res []byte) {
    res := []byte(s)
}

It seems that the Viper encoding does not relate the contents of the byte slice to the given string.