search

SSoelvsten / mlightdp

An extensive implementation of the LightDP language of Zhang and Kifer used to prove algorithms to be privacy-preserving
MIT License
3 stars 0 forks source link

Discharge proof obligations with Z3 #10

Open SSoelvsten opened 4 years ago

SSoelvsten commented 4 years ago

During the differential privacy type checking we currently generate proof obligations of numerical constraints, which are output into the resulting Dafny file. We experienced that Dafny has trouble with verifying a program, when it is requested to prove too many trivial statements such as 0 = 0, ˆq[i] − ˆq[i] = 0 etc. As long as no variables are involved, such as in the first expression, then it can be trivially discharged by computing the result. In the second expression one could also discharge this by normalising the equation and make terms cancel out. The proof obligations may become more complicated than that, at which point a much more sophisticated tool like Z3 would have to be used anyway. Hence, we suggest to merely discharge all proof obligations with Z3; if it fails we then output them to Dafny as we currently do.

SSoelvsten commented 4 years ago

When running Dafny through the console, these trivial assertions do not seem to confuse the proof verifier as much as it does in Visual Studio Code.

Being able to "remove" the trivial cases would make the output less cluttered and easier to grasp.

SSoelvsten commented 4 years ago

We started working on normalisation solving to take care of almost all trivial cases, but quickly gave up. One might instead take a look at disolver.zip and finish this rather than integrating with z3.

Going for z3 is much less error prone though.