Conversation
This was recommended as a workaround for #2154 and #1957 by the Z3 maintainers (Z3Prover/z3#5243). The original issue arises because Z3 cannot assume that the exponent is non-negative, and so must infer that the result could potentially have type Real after evaluating the exponentiation. By adding the to_int cast, we opt in to integer semantics everywhere ^Int is used. Additionally, this commit adds a simplification rule for integer exponentiation that sends negative exponents to zero directly from K.
|
Note that we probably want to wait until the downstream projects have bumped their versions of Z3 to merge this. My progress on doing so:
|
Baltoli
changed the title
|
As it turns out, there's a transient prover bug in Z3 4.8.12 that breaks the Michelson test suite. To address this, we're dropping back to Z3 4.8.11. |
| RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.11 \ | ||
| && cd z3 \ | ||
| && python scripts/mk_make.py \ | ||
| && cd build \ | ||
| && make -j8 \ |
There was a problem hiding this comment.
I guess we actually need to adjust the packgaing rules...
There was a problem hiding this comment.
@dwightguth how do we want to approach this? Should K bundle its own Z3, or we just have instructions for people that they must separately install the correct Z3.
|
Marking this as a draft because Z3 The issue tracking this regression is #2247 |
|
@ehildenb @dwightguth This is ready to go now that the individual semantics have all been merged. There's a comment above regarding the packaging strategy that we may want to address, however - let me know what the best thing to do there is. |
|
I think the only realistic solution is to just update all the documentation (so README and install guide) to mention that users are expected to separately install a newer version of z3 if they don't have the correct version. |
|
OK @ehildenb - I'll add a stanza to the README and install guide to document that we expect users to separately install z3 version 4.8.11. |
| rule _ ^Int N => 0 requires N <Int 0 [simplification] | ||
|
|
There was a problem hiding this comment.
I'd like to see a test that exercises this new Z3 encoding. Anything that sends the symbol to Z3 on the Haskell backend should do, because it was causing crashes previously.
requires "domains.md"
module TEST
imports BOOL
imports INT-SYMBOLIC
syntax KItem ::= runLemma ( Bool ) | doneLemma ( Bool )
// -------------------------------------------------------
rule <k> runLemma(B) => doneLemma(B) ... </k>
rule N ^Int N' <=Int M ^Int M' => true
requires 0 <Int N andBool 0 <Int N'
andBool 0 <Int M andBool 0 <Int M'
andBool N <=Int M andBool N' <=Int M'
[simplification, smt-lemma]
endmodule
module TEST-SPEC
imports TEST
claim <k> runLemma(3 ^Int X <=Int 3 ^Int Y) => doneLemma(true) ... </k>
requires 0 <Int X andBool 0 <Int Y
andBool X <=Int Y
endmodule
I'd also like Daejun to double-check this new Z3 encoding of _^Int_, to make sure we are getting the correct semantics.
There was a problem hiding this comment.
Hmmm, is -1 the only special case? Maybe we should just remove this simplification rule altogether.
For -2, the result is 1/I, which I guess should go to 0 for 1 <Int I. I guess it's not worth adding these axioms yet until we see that we need them.
So let's remove this rule altogether.
There was a problem hiding this comment.
@ehildenb Note that it is not only for the simplification rule, but also for the z3 encoding in the hook: (ite (< #2 0) 0 (to_int (^ #1 #2))). As I mentioned, this encoding is incorrect for #1 being 1 or -1.
There was a problem hiding this comment.
Well, I think we could also change the smt hook to say (and (< 0 #1) (< 0 #2)), so that we don't have to think about the 0/negative cases. Then we could add K rules for specifically the various 0 cases N ^ 0 requires 0 <Int N, 0 ^ N requires 0 <Int N, 0 ^ 0.
There was a problem hiding this comment.
Let me clarify a bit, to make sure we are all on the same page:
Let X and N be an integer. Let Y be \trunc(X ^ N).
(\trunc means the truncation rounding, e.g., \trunc(-0.1) = 0, \trunc(0.1) = 0, \trunc(1.2) = 1, etc.)
Then we have:
X = 0implies( if N > 0, then Y = 0, else ( if N < 0, then Y = \infty, else Y = ??? ) )(see below for0^0)X = 1impliesY = 1X = -1implies( if N is even, then Y = 1, else Y = -1 )(X > 1 or X < -1) and N < 0impliesY = 0
Note that:
N = 0does not necessarily implyY = 1until we define0^0 = 1.N < 0does not implyY = 0. (See (1), (2), and (3) above for the counter-examples.)
Remark:
Regarding 0^0, many mathematicians seem to agree on 0^0 = 1 (see here), while WolframAlpha considers it undefined. We need to double-check what's the interpretation of (a specific version of) z3 for that.
There was a problem hiding this comment.
My simple suggestion would be to just put a guard for to_int, like: (implies (>= #2 0) (to_int (^ #1 #2))).
Those who want to reason about the negative exponent case, would need to come up with their own lemmas, simplifications, and/or custom z3 encodings, I think.
There was a problem hiding this comment.
FWIW, I think that if the type system contains both +\infty and -\infty, then 0^N should be undefined when N < 0
There was a problem hiding this comment.
Just adding one point here: as mentioned by @daejunpark, we should double-check the interpretation of 0 ^ 0, and, if I'm not mistaken, ** is underlying implementation of ^ for z3, correct? I've made a script to test x=0, y=0, n=x**y using different versions of z3's python module. Bellow is its output (version followed by the generated model, if can be achieved):
4.4.2.1.post1: [n = 0**0, y = 0, x = 0]
4.5.1.0: [n = 0**0, y = 0, x = 0]
4.5.1.0.post1: [n = 0**0, y = 0, x = 0]
4.5.1.0.post2: [n = 0**0, y = 0, x = 0]
4.8.0.0.post1: [n = 0**0, y = 0, x = 0]
4.8.5.0: [n = 0**0, y = 0, x = 0]
4.8.6.0: [n = 0**0, y = 0, x = 0]
4.8.7.0: [n = 0, y = 0, x = 0]
4.8.8.0: [n = 0, y = 0, x = 0]
4.8.9.0: [n = 0, y = 0, x = 0]
4.8.10.0: unknown
4.8.11.0: unknown
4.8.12.0: unknown
In this case, we may end up getting different outcomes for different versions of z3, so I think a more safe approach would be something on the lines of what @ehildenb said (adding K rules for the specific 0 and negative cases).
|
@ACassimiro ping. |
| rule 1 ^Int _ => 1 [simplification] | ||
| rule -1 ^Int N => 1 requires N %Int 2 ==Int 0 [simplification] | ||
| rule -1 ^Int N => -1 requires N %Int 2 ==Int 1 [simplification] | ||
| rule 0 ^Int N => 0 requires N >Int 0 [simplification] | ||
| rule X ^Int N => 0 requires absInt(X) >Int 0 | ||
| andBool N <Int 0 [simplification] | ||
| rule X ^Int 0 => 1 requires X =/=Int 0 [simplification] |
There was a problem hiding this comment.
@ehildenb @daejunpark I've implemented the special cases for integer exponentiation per the document here.
The SMT encoding will only send _^Int_ to Z3 if both X and N are strictly positive. In the cases where that might not be the case, these simplification rules will apply if we can define the result.
Cases where the result of the exponentiation would be ambiguous (0 ^ 0) or infinite (0 ^ -1) are left undefined; if users need to define these cases they can supply their own axioms.
| syntax Int ::= "~Int" Int [function, klabel(~Int_), symbol, functional, latex(\mathop{\sim_{\scriptstyle\it Int}}{#1}), hook(INT.not), smtlib(notInt)] | ||
| > left: | ||
| Int "^Int" Int [function, klabel(_^Int_), symbol, left, smt-hook(^), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)] | ||
| Int "^Int" Int [function, klabel(_^Int_), symbol, left, smt-hook((ite (and (< 0 #1) (< 0 #2)) 0 (to_int (^ #1 #2)))), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)] |
There was a problem hiding this comment.
I'm not sure what you're trying to encode here. This encoding means if (> #1 0) and (> #2 0), then 0, else (to_int (^ #1 #2)), which doesn't sound correct to me.
There was a problem hiding this comment.
You might want to do this?
UPDATE: please ignore this. it doesn't work, type-error.
| Int "^Int" Int [function, klabel(_^Int_), symbol, left, smt-hook((ite (and (< 0 #1) (< 0 #2)) 0 (to_int (^ #1 #2)))), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)] | |
| Int "^Int" Int [function, klabel(_^Int_), symbol, left, smt-hook((implies (and (< 0 #1) (< 0 #2)) (to_int (^ #1 #2)))), latex({#1}\mathrel{{\char`\^}_{\!\scriptstyle\it Int}}{#2}), hook(INT.pow)] |
There was a problem hiding this comment.
Also, if you have (< 0 #2), you don't need to add (< 0 #1), right? I mean, X ^ N will be well-defined for all X, if N > 0, right?
| rule 1 ^Int _ => 1 [simplification] | ||
| rule -1 ^Int N => 1 requires N %Int 2 ==Int 0 [simplification] | ||
| rule -1 ^Int N => -1 requires N %Int 2 =/=Int 0 [simplification] | ||
| rule 0 ^Int N => 0 requires N >Int 0 [simplification] | ||
| rule X ^Int N => 0 requires absInt(X) >Int 1 | ||
| andBool N <Int 0 [simplification] | ||
| rule X ^Int 0 => 1 requires X =/=Int 0 [simplification] |
There was a problem hiding this comment.
Have we double-checked that _%Int_ is behaving correctly on negative numbers here?
I remember that _%Int_ and _modInt_ had different behaviors for negative inputs on the first number, I just want to make sure we either get the right one, or write this code so that it doesn't matter which one.
|
Reopen when more SMT work is done. Maybe use a newer version also. |
6 participants
We were using the package manager-supplied version of Z3 in several Debian / Ubuntu Dockerfiles. This PR is an attempt to bring these all up to 4.8.12 (to deal with #2154 and #2210); when apt supplies a new enough version we can revert to using that one.
As best I can tell, Arch and macOS supply 4.8.12 through pacman and Homebrew respectively already, so don't need the manual installation.
To get the CI passing, I've had to cherry-pick the commits from #2210 into this PR (#2210 is therefore superseded by this PR and should be closed once this is merged); upgrading Z3 exposes the test failure that led to this problem in the first place, and so it needs to happen at the same time as the
to_intfix.