Unsound rewrite when using requires with partial functions

[virgil-serbanuta]

versions:

$ kompile --version
K version:    v5.6.122-0-g77b76f004a-dirty
Build date:   Thu Jun 08 22:29:39 EEST 2023

$ kore-exec --version
Kore version 0.60.0.0
Git:
  revision:     f7a90ba41aa98d79f400099e2a27156e07543540
  branch:       HEAD
  last commit:  Fri May 5 08:23:49 2023 -0600

To reproduce: a.k

module A
  imports INT
  imports BOOL

  syntax KItem ::= "a"
  rule I:Int => a requires 10 /Int I <Int 0
  rule I:Int => a requires 10 /Int I >=Int 0
endmodule

spec.k

module SPEC
  imports A
  claim _Value:Int => a
endmodule

Command line:

$ kompile a.k --backend haskell && kprove spec.k

The proof passes, although the claim should fail when _Value is 0.

Note that the Haskell backend sends partial functions to z3 (i.e. it sends things like 10 /Int I < 0) without attempting to translate them properly - I think that Z3 division is undefined in the sense that it can be ANY value, while the K division is undefined in the sense that it has NO value.

[goodlyrottenapple]

Initial investigation confirms that it is indeed the last step in the proof, i.e. the check implication which sends the partial function to z3. We have discussed with @jberthold a potential design for the smt translation in the booster, which would add assertions over partial definitions in z3

[ehildenb]

I think in general, we cannot rely on Z3 for handling partial functions, because there is not a good compact way to axiomatize them to Z3 correctly (for how we want them defined).

So if we have some formula \phi(X, Y) we want to send to Z3, we should also compute the "definedness formula" \ceil(X, Y), which can be constructed using SMT attributes (or by inspecting #Ceil rules. We should first check if not \ceil(X, Y) is satisfiable, and if it is, then we cannot send \phi(X, Y) to Z3, we must use some other technique. But if not \ceil(X, Y) is unsatisfiable, then we can send the formula \phi(X, Y) to Z3 safely.

This basically amounts to handling definedness checks ourselves manually, instead of relying on Z3, because Z3 cannot handle partial functions correctly for our purposes.