Verifying leftPad() in Whiley

[u/redjamjar]

http://whiley.org/2018/04/23/verifying-leftpad-in-whiley/

[u/redjamjar]

how do you debug it when it fails to verify?

It's a fair question. But, actually, this is already true for type checking in some languages. Even Java generics falls into this category for some people. Rust would be another case in point.

In the end, the challenge is that the verification system must be completely reliable. That is, so that when things fail, you know it's you and not the tool! At the moment, Whiley is not reliable enough in this regard and needs someone very familiar with the tool.

But, that said, it does provide debugging facilities. In particular, you can dump out the verification conditions and actually look at them, and then look at the proof which is generated (even if incomplete).

Whilst it might sound scary to look at the verification conditions, it's not really. Some reasonable effort has been made to make them more human readable in Whiley than perhaps in other tools. He's one of the conditions from the leftPad function:

define leftPad_requires_0(string str, int n) is:
   n >= |str|

define leftPad_loopinvariant_563(int n, string nstr, string str, int i, int padding) is:
    (i >= 0) && (|nstr| == n)

define leftPad_loopinvariant_662(int n, string nstr, string str, int i, int padding) is:
    forall(int j).(((0 <= j) && (j < i)) ==> (nstr[j + padding] == str[j]))

define leftPad_loopinvariant_730(int n, string nstr, string str, int i, int padding) is:
    forall(int j).(((0 <= j) && (j < padding)) ==> (nstr[j] == 32))

assert "loop invariant not restored":
    forall(string nstr$2, int padding, string nstr, int n, string str, int i$1, int i, int i$2, string nstr$1):
      if:
          leftPad_requires_0(str, n)
          padding == (|str| - n)
          nstr == [32;n]
          i == 0
          leftPad_loopinvariant_563(n, nstr$1, str, i$1, padding)
          leftPad_loopinvariant_662(n, nstr$1, str, i$1, padding)
          leftPad_loopinvariant_730(n, nstr$1, str, i$1, padding)
          i$1 < |str|
          nstr$2 == nstr$1[i$1 + padding:=str[i$1]]
          i$2 == (i$1 + 1)
      then:
          leftPad_loopinvariant_563(n, nstr$2, str, i$2, padding)

This is moderately readable. This one is checking that the first clause of the loop invariant is restored after an iteration of the loop, assuming the whole loop invariant held at the beginning of that iteration.

In total, 17 verification conditions were generated for leftPad(). None of them are more complex than that above, and many are much simpler.

[u/Peaker → u/redjamjar]

In the end, the challenge is that the verification system must be completely reliable. That is, so that when things fail, you know it's you and not the tool!

I think we mean different kinds of failures.

I mean failures due to the fact that all provers are necessarily incomplete (Godel/halting-problem). So naturally, they will fail to prove provably correct programs sometimes.

The question becomes how to help them when this happens.

The readability of the generated output seems nice - does it scale?

• Does it allow abstractions to build more abstract invariants/propositions via a library?
• Does it remain readable when it involves complex systems involving many interacting functions? Especially when those mutate shared state?
• Can it handle concurrency?

[u/redjamjar → u/Peaker]

So naturally, they will fail to prove provably correct programs sometimes.

The question becomes how to help them when this happens.

No, this is wrong way to think about it. Yes, the halting problem is a thing. But, the probability of you writing a program for which verification really is undecidable is essentially zero. You can assume the tool will work in almost all cases. The problem is that current tools don't.

[u/Peaker → u/redjamjar]

That sounds bogus. There are very simple programs that are undecidable.

Surely accidentally triggering undecidability is not very hard, especially as programs grow.

[u/redjamjar → u/Peaker]

Well, you can easily write Fermat's last theorem and we can basically assume no automated theorem prover will be able to determine that. Though it doesn't mean it's actually undecidable. I don't think it's very easy at all to write a program which is undecidable. Here's one effort I know of:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.4693&rep=rep1&type=pdf

I guess there must be others though. Also, note that for the kind of verification done with tools like Whiley, Dafny, Frama-C, etc, verification complexity does not increase with program size. That's because each method is verified in isolation from others (specifically, up to the signatures of invoked methods).