search

uwdb / Cosette

Cosette is an automated SQL solver.
BSD 2-Clause "Simplified" License
666 stars 54 forks source link

Simple WHERE test not possible #78

Closed matthiastz closed 4 years ago

matthiastz commented 4 years ago

setup: `schema PlaylistTrackSchema(PlaylistId: int, TrackId: int); table PlaylistTrack(PlaylistTrackSchema);

query q1 -- define query q1 SELECT a.TrackId FROM PlaylistTrack a WHERE TrackId < 100;

query q2 -- define query q1 SELECT a.TrackId FROM PlaylistTrack a WHERE NOT (a.TrackId > 99);

verify q1 q2; -- does q1 equal to q2?`

result: Invalid generated Coq code. Please file an issue.

{"size":[1],"status":"UNSAT"} generated/yXBSucoahCAUX.rkt:17:15: trackid: unbound identifier in module in: trackid context...: /root/.racket/6.8/pkgs/rosette/rosette/base/form/module.rkt:16:0 standard-module-name-resolver /Cosette-Web/backend/Cosette/rosette/server.rkt:38:10

(tested on https://demo.cosette.cs.washington.edu/)

stechu commented 4 years ago

Thanks for the report. Unfortunately, the prover part of the Cosette cannot reason about integer arithmetics. E.g. the be able to prove that these two queries are equivalent, a prover need to be able to reason about two things:

  1. TrackId is a integer
  2. NOT (a.TrackId > 99) is equivalent to TrackId < 100

This is a known issue. And I don't think we have a plan to fix it in the near term.

However, the model checking part could, that is why it returns UNSAT, which means the model checker thinks that these two queries are equivalent on some bounded model size.