Faulty Selection sort verification

[sebastianselander]

blog/assets/src/insertion-sort/VerifiedInt.dfy

Line 8 in 6069d9b

forall i: nat :: 0 < left <= i < right ==> a[i-1] <= a[i]

blog/assets/src/insertion-sort/VerifiedInt.dfy

Line 34 in 6069d9b

Ordered(a,0,a.Length) && Preserved(a,0,a.Length)

blog/assets/src/insertion-sort/VerifiedInt.dfy

Line 50 in 6069d9b

invariant Ordered(a,0,i)

They way the Ordered predicate is specified and then used makes it trivially true.
Ordered(a,0,a.Length) leaves us with 0 < 0 in the left-hand side of the implication.

[sebastianselander]

The specification only checks that the algorithm preserves all elements

[jtristan]

Good catch!

I think the following is a fix.

module M1 {

  ghost predicate Ordered(a: array<int>, right: nat)
    reads a
    requires right <= a.Length
  {
    forall i: nat :: 0 < i < right ==> a[i-1] <= a[i]
  }

}

module M2 {

  import opened M1

  twostate predicate Preserved(a: array<int>, left: nat, right: nat)
    reads a
    requires left <= right <= a.Length
  {
    multiset(a[left..right]) == multiset(old(a[left..right]))
  }

}

module M3 {

  import opened M1
  import opened M2

  twostate predicate Sorted(a: array<int>)
    reads a
  {
    Ordered(a,a.Length) && Preserved(a,0,a.Length)
  }

}

module M4 {

  import opened M1
  import opened M2
  import opened M3

  method SelectionnSort(a: array<int>)
    modifies a
    ensures Sorted(a)
  {
    for i := 0 to a.Length
      invariant Ordered(a,i)
      invariant Preserved(a,0,a.Length)
      invariant i != 0 ==> forall k : nat :: i <= k < a.Length ==> a[i-1] <= a[k]
    {
      var minValue := a[i];
      var minPos := i;
      for j := i + 1 to a.Length
        invariant i <= minPos < a.Length
        invariant a[minPos] == minValue
        invariant forall k : nat :: i <= k < j ==> minValue <= a[k]
      {
        if a[j] < minValue {
          minValue := a[j];
          minPos := j;
        }
      }
      if i != minPos {
        a[i], a[minPos] := minValue, a[i];
      } 
    }
  }

}

@stefan-aws could you double check?

This may or may not be the right fix to use for the blog post. If it is, next step will be to go back to the blog post and update accordingly.

[jtristan]

@atomb This is a striking example of a spectacular specification failure, do you know if the auditor would have flagged this?

[atomb]

This is a really interesting example! The auditor wouldn't detect this, but the proof dependency analysis almost would. Say you rewrite the ensures clause into two, like so:

  method SelectionnSort(a: array<int>)
    modifies a
    ensures Ordered(a,0,a.Length)
    ensures Preserved(a,0,a.Length)
  {

If you then run dafny verify --warn-contradictory-assumptions --log-format text VerifiedInt.dfy you'll get output with the following text (among a lot of other stuff):

[...]

  Assertion batch 31:
    Outcome: Valid
    Duration: 00:00:00.0355306
    Resource count: 24180

    Assertions:
      VerifiedInt.dfy(47,13): this postcondition holds

    Proof dependencies:
      VerifiedInt.dfy(47,13)-(47,33): ensures clause

[...]

This indicates that the only thing used to prove the Ordered postcondition is the postcondition itself. This isn't currently something we warn about, but I think it should be.

We currently warn about a proof of an assertion/postcondition that does not depend on the assertion itself, because that means it was proved vacuously. We don't warn, however, for a proof that depends only on the assertion being proved. For inline assertions, there may be legitimate situations where the proof is self-contained -- where the predicate is a tautology. For a postcondition, however, I think the situation almost certainly indicates a mistake. We should implement that check.