I understand that with nonlinear models Z3 and many SMT solvers reserve the right to say Unknown because not all nonlinear models are decidable. But many cases, such as this, are easy to a human and I'd hope easy to Z3.
In this instance an uninterpreted function with the semantics of reading bytes from memory must satisfy that the value returned fits within the number of bits read (8 * bytes).
The theorem statement I'm interested in relates the value of some integer with the value read from memory. The negated version should be unsatisfiable but returns unknown:
; getmem length mem := return length bytes from memory
(declare-fun getmem (Int Int) Int)
; naturally this number is less than 2 ^ (number of bits)
(assert (forall ((len Int) (mem Int)) (< (getmem len mem) (^ 2 (* 8 len)))))
(declare-const x Int)
(declare-const y Int)
(assert (< 64 y))
(assert (>= (getmem 8 x) (^ 2 y)))
(check-sat)
Why is it unknown instead of unsatisfiable? And is there a workaround for problems that act on bits? I've tried bitvectors before but they feel cumbersome.
I'm using z3 in the browser at microsoft's site: https://microsoft.github.io/z3guide/playground/Freeform%20Editing
XY Problem: I'm trying to use an SMT solver as a backend for handling basic arithmetic goals like this in Coq. I was hoping to use Z3 because it is well supported, but a lot of my goals deal with modulo arithmetic, bitwise operations, and bounds, which makes them very nonlinear.
As you noted, exponentiation is not easy to deal with for SMT solvers; and for very good reasons. SMTLib does not even define it; it's a z3 extension. Furthermore, z3 knows very little about the operator ^; it mostly works when the terms are all ground.
One thing to notice is the type of ^. It actually returns a real number, not an integer as you might expect. The reason for this is the possibility of the second argument being negative. (Consider (^ 2 (- 3)), obviously it is not an integer.)
Z3 (for better or worse) inserts to_real conversions whenever you use exponentiation to make the types work out. (I personally think that's a bad idea: All conversions should be explicit; but that's obviously not an opinion shared by everyone.)
So, what you want to do is to avoid ^ at all costs. Instead define your own power function, over integers, and see if that gets things through. Here's a try:
; pow x y = if (x < 0 || y < 0) 0 (x^y)
(declare-fun pow (Int Int) Int)
; getmem length mem := return length bytes from memory
(declare-fun getmem (Int Int) Int)
; naturally this number is less than 2 ^ (number of bits)
(assert (forall ((len Int) (mem Int)) (< (getmem len mem) (pow 2 (* 8 len)))))
(declare-const x Int)
(declare-const y Int)
(assert (< 64 y))
(assert (>= (getmem 8 x) (pow 2 y)))
(check-sat)
I declared pow as an uninterpreted function on purpose; as its definition will require recursion. While SMTLib does allow recursive function definitions, it's usually a good idea to avoid them if you can, as they make the logic semi-decidable. Also note the comment I put in: I'm intending this function to return 0 if either argument it receives is negative. (This is an arbitrary choice, make sure it works for your purposes!)
If you run the above, you'll see that z3 simply loops forever. We need to teach it a few things about our intended meaning of exponentiation. The most obvious one is:
(assert (forall ((a Int) (b Int) (c Int))
(=> (>= b c)
(>= (pow a b) (pow a c)))))
The above property is what we'd expect our pow function to satisfy: If you increase the exponent, the value gets larger. Now, z3 says:
unsat
as you'd expect. So, that's the "workaround" you're looking for. Of course, it worked for this "theorem," but it's not guaranteed to be sufficient for arbitrary uses of pow. If you pursue this path, you'll keep adding "helper" assertions as you go along. Whether that'll be sufficient for your purposes is anybody's guess. It all depends on what sort of properties you want to prove.
Also keep in mind that you might want to "prove" these helpers in a different system to make sure you're not asserting false propositions, creating an inconsistent state. This would be unsound. You mentioned Coq; that would be a fine choice of a theorem-prover to prove your helpers first.
Having said all this, I should also point out that the bit-vector theory is precisely designed to deal with machine-arithmetic. Your comment mentions you find it "cumbersome," but I'd recommend giving it another shot: I assume you're interested in proving things about computer programs using machine arithmetic, and that's precisely what bit-vectors are all about. (Of course, you can't be polymorphic about the length of bit-vectors, which does present limitations. For instance you won't be able to write your get-mem to return a valid type: How large should it be?) But in any case, bit-vector solvers are quite powerful, and they should be preferred over integer-solvers if at all possible, especially in the presence of non-linear constraints.