Adding slice to map removes permissions of other slices in map

[ThomasMayerl]

In the following code, the first assert is successful. Based on the preconditions we know that, there is a key "found" in the map and thus, we have access to the entire slice cache["found"]. If we now add an empty slice cache["not found"] we can afterwards not prove anymore that we have access to the entire slice cache["found"]:

requires acc(cache, 1/2)
ensures res === let entry, ok := cache[str] in entry
decreases
pure func getSlice(cache map[string][]string, str string) (res []string)

requires acc(cache)
requires forall str string :: {str in domain(cache)} str in domain(cache) ==> (forall k int :: {&getSlice(cache, str)[k]} 0 <= k && k < len(getSlice(cache, str)) ==> acc(&getSlice(cache, str)[k]))
requires "found" in domain(cache)
requires "not found" in domain(cache)
ensures acc(cache)
ensures forall str string :: {str in domain(cache)} str in domain(cache) ==> (forall k int :: {&getSlice(cache, str)[k]} 0 <= k && k < len(getSlice(cache, str)) ==> acc(&getSlice(cache, str)[k]))
func tmp(cache map[string][]string) {
    assert forall k int :: {&getSlice(cache, "found")[k]} 0 <= k && k < len(getSlice(cache, "found")) ==> acc(&getSlice(cache, "found")[k])
    cache["not found"] = []string{}
    assert forall k int :: {&getSlice(cache, "found")[k]} 0 <= k && k < len(getSlice(cache, "found")) ==> acc(&getSlice(cache, "found")[k])
}

[jcp19]

do you get the same error if you use ints instead of strings as the type of keys?

[ThomasMayerl]

Yes, with ints the same issue is reproducible. For example, the following code shows the same issue:

requires acc(cache, 1/2)
ensures res === let entry, ok := cache[key] in entry
decreases
pure func getSlice(cache map[int][]string, key int) (res []string)

requires acc(cache)
requires forall key int :: {key in domain(cache)} key in domain(cache) ==> (forall k int :: {&getSlice(cache, key)[k]} 0 <= k && k < len(getSlice(cache, key)) ==> acc(&getSlice(cache, key)[k]))
requires 200 in domain(cache)
requires !(404 in domain(cache))
ensures acc(cache)
ensures forall key int :: {key in domain(cache)} key in domain(cache) ==> (forall k int :: {&getSlice(cache, key)[k]} 0 <= k && k < len(getSlice(cache, key)) ==> acc(&getSlice(cache, key)[k]))
func tmp(cache map[int][]string) {
    assert forall k int :: {&getSlice(cache, 200)[k]} 0 <= k && k < len(getSlice(cache, 200)) ==> acc(&getSlice(cache, 200)[k])
    cache[404] = []string{}
    assert forall k int :: {&getSlice(cache, 200)[k]} 0 <= k && k < len(getSlice(cache, 200)) ==> acc(&getSlice(cache, 200)[k])
}

[ThomasMayerl]

Another interesting aspect: If we access the map entry that we have access to, then we suddenly receive a postcondition error, that injectivity cannot be proven, instead of the assertion error:

requires acc(cache, 1/2)
ensures res === let entry, ok := cache[key] in entry
decreases
pure func getSlice(cache map[int][]string, key int) (res []string)

requires acc(cache)
requires forall key int :: {key in domain(cache)} key in domain(cache) ==> (forall k int :: {&getSlice(cache, key)[k]} 0 <= k && k < len(getSlice(cache, key)) ==> acc(&getSlice(cache, key)[k]))
requires 200 in domain(cache)
requires !(404 in domain(cache))
ensures acc(cache)
ensures forall key int :: {key in domain(cache)} key in domain(cache) ==> (forall k int :: {&getSlice(cache, key)[k]} 0 <= k && k < len(getSlice(cache, key)) ==> acc(&getSlice(cache, key)[k]))
func tmp(cache map[int][]string) {
    oldList := getSlice(cache, 200) // Here we just added this line, changes the reported error
    assert forall k int :: {&getSlice(cache, 200)[k]} 0 <= k && k < len(getSlice(cache, 200)) ==> acc(&getSlice(cache, 200)[k])
    cache[404] = []string{}
    assert forall k int :: {&getSlice(cache, 200)[k]} 0 <= k && k < len(getSlice(cache, 200)) ==> acc(&getSlice(cache, 200)[k])
}

[ThomasMayerl]

Upon further inspection, I think that Gobra is unable to reason about this with the addition of the getSlice function. However, we need this to specify valid triggers (this is a workaround to the triggering problem). In this instance, not specifying triggers, will not trigger Gobra to specify triggers by itself, which will make Viper do it, which then comes up with valid triggers. So in this instance, not specifying triggers at all and writing the snippet like this seems to work:

requires acc(cache)
requires forall key int :: key in domain(cache) ==> let entry, _ := cache[key] in (forall k int :: {&entry[k]} 0 <= k && k < len(entry) ==> acc(&entry[k]))
requires 200 in domain(cache)
requires !(404 in domain(cache))
ensures acc(cache)
ensures forall key int :: key in domain(cache) ==> let entry, _ := cache[key] in (forall k int :: {&entry[k]} 0 <= k && k < len(entry) ==> acc(&entry[k]))
func tmp(cache map[int][]string) {
    entry1, ok := cache[200]
    assert forall k int :: {&entry1[k]} 0 <= k && k < len(entry1) ==> acc(&entry1[k])
    cache[404] = []string{}
    entry2, ok  := cache[200]
    assert forall k int :: {&entry2[k]} 0 <= k && k < len(entry2) ==> acc(&entry2[k])
}

[ThomasMayerl]

I do think that the problem is that the triggers are not issued and when we change the map that Z3 cannot prove anymore that the conditions hold since nothing is triggered. This would also explain why we come a bit further when we add the line

oldList := getSlice(cache, 200)

However, in many cases not specifying triggers is not the solution because Gobra might then create invalid triggers (containing conditionals). I stumble upon more and more cases where the workaround with specifying a function giving back the appropriate slice in the map does not work anymore. I have also noticed that we already check for map accesses in triggers https://github.com/viperproject/gobra/blob/9db248cf4b35ee54701502c741ba2c0d64a80662/src/main/scala/viper/gobra/translator/encodings/maps/MapEncoding.scala#L146 The problem is that we don't check if map accesses are not on the top-level of triggers (e.g. when we quantify over the indices of the slice within the map like in {&cache[str][k]}).

I think that all of this means that

• by not specifying any triggers, Gobra will insert triggers containing conditionals (which is exactly what the code location from above tries to avoid).
• by specifying triggers like {&cache[str][k]} yourself, Gobra will not apply the pattern from the code location from above since the map access is not on the top level, leading to Logic error: Expected slice, array, map, or sequence, but got InternalSingleMulti([]string,([]string,bool))
• by rewriting the triggers using a function call, Z3 has difficulties proving the assertions.

Is there any possibility to also use the working MapEncoding when the map access is not on the top level of the trigger?

[ThomasMayerl]

Another (temporary) workaround seems to be to combine using the map triggers and a function call by adding an assertion that the map access equals the function call, like so:

requires acc(cache)
requires forall str string :: {cache[str]} str in domain(cache) ==> (cache[str] === getSlice(cache, str)) && forall k int :: {&getSlice(cache, str)[k]} 0 <= k && k < len(getSlice(cache, str)) ==> acc(&getSlice(cache, str)[k])
requires "found" in domain(cache)
requires !("not found" in domain(cache))
ensures acc(cache)
ensures forall str string :: {cache[str]} str in domain(cache) ==> (cache[str] === getSlice(cache, str)) && forall k int :: {&getSlice(cache, str)[k]} 0 <= k && k < len(getSlice(cache, str)) ==> acc(&getSlice(cache, str)[k])
func tmp(cache map[string][]string) {
    assert (cache["found"] === getSlice(cache, "found")) && forall k int :: {&getSlice(cache, "found")[k]} 0 <= k && k < len(getSlice(cache, "found")) ==> acc(&getSlice(cache, "found")[k])
    cache["not found"] = []string{}
    assert (cache["found"] === getSlice(cache, "found")) && forall k int :: {&getSlice(cache, "found")[k]} 0 <= k && k < len(getSlice(cache, "found")) ==> acc(&getSlice(cache, "found")[k])
}