Sensitive Behavior with Implications and Triggers

[totoyoyo]

Carbon shows some pseudorandom verification results involving implications and triggers. Running the code below using Carbon, disableCaching as true, and the current Nightly build of ViperIDE gives different verification results for each method, even though they are essentially the same. Command line Carbon would also yield the same outcome.

domain props {
    function a(i: Int): Bool 
    function b(): Bool
    function precondition(i: Int): Bool

    axiom preconditionAlwaysTrue {
        forall i: Int :: {precondition(i)}
        precondition(i)
    }

    axiom preconditionImpliesB {
        forall i: Int :: {precondition(i)}
        precondition(i) ==> b()
    }
}

// function dummy0() : Bool  
// function dummy1() : Bool  
// function dummy2() : Bool  
// function dummy3() : Bool  

method test1() {
    // Assumes a(i) is true if precondition(i) is true (which is always true from line 8)
    assume forall i: Int :: {a(i)} 
        precondition(i) && Set(1) == Set(1)   
            ==> a(i)

    assert a(0) // Should instantiate the above axiom, which instantiates precondition(i), which from line 13 should prove b() 
    assert b()   
}

method test2() {
    // same as above method except adding meaningless Set(2) == Set(2)
    assume forall i: Int :: {a(i)} 
        precondition(i) && Set(1) == Set(1) && Set(2) == Set(2) 
            ==> a(i)

    assert a(0)
    assert b()
}

method test3() {
    // same as above method except adding meaningless Set(3) == Set(3)
    assume forall i: Int :: {a(i)} 
        precondition(i) && Set(1) == Set(1) && Set(2) == Set(2) && Set(3) == Set(3)
            ==> a(i)

    assert a(0)
    assert b()
}

Also, uncommenting the dummy functions above the methods will rescramble the results, making some methods suddenly verify or fail verification.

[alexanderjsummers]

Here is a hypothesis from our earlier discussions, assuming a version with none of the spurious set == set conjuncts:

• assert a(0) assumes literal ¬a(0) (when checking the assert) or a(0) when assuming it afterwards; both result in adding a(0) to the E-graph, triggering an instantiation of the quantifier above; the body of the quantifier learned is equivalent to ¬precondition(0) V a(0). In particular, the proof of assert b() afterwards is in a state in which both ¬b() and a(0) are assumed literals. Let's consider what happens with the clause ¬precondition(0) V a(0) w.r.t. case-splits.
• IF the first disjunct is chosen first for case-splitting, then:

1. ¬precondition(0) is added as a decision literal and makes it into the E-graph
2. This causes both domain axioms to get instantiated
3. The result is that we learn both precondition(0) and b()
4. This gives a contradiction with assumption 1. and causes backtracking but, assuming clause-learning is enabled and kicks in, this will also cause precondition(0) to be added (after the back-track) as an additional unit clause.
5. This gives the same quantifier instantiations again, which are enough to complete the proof for the second assert (for the first, we get the proof directly via the assumption of a(0)).

• BUT, if instead the first case-split Z3 makes is on the second disjunct of ¬precondition(0) V a(0) then we end up with a second (redundant) copy of a(0) as an assumption, and no quantifier instantiations are unlocked (we don't have the bonus learned clause of course; that came from the other branch of the case-split). Since we can't get unsat in this case-split, the proof fails.

So, we can expect this example to succeed or fail based on Z3's choice of which literal to case-split on first.

Note that this is different from my own expectation: I had thought that Boogie (or possibly Z3) does something to make A ==> B behave in such a way that B is only ever considered when the terms from A are available in the E-graph. This doesn't seem to actually be the case. Changing the implication to explicitly encode short-circuiting, via A ==> A && B removes the instability. We should consider doing this in Carbon (or Boogie).

[totoyoyo]

A relevant Boogie option /causalImplies exists in its documentation, but isn't actually implemented.

  /causalImplies
                Translate Boogie's A ==> B into prover's A ==> A && B.

They have since removed the option: boogie-org/boogie#757.