Missing axiom(s) in the axiomatization of sets

[viper-admin]

Created by bitbucket user OmerSakar on 2019-12-13 15:25 Last updated on 2019-12-13 15:52

When reasoning about a set and its subset (using the subset operator), there seems to be an axiom missing that relates the size of the subset to the other set. See the example below.

function setComp(): Set[Int]
ensures forall x: Int :: (x >= 0 && x <= 5) <==> (x in result)

method main2() {
    var set1: Set[Int] 
    set1 := setComp()
    
    assert Set(0, 1, 2, 3) subset set1 
    assert |set1| >= 4 // fails
}

Here we have a function setComp, its result is a set of integers between 0 to 5 (inclusive). In the method main3, we have a set set1 and we assign the result of the function setComp to it.

Reasoning directly about the size of the set is difficult (for example assert |set1| == 6 will not assert on its own). Instead we would like to reason about a lowerbound of the size, given that we can assert that some set (with a known size) is the subset of set1 (e.g. Set(0, 1, 2, 3)).

In the example, we assert that Set(0, 1, 2, 3) is a subset of set1 (on line 7). The expectation is that it can then be asserted that the size of set1 is greater or equal to 4 (as in line 8). Unfortunately, the last assertion fails.

After inspecting the set axioms Viper uses, I see that an axiom is missing which relates the size of the set and the subset.

[viper-admin]

@mschwerhoff commented on 2019-12-13 15:28

Does Carbon, the other Viper verifier, exhibit the same behaviour? If so, please file an issue at the [Silver repository](https://bitbucket.org/viperproject/silver), because both verifiers should use the same set of axioms for built-in data types such as sets.

[viper-admin]

@alexanderjsummers commented on 2019-12-13 15:31

Unfortunately, I don't think the two verifiers use the same set of axioms at the moment; neither from the same file, nor the actual same axioms. We should fix that, but until we do, I guess it makes sense to track issues separately.

[viper-admin]

Bitbucket user OmerSakar commented on 2019-12-13 15:36

I have submitted the (same) issue on the Carbon project.

[viper-admin]

@mschwerhoff commented on 2019-12-13 15:52

Thank you, and yes, please create a Silver issue whose description merely links to the Silicon and Carbon issues.

[mschwerhoff]

OmerSakar: Silicon now provides a command-line option to override, and thus extend, the set/multiset/sequence axioms Silicon uses. To locally fix the issue you reported, follow these steps:

1. Create a copy of Silicon's sequences.vpr, e.g. mysets.vpr

2. Add the following axiom to mysets.vpr:

   axiom subset_cardinality {
       forall s1: $Set[E], s2: $Set[E] ::
           {Set_subset(s1, s2), Set_card(s1)}
           {Set_subset(s1, s2), Set_card(s2)}
         Set_subset(s1, s2) ==> Set_card(s1) <= Set_card(s2)
     }
   

3. Save your issue as test.vpr and run silicon --setAxiomatizationFile mysets.vpr test.vpr