OCamlPro / owi

WebAssembly Swissknife & cross-language bugfinder
https://ocamlpro.github.io/owi/
GNU Affero General Public License v3.0
135 stars 17 forks source link

checking unbounded quantification #425

Open Laplace-Demon opened 2 months ago

Laplace-Demon commented 2 months ago

discussion 23/08

zapashcanon commented 2 months ago

Do you want to start implementing it ?

In the meantime, we can probably take care of providing the missing model_exists(var, prop) function, although I'm not completely sure how we could implement it because it is more complicated than simply asking if a model exists. (cc @filipeom)

Laplace-Demon commented 2 months ago

Do you want to start implementing it ?

In the meantime, we can probably take care of providing the missing model_exists(var, prop) function, although I'm not completely sure how we could implement it because it is more complicated than simply asking if a model exists. (cc @filipeom)

There won't be much problem with respect to code generation, and I've just realized we no longer need the PNF form, a simple recursion works.

  • model_exists(var, prop) which returns a boolean, indicating whether the proposition prop holds true for one possible value of var, prop may contain free variables.
  • model_forall(var, prop) which returns a boolean, indicating whether the proposition prop holds true for all possible values of var, prop may contain free variables.

In the mean time, just like what you said, I'm not sure if those are feasible in the solver.

filipeom commented 2 months ago

Maybe I misunderstood this, but it seems like a lot of work, we'd essentially be trying to reimplement quantifier elimination for fixed size bitvectors?

This makes the analysis inherently undecidable which will make the solver poop its pants. But why wouldn't we want to use Z3's quantifiers? They probably do a good job a trying to solve these? It would output a bunch of Unknowns for harder formulas but adding then in smtml would be easy

zapashcanon commented 2 months ago

No, we actually want to use Z3! We are going to craft an example of what we want to achieve and show it to you on Friday :)