Unsoundness in program verification example without permissions

[marcoeilers]

Silicon verifies the following two files that students handed in in the Program Verification course. Each file contains an assert false. There are no other assumes or inhales, no permissions are used, and the tree domains look completely standard to me.

arlt_silicon_unsound.txt asserts false in line 133
erhart_silicon_unsound.txt asserts false in line 137

[mschwerhoff]

Cutting down the examples would be greatly appreciated :-)

[marcoeilers]

Reduced version:

function f(i: Int): Int
{ i }

method mm(current: Seq[Int])
    requires |current| == 2
{
  var next: Seq[Int]
  next := Seq[Int]()

  assert forall i: Int :: i >= 0 && i < 2 &&
            (forall j: Int :: j >= 0 && j < 0 &&
            (forall k: Int :: k >= 0 && k < 0 &&
              f(next[j]) > f(next[k]))
                ==> f(next[j]) == f(current[i]) - 1)
  assert false
}

[marcoeilers]

I think I've found the problem. Silicon emits this quantifier:

(assert (forall ((k@6@01 Int)) (!
  (and
    (and
      (>
        (f $Snap.unit (Seq_index (as Seq_empty  Seq<Int>) j@5@01))
        (f $Snap.unit (Seq_index (as Seq_empty  Seq<Int>) k@6@01)))
      (< k@6@01 0))
    (>= k@6@01 0))
  :pattern ((f%limited $Snap.unit (Seq_index (as Seq_empty  Seq<Int>) k@6@01)))
  :qid |prog.l13|)))

which is equivalent to false, as part of the nested auxiliary terms:

v1.decider.prover.comment("Nested auxiliary terms: non-globals (tlq)")
v1.decider.assume(tlq)

[marcoeilers]

Okay, I'm confused. If I just remove that line (

silicon/src/main/scala/rules/Evaluator.scala

Line 669 in faaaf16

v1.decider.assume(tlq)

), all tests still pass (and the unsound examples above fail to verify, as they should).

@mschwerhoff Can I just remove this line? What is it supposed to do, in what situation do we need it?

[mschwerhoff]

If I remember correctly, I used "global" quantifiers in an attempt to reduce triggering-related incompletenesses. It can (could?) happen that a new symbol (say, s2) is introduced under a quantifier (e.g. due to heap-dependent triggers, or joining symbolic evaluation paths), in which case any definition of that symbol (= definitional axioms) would become part of the auxiliary quantifier that Silicon emits in addition to the symbolic version of the source quantifier. Assume that the new symbol occurs in the quantifier's trigger, e.g. apply(s2, x), that there already is a term apply(s1, y) available, and that s1 == s2 is logically true. However, in order to learn that, Z3 needs to instantiate the auxiliary quantifier first, but to do so, it first needs to learn s1 == s2 ... Over the years, I made various attempts to retrospectively pull out such definitional axioms, e.g. by finding nested quantifiers that don't reference a variable from the outer quantifier. Maybe the unsoundness here stems from such an attempt.

Actually, the way tlqGlobal and tlq are computed, seems rather unsound: a quantifier q2 nested under a quantifier q1 is pulled out if q2 does not mention any variable bound by q1 — but the nested quantifier could be conditional, e.g.

forall x . false ==> forall y. false

It seems that the nested quantifier will be pulled out 😱

As to why commenting the line doesn't break anything: I don't remember being able to completely solve the original problem, but it could be that making aux-triggers heap-independent and various forms of caching (e.g. snapshot map caching) avoid the problems covered by our test suite. Disabling caching might reveal problematic cases.

Lastly, potentially related: #228, #611.

[marcoeilers]

Thanks for the explanation!

It seems that the nested quantifier will be pulled out

That's exactly what's happening here, yes.
Okay, then I'll have a look if I can restrict this quantifier pulling out to definitional axioms for new symbols, or otherwise restrict it to make sure it's sound.

[mschwerhoff]

From the top of my head I'd say that at least heap-summarising snapshots are always, since symbolic heap chunks exist unconditionally (or their permission value contains a conditional). Instead of later on attempting to detect global definitions via a syntactic analysis, it would be cleaner to mark them as global upon creation (there even is a isGlobal field in quantifiers). But I never took the time to change this (and apparently hacked in this unsound quantifier pulling code instead) ...