Underspecification leads to invalid proofs.

traiansf commented 6 years ago

The proved does not always detect potentially stuck states and, due to that, can prove erroneous statements.

Below @virgil-serbanuta and myself took advantage of the underspecification of division (division by 0 is unspecified) in the semantics to prove that M / N always reaches M /Int N, additionally ensuring that N =/=Int 0.

@grosu, @bmmoore please take a look. @andreistefanescu could you confirm? Also, could you advise on how complex would be to fix it?

Steps to reproduce

In k-distribution/samples-kore/kernelc
kompile kernelc.k
Consider the following program div0.c:
```
int sum_iterative
(int m, int n) {
 return m / n;
}
```
Using sum_iterative since it is already defined in the SYNTAX module.

and the corresponding spec div0_spec.k:

module DIV0-SPEC
 imports KERNELC

rule
 <fun>... FUN:Map ...</fun>
 <k>
   sum_iterative(tv(int, M:Int), tv(int, N:Int))
 =>
   tv(int, M /Int N)
 ...</k>
ensures N =/=Int 0
endmodule

krun --prove tests/simple/div0_spec.k --smt_prelude ../../include/z3/basic.smt2 tests/simple/div0.c

bmmoore commented 6 years ago

That looks bad. In general terms we should be able to compute a condition for not getting stuck.

andreistefanescu commented 6 years ago

@traiansf yes, this is a limitation of the prover. A better way of phrasing it is that the prover assumes that the semantics is "complete".

In theory, the condition can be arbitrarily complex, and thus undecidable. In practice, you can try to look at the cases when narrowing occurs (as opposed to rewriting), and check that the disjunction of the unification constrains if true. It should work when the narrowing only splits on boolean/integer values. I can give more details about the codebase if you decide to work on this.

traiansf commented 6 years ago

I believe we should either work on solving this problem or develop a "completeness checker", maybe similar to the Sufficient Completeness Checker of Maude. Because it's ok in theory to say the semantics should be complete, but in practice it would be unsafe to assume that of a reasonably large semantics.

Personally, I would advocate for a separate tool for checking completeness. The benefit of it would be that it's orthogonal to the prover and it doesn't clutter it even more.

grosu commented 6 years ago

Guys, this is the fifth time for me to discuss this issue. Not sure what's the best way to avoid wasting our/my time re-discussing things over and over again.

I agree with the checking completeness tool. That will be needed anyway for the semantics of K in matching logic, because there will be axiom stating that a step can only be made with one of the rules and with nothing else. So if we have a completeness checker, then this becomes simpler, too.

For the completeness checker, @traiansf and others, I think we can/should have a reduction to SMT or matching logic. That is, suppose that the rules in our semantics are, after lifting => to the top level,

phi_1 => psi_1
phi_2 => psi_2
...
phi_n => psi_n

Then what we need is to prove, in matching logic, the validity of:

|= phi_1 \/ phi_2 \/ ... \/ phi_n

The ML prover should take this be able to prove it. Some of the symbols can be constructors and their axioms can certainly help there; see the ML recent journal paper for how: http://fsl.cs.illinois.edu/index.php/Matching_logic, section 5.7

traiansf commented 6 years ago

I think what you propose would work only for a system without final states... Maybe we can define valid final states as a predicate and disjunct that with your condition.

joi, 9 nov. 2017, 14:26 Grigore Rosu notifications@github.com a scris:

Guys, this is the fifth time for me to discuss this issue. Not sure what's the best way to avoid wasting our/my time re-discussing things over and over again.

I agree with the checking completeness tool. That will be needed anyway for the semantics of K in matching logic, because there will be axiom stating that a step can only be made with one of the rules and with nothing else. So if we have a completeness checker, then this becomes simpler, too.

For the completeness checker, @traiansf https://github.com/traiansf and others, I think we can/should have a reduction to SMT or matching logic. That is, suppose that the rules in our semantics are, after lifting => to the top level,

phi_1 => psi_1 phi_2 => psi_2 ... phi_n => psi_n

Then what we need is to prove, in matching logic, the validity of:

|= phi_1 \/ phi_2 \/ ... \/ phi_n

The ML prover should take this be able to prove it. Some of the symbols can be constructors and their axioms can certainly help there; see the ML recent journal paper for how: http://fsl.cs.illinois.edu/index.php/Matching_logic, section 5.7

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/kframework/k/issues/2360#issuecomment-343139611, or mute the thread https://github.com/notifications/unsubscribe-auth/ACwZU0RghUIPGzKOE_W047D8QIujG0sXks5s0u99gaJpZM4QS8_b .

virgil-serbanuta commented 6 years ago

It seems that this might not be a bug that we can fix easily, so I guess it should be its own project, not just maintenance work which we do on the spot, right?

To make sure I understand, since I'm still new to matching logic:

Considering that in our rules we assume a T cell at the top, the full formula that we need to check would be |= ((exists x1..xm) (x1, ... xm)) -> (phi_1 \/ phi_2 \/ ... \/ phi_n), right?

virgil-serbanuta commented 6 years ago

It seems that Github ate some of my characters... The formula should be: |= ((exists x1..xm) <T>(x1, ... xm)) -> (phi_1 \/ phi_2 \/ ... \/ phi_n)

grosu commented 6 years ago

Something like that, @virgil-serbanuta . Note that the patterns phi_i also contain the constraints on their variables (the side conditions).

Yes, we cannot / should not fix this now in this Java version. This is tricky and will take some time. Also, I am pretty sure that our current version misses lots of important axioms, such as what is a constructor and what not, so most likely Z3 will not even have what it needs in order for the property to be provable. We should do this properly with the next version of the symbolic engine, based on the formal semantics of K that will be make public shortly.

bmmoore commented 6 years ago

I don't know how slow it would be, but I think it might not be very complicated to dynamically check it in the prover. At every single step is the prover is already finding a list of candidate rules, and for each rule computing a path condition PC_i for each, and throwing out rules where Z3 can prove PC_i is unsatisfiable before computing successor states according to the remaining rules. If we added one more query and Z3 can prove (not (or PC_1 ... PC_n)) is unsatisfiable, then we would know that the current step is complete.

kframework / k-legacy

Underspecification leads to invalid proofs. #2360