Backend exits with ErrorDecidePredicateUnknown when Z3 reports "unknown"

[hjorthjort]

It seems the Haskell backend crashes with Error (ErrorDecidePredicateUnknown) when Z3 returns unknown and the prover can't proceed because of it. This means that certain tricky (non-linear) integer expressions can cause the backend to crash, when it instead could split and proceed. For example, I have the following assertion which, together with the rest of the assertions, makes (check-sat) return unknown:

(assert (not (and (= true (> (mod (* <0> <1> ) <2> ) 0 ) ) (not (= <2> 0 ) ) ) ) )

Interestingly, this assertion on its own (with <0>, <1>, <2> declared as Int) is satisfiable. So somehow the theory of Int has been sufficiently restricted that Z3 can't figure it out anymore. That might be something we can address. But more importantly, I would like to make sure the prover doesn't give up because z3 reports unknown.

In this case, bumping the timeout doesn't change the result (or the runing time): (set-option :timeout 400000000 )

Reproducing

I have a fairly self-contained example in the Michelson semantics: https://github.com/runtimeverification/michelson-semantics/tree/ErrorDecidePredicateUnknown

The branch is ErrorDecidePredicateUnknown.

To reproduce, clone the repo, check out the branch, and run ./script.sh (updates submodules, builds deps, runs the right proof and logs the smt queries).

Here's the claim it tries to prove:

   claim <k> PUSH nat X:Int ; PUSH nat Y:Int ; PUSH nat Z:Int ; MUL ; EDIV ; IF_NONE {} { DUP ; CDR ; SWAP ; CAR ; PUSH nat 0 ; DIG 2 ; COMPARE ; EQ } => . ... </k>
        <stack> .Stack => [ bool ?_ ] ; [ nat (Z *Int Y) /Int X ] ; .Stack </stack>
    requires X >Int 0
     andBool Y >Int 0
     andBool Z >Int 0

This will crash due to issuing (assert (not (and (= true (> (mod (* <0> <1> ) <2> ) 0 ) ) (not (= <2> 0 ) ) ) ) ) to Z3.

Another claim that produces a similar result, but without taking any semantic steps, is the following:

  claim <k> PUSH nat X:Int => ?_ ... </k>
        <stack> .Stack => ?_ </stack>
   requires (Y *Int Z) modInt X ==Int 0

As you can see, the issue is saying anything about non-linear formula in the context of the rest of our semantics.

[ttuegel]

This means that certain tricky (non-linear) integer expressions can cause the backend to crash, when it instead could split and proceed.

But more importantly, I would like to make sure the prover doesn't give up because z3 reports unknown.

This is expected, and we have no intention of changing this behavior. The backend cannot possibly tell the difference between these scenarios:

1. The result is unknown, but the path condition could split on some variable and continue to make meaningful progress.
2. Z3 needs more time or memory.
3. There is a real problem with the lemmas sent to Z3.

Only the user can distinguish these scenarios. If the backend continues rewriting carelessly, the user loses any context that could help them solve the problem. The backend halts to report an error so that the user has at least a chance of correcting the underlying problem.

Also, more broadly, it's not the backend's job to tame Z3.

[ehildenb]

Well I think we need to discuss the best way to solve the issue that prompted this one, which was about how the backend is halting when checking the initial state for feasibility, and everything is getting sent to Z3 which cannot make a decision because some non-linear arithmetic is involved. Rikard can explain better, but my understanding is the initial state has a sub-constraint that looks like this:

        0 <Int X
andBool 0 <Int Y
andBool 0 <Int Z
andBool 0 <Int (X *Int Y) %Int Z

But Z3 is returning that this is unknown satisfiabiity. How can we inform the Haskell backend to make progress beyond this point? We have one solution, which is to define a wrapper:

syntax Int ::= #ourExpression(Int , Int , Int) [function, no-evaluators, smtlib(ourExpression)]

rule (X *Int Y) %Int Z => #our_expression(X, Y, Z) [simplification]

So then Z3 sees the uninterpreted function instead.

But it seems tedious to do this for every type of input state that Z3 cannot decide if it's feasible or not. Is there a better way to inform the backend that we know this is feasible?

@hjorthjort did I explain it correctly?

[hjorthjort]

Yes, that's correct. I should add that the assertion from sub-constraint is reported as satisfiable if it is stated on its own in a z3 session, but it becomes unknown when taken together with the other assertions for the semantics

[hjorthjort]

This is expected, and we have no intention of changing this behavior. The backend cannot possibly tell the difference between these scenarios:

1. The result is unknown, but the path condition could split on some variable and continue to make meaningful progress.
2. Z3 needs more time or memory.
3. There is a real problem with the lemmas sent to Z3.

Only the user can distinguish these scenarios. If the backend continues rewriting carelessly, the user loses any context that could help them solve the problem. The backend halts to report an error so that the user has at least a chance of correcting the underlying problem.

It seems to me that the best course of action depends on what the user concludes.

If (2) is the case, I can increase time and memory for Z3 with a flag. If (3) is the case, the backend does the right thing and halts and I can inspect the situation. But if (1) is the case, I don't really have any option. I need to treat it as (3) and massage Z3 into reasoning about things it's not great at reasoning about. In this case, I think I would like to be able to somehow tell the backend to keep going.

Like @ehildenb said, we have this workaround, but it seems tedious and may not be the right course of action (because we need to change every instance of a pattern into an uninterpreted function, regardless if Z3 is struggling with that particular instance or not).

[ttuegel]

I think I would like to be able to somehow tell the backend to keep going.

How would you like to do that?

[hjorthjort]

I was thinking a flag, like --split-on-decide-predicate-unknown or similar, unless we want to make the ErrorDecidePredicateUnknown into a warning instead, in which case the existing --warnings-to-errors and --error-entries flags could be used to turn it back into an error when preferred.

[hjorthjort]

Here's a minified Z3 script that reports unknown. Seems the issue is with the big assertion for "Add Liquidity Params".

So it seems related to the helpers we use in this file: https://github.com/runtimeverification/michelson-semantics/blob/master/tests/proofs/dexter/dexter.md#putting-it-all-together

Basically, in order to run the proofs without having to specify the side conditions that the input values are values that would be legal in Michelson, we use the #runProof semantic step with an ensures class to check if parameters are valid.

The minified example only keeps the first of the assertions created by this structure, but I tried a few other ones and they seemed to trigger the same issue.

transcript_minified.smt2.txt

[hjorthjort]

Here's the full, unminified transcript transcript_full.smt2.txt

[ttuegel]

I am using Z3 4.8.9, and I cannot reproduce this unknown. The minified and full transcripts you provided return sat.

[hjorthjort]

That's good news. I'm using Z3 4.8.7, will try an upgrade