Full correctness

[traiansf]

Based on the previous design doc, coauthored with @virgil-serbanuta and @xc93, and implemented in the Haskell Backend, I sketched up a derivative one which would allow incorporating termination as part of the proof of a claim.

I'm not expecting this to have immediate impact, but I kept thinking that it's within our grasp to incorporate termination as part of the proving process and I wanted to follow that train of thought to get a better feeling.

Summary: the changes are simple, although they would require some support from the frontend and backend.

• ask the user to provide an integer measure pattern to (a group of) claim(s)
• while proving a claim guard its application (as a circularity/induction hypothesis) by a check that the measure has decreased

Note that the measure needs not be integer and the same ideas could be used with any well-founded order; however, using integers allows for the guards to be simply expressed and checked by the SMT.

[xc93]

I reviewed the first part of the document where the new "eventually" operator is defined. I'm not very convinced that the proposed operator correctness defines the intended meaning of total correctness.

[xc93]

In our papers, ≡ means the same thing as :=, meaning that the LHS is defined as an abbreviation of the RHS. But here I guess you mean |- ♢φ = φ ∨ (○♢φ ∧ •⊤), which is saying that the equation is provable.

How do you prove it? It's not obvious to me. By unfolding the fixpoint, I can prove

|- ♢φ = φ \/ •♢φ  // this is wrong. I misunderstood it with the usual eventually. 

But I don't see how that RHS is equal to φ ∨ (○♢φ ∧ •⊤).

[traiansf]

OK, maybe I'm missing the point here, but if I consider the "functor" defined on sets by
F(X) := φ ∨ (○X ∧ •⊤), which would read as
F(X) is the union between the set of configuration for which φ holds and those which are not stuck and whose all possible transitions lead into X.

Then wouldn't LFP(F) satisfy that LFP(F) = F(LPF(F))? If so, this should be enough to establish the equality you are wondering about.
Moreover, isn't is right that LFP(F) can be set-theoretically defined as ⋁ₙFⁿ(⊥)
Then noting that F(⊥) = φ ∨ (○⊥ ∧ •⊤) = φ ∨ (¬•¬⊥ ∧ •⊤) = φ ∨ (¬•⊤ ∧ •⊤) = φ ∨ ⊥ = φ is the set of configurations for which φ holds, we would have that

• F(F(⊥)) is the union between the set of configuration for which φ holds and those which are not stuck and whose all possible transitions lead into configurations for which φ holds.
• F(F(F(⊥))) is the union between the set of configuration for which φ holds and those which are not stuck and whose all possible transitions lead into the union between the set of configuration for which φ holds and those which are not stuck and whose all possible transitions lead into configurations for which φ holds.
• ...

Hence Fⁿ(⊥) seems to define the set of configurations for which φ holds on all paths in at most n-1 steps.

Since by the above expression for LPF(F), a configuration is in LFP(F) if there exists a natural number such that the configuration belongs to Fⁿ(⊥), this says that LFP(F) defines the set of configuration for which φ holds on all paths after a finite number of steps, which is in my opinion total correctness.

If we agree on this, I'll try to rewrite the existing text to incorporate this argument.

[traiansf]

about ≡: I was using it to denote semantic equivocalence; I've now replaced it with plain equality in the document.

[xc93]

Then wouldn't LFP(F) satisfy that LFP(F) = F(LPF(F))? If so, this should be enough to establish the equality you are wondering about.

Yes, I misunderstood it with the usual "eventually". It is correct that we can prove |- ♢φ = φ ∨ (○♢φ ∧ •⊤)

Btw, I highly suggest we use a different symbol than ♢. ♢ has already been used to represent (one-path) eventually, which is defined as ♢phi = mu X . phi \/ •X.

Isn't is right that LFP(F) can be set-theoretically defined as ⋁ₙFⁿ(⊥)

No, it is incorrect. See transfinite induction (https://en.wikipedia.org/wiki/Transfinite_induction).

Basically, ⋁ₙFⁿ(⊥) (which is a limit) may not converge. We need to compute F(⋁ₙFⁿ(⊥)) (which is F applied to the limit) and keep applying F again, until we consume all the natural numbers (again) and reach to another limit, and then apply F to the second limit. And keep repeating until finally, it converges.

Therefore, the only rigorous way (in my view) to reason about the semantics of a fixpoint is to following the semantics of matching logic and the Knaster-Tarski theorem. Unfolding can give us some intuition, but it won't give us a rigorous proof (unless we use transfinite unfolding).

However, in this case, I think if we can prove the following using the matching logic proof system, then we establish the correctness of the encoding thoroughly:

(Goal) |- LHS = RHS
where LHS = mu X.φ ∨ (○X ∧ •⊤)
and RHS = (nu X.φ ∨ (○X ∧ •⊤)) /\ (mu X . ○X)

[traiansf]

Thanks for pointing that out. It skipped my mind that F would need to be continuous.

I think the proposal would still work as-is (and as further detailed in the new commits) if F can be shown to be Omega-continuous, i.e, that it commutes with limits of increasing chains. As far as I know, most of the commonly used Fs have this property; I'll try to think whether it's something we can generally show for the kind of patterns we use here.

[xc93]

So, the claim

s1 -> ♢s2

states that P(s1) holds, where P(_) is an inductive predicate on configurations defined as

1. P(s2) holds
2. and if P(G) holds and G is not stuck, then for all G' => G, P(G') holds.

Is the above correct? And if so, I think s1 -> ♢s2 iff

s1 -> one-path-eventually s2 // if s1 is not stuck
s1 = s2 // if s2 is stuck 

Is that correct?

[traiansf]

I decided to remove that completely, as it was confusing to begin with (I just copied it over from the original all-path reachability design doc),

[xc93]

If the main object is to capture total correctness, then how about the following encoding?

reachability phi /\ WF
where reachability is either one-path or all-path reachability, already defined in matching logic
and WF := μX . ○X is the set of well-founded states (i.e., states that do not have infinite traces)

Its meaning is straightforward. Firstly, the reachability claim phi holds (either one-path or all-path, which is orthogonal). In addition, all execution traces must be finite (captured by WF).

Then, we may prove that all-path-reachability phi /\ WF is equal to the "eventually" defined above (but at this point I'm a bit suspicious).

[traiansf]

Of course, your proposal is straightforward, more general, and it would be nice to have support for it in the backend eventually. However, being more general might make it also harder to prove, and the proof itself might carry a nonnegligible amount of redundancy as it disconnects proving termination from proving reachability, when in fact you will probably want to use the same invariants, etc.

The approach I presented here is inspired from Dafny, and seems to work quite well there. Also implementing it in the backend might require less effort than implementing a more general solution.

[xc93]

I agree. I think it's definitely a good idea to prove both termination and correctness at the same time. What I'm suggesting is to use reachability phi /\ WF to justify the correctness of the "total-correctness eventually operator" encoding, by proving them equivalent using the proof system.

[ana-pantilie]

@traiansf thank you for writing this up! We probably will end up wanting something like this implemented, but I don't believe this implementation will live in the Haskell backend, but in pyk or some other client to the symbolic execution API.

@ehildenb where do you think a document like this should be stored? Maybe we can keep it in the backend repo and sometime in the future move it somewhere more appropriate?

[traiansf]

@traiansf thank you for writing this up! We probably will end up wanting something like this implemented, but I don't believe this implementation will live in the Haskell backend, but in pyk or some other client to the symbolic execution API.

I can move it to some other repo if somebody can point me to a more appropriate place. The main reason I started it here is the fact that it's based on the other All-Path-Reachability document which I think is still largely how the Haskell backend performs verification.