Unable to prove assert directly after equivalent assume

[ThomasMayerl]

In the following code, we cannot prove the assert even though the assertion should be true because of the equivalent loop invariant. If we write an assume directly before the assert, the assert can still not be proven.

var items = []string{}

preserves forall k int :: {&items[k]} 0 <= k && k < len(items) ==> acc(&items[k])
func tmp() {
    itemMap := map[string][]string{}

    invariant acc(itemMap)
    invariant forall k int :: {&items[k]} 0 <= k && k < len(items) ==> acc(&items[k])
    invariant forall str string :: str in domain(itemMap) ==> let entry, _ := itemMap[str] in (forall k int :: {&entry[k]} 0 <= k && k < len(entry) ==> acc(&entry[k]))
    invariant forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> let entry, _ := itemMap[str] in (forall k int :: {&entry[k]} 0 <= k && k < len(entry) ==> exists l int :: 0 <= l && l < len(items) && items[l] == entry[k])
    for _, item := range items { 
        //assume forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> let entry, _ := itemMap[str] in (forall k int :: {&entry[k]} 0 <= k && k < len(entry) ==> exists l int :: 0 <= l && l < len(items) && items[l] == entry[k])
        assert forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> let entry, _ := itemMap[str] in (forall k int :: {&entry[k]} 0 <= k && k < len(entry) ==> exists l int :: 0 <= l && l < len(items) && items[l] == entry[k])
        v := itemMap[item]
        if v == nil {
            itemMap[item] = []string{}
        }
        entry, _ := itemMap[item]
        itemMap[item] = append(perm(1), entry, item)
    }
}

[jcp19]

what happens if we do not explicitly provide triggers to the quantifiers over maps?

[ThomasMayerl]

Then invalid triggers are inserted again by Gobra, meaning that Viper cannot verify the assertions

[ThomasMayerl]

In this instance, the triggers seem to be the issue. The correct invariant would be

forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> forall k int :: {&getSlice(itemMap, str)[k]} 0 <= k && k < len(getSlice(itemMap, str)) ==> exists l int :: 0 <= l && l < len(items) && items[l] == getSlice(itemMap, str)[k]

if we have another function

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)

Then we run into another issue Quantified resource getSlice(itemMap, str)[k] might not be injective. Gobra seems to forget that we can access all of the elemnts including the empty slice that we added. We can fix this by adding the following invariant:

invariant forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> getSlice(itemMap, str) != nil

We also need to change the permissions of the append to 1/2. As such, the following code now verifies:

var items = []string{}

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)

preserves forall k int :: {&items[k]} 0 <= k && k < len(items) ==> acc(&items[k])
func tmp() {
    itemMap := map[string][]string{}

    invariant acc(itemMap)
    invariant forall k int :: {&items[k]} 0 <= k && k < len(items) ==> acc(&items[k])
    invariant forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> getSlice(itemMap, str) != nil
    invariant forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> forall k int :: {&getSlice(itemMap, str)[k]} 0 <= k && k < len(getSlice(itemMap, str)) ==> acc(&getSlice(itemMap, str)[k])
    invariant forall str string :: {str in domain(itemMap)} str in domain(itemMap) ==> forall k int :: {&getSlice(itemMap, str)[k]} 0 <= k && k < len(getSlice(itemMap, str)) ==> exists l int :: 0 <= l && l < len(items) && items[l] == getSlice(itemMap, str)[k]
    for _, item := range items { 
        v := itemMap[item]
        if v == nil {
            itemMap[item] = []string{}
        }
        entry, _ := itemMap[item]
        itemMap[item] = append(perm(1/2), entry, item)
    }
}