This project is read-only.

Possible to declare a ghost for the value such that a given existential is satisfied?

Mar 3, 2013 at 9:14 PM
I am working on creating a verified implementation of strlcpy and I am encountering a tricky issue where VCC is able to verify one \exists assertion but not another. Specifically, src is a NUL-terminated string, and VCC can verify that there is an index j within [i, l] such that src[j] is a NUL character:
_(assert \exists size_t j; j >= i && j <= l && src[j] == '\0')
What I want to do is say that there is a k such that k <= l - i and src[i + k] == '\0'. Of course, one such value of k is the value j - i. If I substitute i + k for j, VCC should be able to verify:
_(assert \exists size_t k; i + k >= i && i + k <= l && src[i + k] == '\0')
_(assert \exists size_t k; k >= 0 && k <= l - i && src[i + k] == '\0')
_(assert \exists size_t k; k <= l - i && src[i + k] == '\0')
But it can't.

Is there a way to let a ghost size_t be the j of the \exists assertion?
Mar 4, 2013 at 9:28 AM
Edited Mar 4, 2013 at 10:51 AM
As far as I know, there is currently no (easy) way of doing what you ask. There have been many discussions about introducing a non-deterministic choice operator (choice: ('a -> bool) -> 'a), that would non-deterministically choose an element of type 'a that fulfills the predicate given as argument, after proving that there exists such an element. However, I don't think this has been implemented since then, and there are quite a few difficulties hiding in there.

In any case, I believe that your issue can be solved with well-chosen triggers (I think match_long(j), or similar triggers, maybe check the test suite?). Another possibility would be to make your existentials talk about \integers instead, so as to avoid overloading the provers with irrelevant proof obligations.

Unfortunately, I can't run tests at the moment, but I hope this short reply helps.

Cheers,
Francois

EDIT: Note that another way to get a ghost value that fulfills the predicate, when you know it, would be to explicitly have the witness somewhere in ghost code. In this case, you could take as an additional ghost parameter a ghost size_t that can be used as j and then use it in your proofs. Of course, this just delays the issue, but you can then probably write a _(def ...) or _(abstract ...) function that computes such a j from a NULL-terminated string. For that matter, you could also use such a function directly to extract a witness when needed. A possible contract for such a functional would be (memory-safety invariants are omitted, as I can never get them right on the first try and cannot iterate right now):

_(abstract size_t computeLength(unsigned char* ptr,size_t i,size_t l)
_(requires \exists size_t j; j >= i && j <= l && ptr[j] == '\0')
_(ensures res >= i && j <= l && ptr[res] == '\0'))

You now only have to come up with an inductive expression that computes it. Note that you can also use such a function as the loop invariant for strlen, for example, so it might be more generally useful than this particular application, and may even be worth exposing to the consumer code if you plan to distribute your verified library.
Mar 4, 2013 at 2:07 PM
Hello Francois,

Thank you for your response.

I tried adding triggers (hopefully I did this correctly), but VCC still did not verify the "shifted" \exists assertion.

This morning, I was finally able to get it working by beefing up the \exists assertion:
_(ghost const char *into_src = src + i;)
_(assert \exists size_t j; j >= i && j <= l && src[j] == '\0' && (j - i) >= 0 && (j - i) <= (l - i) && into_src[j - i] == '\0')
return i + strlen(src + i _(ghost l - i));
Yay!
Mar 5, 2013 at 11:44 AM
Excellent.

In my experience with VCC, making proofs using assertions is good if you're planning on pushing your project out and never coming back to it (or, never putting your project down in the first place), as updates to VCC, Boogie or Z3 may break any of the many tiny steps that ensure that the toolchain is able to discharge the generated proof obligations. This can be a nightmare to debug.

I recently had to dive back into 6 month old verified code to figure out why a proof was no longer going through, and cursed myself for trying to be clever and reducing the annotations to the strict minimum necessary to get the thumbs up from VCC (it turns out, at some point along the chain, one single invariant got instantiated differently between the two versions and broke the entire reasoning chain). So my advice (in general, not just to you) is "If you think a functional description can serve as documentation for your thought process, write it down, even if you later comment it out for style." Such a functional description not only explains what the code is meant to be doing with a clarity that an assertion will never be able to achieve, but will also help you in debugging your verification should it break further down the line.

Obviously, this is not very good advice for new projects whose specification is moving along with the code, but I think it is fairly good practice for standard libraries. This ends my rant :)

Cheers,
Francois