This project is read-only.

Termination of ghost code

Nov 16, 2011 at 4:22 PM
Edited Nov 16, 2011 at 4:27 PM

I am starting this discussion thread to avoid hijacking Ernie's report in the issue tracker.
I have a particular question about it, but feel free to use it to exchange more general ideas about termination in ghost code.

Regarding the general termination checks on ghost code (and not only ghost functions), I am still unconvinced that the following piece of ghost code should be considered terminating.

if (\forall \integer i; map[i])
  do()
else
  dont()

This is obviously related to decidability/computability issues and may go deeper into proof theory territory than VCC's ambitions, but I would like to be convinced that it is ok to write ghost code like this.

Francois

PS: I'm open to using other communication mediums to talk about this (just let me know when and how), although I have to admit the asynchronous aspect of the discussion board fits my time constraints a lot better at the moment. Plus, I'm just looking to be convinced right now, not to argue about it :)

Nov 16, 2011 at 7:07 PM
Edited Nov 16, 2011 at 7:09 PM

It definitely is ok to write ghost code like this when you quantify over finite domains since there are no decidability/computability issues. So if you would change this to

(\forall \integer i; a < i && i < b ==> map[i])

you definitely are on the safe side.

 

On first glance, your example looks in no sense worse than

assert (\forall \integer i; map[i]);

Operationally, both can be seen as case-distinctions on the current state of the abstract machine. In the case of assert, the machine will either skip (in case the assert is fulfilled) or go to a fail state (when the assert is violated). In your example, the abstract machine either executes the do() or the dont() part, depending on whether the the \forall-expression is true.

Considering termination of code as the property that the abstract machine executing the code will halt when it has performed a finite number of steps, your code terminates.

In the assert-case, decidability should not affect soundness because the prover must ensure that the assertion is fulfilled in all runs -- if it can prove that, fine. Actually, in verification we do not need to consider anything that comes after an assert when we fail to decide whether the assert is fulfilled -- failing decision of the assert, the verification simply fails.

In your example, however, it might be that we can not decide whether the assertion is true or false -- then, it is not clear which step can be made by the abstract machine. In verification this code should act like a case distinction (A => x) /\ (-A => y), effectively assuming that the assertion is either true or false. I'm not sure whether this is harmless or not.

Usually, however, the map in question will be constructed by a lambda expression (and maintained by appropriate invariants) in such a way that it is easy to prove or disprove the truth of your assertion.

Nov 21, 2011 at 12:12 PM

Thanks for your answer Sabine.

I completely agree that quantified formulas are trivially fine in most cases (including the ones you display). My concerns indeed come from the case where the quantified formula is assumed to be decidable (that is, when it appears in a control-flow altering statement other than an assertion). We could preface all such uses of quantified formulas with an assertion that the formula is either true or false (assuming that this is not trivially discharged by Z3), at the cost of a possibly major loss of precision.

Another solution would be to somehow come up with a convincing argument why it is ok to be in such a situation, whilst justifying why we need recursion in ghost code to be well-founded: the usual argument being "VCC only proves that the code implements the specification(/ghost code), then it is your job to make sure that the specification is not trivial" justifies the absence of termination checking, but makes it hard to justify a partial implementation of it.

Maybe the simple addition of a _(decidable) attribute on ghost predicates would be sufficient as a first step, as a means to make all assumptions of the verification explicit. Later on, one could go ahead and try to implement further decidability checks, proving that the implementation of _(decidable) predicates is indeed total and functional (probably by proving well-foundedness of the induction).

The main question now is if anyone, other than my constructive self, really needs this to feel confident in a "Verification Successful" answer (without assumes or axioms, and with verified bodies for all functions, of course...). 

Nov 21, 2011 at 2:37 PM

From Wikipedia (Undecidable problem):

"Undecidability of a statement in a particular deductive system does not, in and of itself, address the question of whether the truth value of the statement is well-defined, or whether it can be determined by other means. Undecidability only implies that the particular deductive system being considered does not prove the truth or falsity of the statement. Whether there exist so-called "absolutely undecidable" statements, whose truth value can never be known or is ill-specified, is a controversial point among various philosophical schools."

On "absolutely undecidable statements" I found the following paper:

http://dx.doi.org/10.1017/CBO9780511750762.012

It appears to me that in the end it comes down to whether you believe that an absolutely undecidable statement that can be expressed in a second-order formula exists. That would mean a formula for which no mathematical theory extending the mathematical theory of the VCC by additional axioms -- which is consistent and decides the formula -- exists. For many undecidable formulas, introducing additional axioms turns them into decidable ones.

Personally, I must say that everything not justified bothers me, so I can fully understand your concerns. Also, in order to communicate clearly what the VCC is sound against, it is important to either justify implicit assumptions or to make them explicit. In this case, I'm still not sure whether we need a _(decidable) attribute or whether we can find some proof of "everything we can possibly write down in the VCC is not absolutely undecidable". I suppose something like this is what you were looking for when you started the discussion.

Actually, I would file this issue not under "termination" but under "well-definedness" of the abstract machine executing the ghost code, considering that -- if there is such a thing as an absolutely undecidable statement -- there simply is no step defined that the machine can make. The way I see termination, I already assume that the code is executed but can still diverge due to loops or similar constructs -- for which termination checking was implemented.

Nov 23, 2011 at 1:35 AM
Edited Nov 23, 2011 at 1:36 AM

Okay, there seems to be some fundamental misunderstanding about what termination of ghost code means, and why it matters.

The reason that using ghost code in VCC is sound is that the concrete program (the program with all ghost code and data removed) simulates the full program (the one with the ghost code and data). More precisely, if you have any execution of the concrete program, there is a corresponding execution of the full program running alongside it, such that the concrete states always match up and the control states match up at the end of each conrete step. Given this simulation, if you prove that the full program never reaches a bad state (e.g., a state where an assertion fails), you immediately have a proof that the concrete program never reaches a bad state; if you prove that the full program has no nonterminating executions, then the concrete programs has no nonterminating  executions.

To construct this simulation, you need the ghost code in between sucessive concrete actions to terminate; if the ghost code between two concrete steps was to not terminate, there would be no path to get to the next concrete step. Note that ghost code must terminate under angelic nondeterminism, not the demonic nondeterminism that we use for concrete code; this means that you have to show that there exists some terminating execution of the ghost code (as opposed to the concrete code, which has to be correct for all executions). However, VCC does not take advantage of this - you reason about ghost code considering all possible executions, just to make reasoning about ghost and concrete code work the same way (ignoring concurrency, where we take advantage of the fact that we don't have to take scheduler boundaries before atomic ghost actions).

All of this is independent of what a state is (as long as you have something like a countable axiom of choice to show that you can make all the necessary nondeterministic choices for the ghost code). The easiest way to model the full logic of VCC is to just embed it within your favorite set theory. (You don't even need the subset axiom except to form the powerset of naturals.) Using this, you can write a simple formula capturing the set of executions of a program, even if it has quantification over infinite domains.

So in short, the answer is that there is no problem with having ghost code use uncomputable predicates, as long as the logic for reasoning about individual states remains consistent.

Nov 23, 2011 at 3:13 PM
Thanks Ernie.

I now remember how my discussion with Michal about this ended with him saying "ghost code is angelic", convincing me until I forgot about it. Now that it's written down somewhere, chances are I won't forget it again. Hope the public discussion will be of use to someone else as well.

As a side note to myself (for when I forget this and search for it), angelic non-determinism also takes care of the fact that VCC does not currently check that implementations for abstract functions are deterministic: the first call to the non-deterministic function with certain arguments fixes the behaviour of all subsequent calls with the same arguments. We may actually be able to make use of this in a smart way for specs that require the modelling of memoization.

On Wed, Nov 23, 2011 at 1:35 AM, erniecohen <notifications@codeplex.com> wrote:

From: erniecohen

Okay, there seems to be some fundamental misunderstanding about what termination of ghost code means, and why it matters.

The reason that using ghost code in VCC is sound is that the concrete program (the program with all ghost code and data removed) simulates the full program (the one with the ghost code and data). More precisely, if you have any execution of the concrete program, there is a corresponding execution of the full program running alongside it, such that the concrete states always match up and the control states match up at the end of each conrete step. Given this simulation, if you prove that the full program never reaches a bad state (e.g., a state where an assertion fails), you immediately have a proof that the concrete program never reaches a bad state; if you prove that the full program has no nonterminating executions, then the concrete programs has no nonterminating executions.

To construct this simulation, you need the ghost code in between sucessive concrete actions to terminate; if the ghost code between two concrete steps was to not terminate, there would be not path to get to the next concrete step. Note that ghost code must terminate under angelic nondeterminism, not the demonic nondeterminism that we use for concrete code; this means that you have to show that there exists some terminating execution of the ghost code (as opposed to the concrete code, which has to be correct for all executions). However, VCC does not take advantage of this - you reason about ghost code considering all possible executions, just to make reasoning about ghost and concrete code work the same way (ignoring concurrency, where we take advantage of the fact that we don't have to take scheduler boundaries before atomic ghost actions).

All of this is independent of what a state is (as long as you have something like a countable axiom of choice to show that you can make all the necessary nondeterministic choices for the ghost code). The easiest way to model the full logic of VCC is to just embed it within your favorite set theory. (You don't even need the subset axiom except to form the powerset of naturals.) Using this, you can write a simple formula capturing the set of executions of a program, even if it has quantification over infinite domains.

So in short, the answer is that there is no problem with having ghost code use uncomputable predicates, as long as the logic for reasoning about individual states remains consistent.

Read the full discussion online.

To add a post to this discussion, reply to this email (VCC@discussions.codeplex.com)

To start a new discussion for this project, email VCC@discussions.codeplex.com

You are receiving this email because you subscribed to this discussion on CodePlex. You can unsubscribe or change your settings on codePlex.com.

Please note: Images and attachments will be removed from emails. Any posts to this discussion will also be available online at codeplex.com