search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

Incompleteness in CoerciveSubtypeOperator #104

Open DavePearce opened 7 years ago

DavePearce commented 7 years ago

In resolving #82, a problem related to incompleteness of subtyping is exposed. 

type nullint is (null|int x)
type boolint is (bool|int x)

assert:
   forall({any f} x):
       if:
          x.f is nullint
          x.f is boolint
       then:
          x.f is int

The proof produced is

 68. exists({any f} x).((((x.f is !!nullint) && (x.f is !!boolint)) && ((x.f () 
 70. exists({any f} x).(((x.f is !!nullint) && (x.f is !!boolint)) && (Simp 68) 
 69. ((x.f is !!nullint) && (x.f is !!boolint)) && (x.f is !int)  (Exists-E 70) 
 61. (x.f is !!nullint) && (x.f is !!boolint)                        (And-E 69) 
 63. x.f is !int                                                     (And-E 69) 
 57. x.f is !!nullint                                                (And-E 61) 
 60. x.f is !!boolint                                                (And-E 61) 
 74. x is {!int f, ...}                                               (Is-I 63) 
 77. x is {!!nullint f, ...}                                          (Is-I 57) 
 80. x is {!!boolint f, ...}                                          (Is-I 60) 
./test_type_73.wyal:4: null
assert:
^^^^^^^^^

The problem is that it is not correctly reasoning that ({any f}&{!(int) f, ...}&{nullint f, ...}&{boolint f, ...}) is equivalent to void.

My feeling is that this is due to the incompleteness of subtyping ... ?

DavePearce commented 7 years ago

UPDATE: yes, the problem is related to completeness of the CoerciveSubtypeOperator. This generates a bunch of queries like the following:

IS: {nullint f, ...} & !{nullint f, ...} == 0
IS: {nullint f, ...} & !{boolint f, ...} == 0
IS: {!(int) f, ...} & !{boolint f, ...} == 0
IS: {any f} & !{boolint f, ...} == 0
IS: {!(int) f, ...} & !{boolint f, ...} == 0

The key issue here seems to be that it's not expanding boolint and nullint eagerly. We can test this by expanding them manually. Try this:

assert:
   forall({any f} x):
       if:
          x.f is (null|int)
          x.f is (bool|int)
       then:
          x.f is int

No, this doesn't verify. The reason is that it doesn't pull unions out of records, so we end up with things like {!(int) f, ...} & !{(bool|int) f, ...} == 0

We can take it one step further:

assert:
   forall({any f} x):
       if:
          x is {(null|int) f}
          x is {(bool|int) f}
       then:
          x.f is int

This still doesn't verify. But, the last step ... should?

assert:
   forall({any f} x):
       if:
          x is {null f}|{int f}
          x is {bool f}|{int f}
       then:
          x.f is int

YES: this verifies!