Unsatisfiable branches not pruned

[sskeirik]

During a Michelson proof execution, I end up with 12 branches, 2 of which are reported by our script as failures, but these are spurious, because they are unsatisfiable. Note that Michelson currently uses krun with --search-final and not kprove as its symbolic execution driver and we manually inspect final states using a script to decide if they are solved --- i.e. <k> empty or <assumeFailed> contains true.

Version Info

== KMich Version
8497e1b
== K Version
RV-K version 1.0-SNAPSHOT
Git revision: 06e5157
Git branch: master
Build date: Fri Aug 21 10:14:15 CDT 2020
== Kore Version
Kore version 0.27.0.0
Git:
  revision:     7fe8fa29de30386f69d97b5a0220fe22521153fb
  branch:       HEAD
  last commit:  2020 Aug 18 13:49:39 -0500
  Build date:   2020 Aug 21 10:17:09 -0500
== Z3 Version
Z3 version 4.8.8 - 64 bit

Reproduce

git clone https://github.com/runtimeverification/michelson-semantics.git
cd michelson-semantics
git checkout 8497e1b
make deps-k
make build-symbolic
# run script to pretty print output
./kmich symbtest ./tests/symbolic/vote-simple.tzt
# raw run command without post-processing
krun -d ./.build/defn/symbolic --search-final ./tests/symbolic/vote-simple

Also see linked dump: https://drive.google.com/file/d/1kl_zBYApQdkx9En_merMW0NKkr9tEDEq/view?usp=sharing

Unsatisfiable Fragment and #Bottom Derivation

(1) { V3 [ #SemanticCastToInt ( V5 ) ] #Equals #SemanticCastToInt ( V6 ) }
(2) { V1 ==Int V5 #Equals false }
(3) { V3 [ #SemanticCastToInt ( V1 ) <- V4 +Int 1 ] [ #SemanticCastToInt ( V5 ) ] #Equals #SemanticCastToInt ( V7 ) }
(4) { V6 ==Int V7 #Equals false }

Then we derive:

(5) by 2 + 3 obtain { V3 [ #SemanticCastToInt ( V5 ) ] #Equals #SemanticCastToInt ( V7 ) } 
(6) by 5 + 1 obtain { #SemanticCastToInt ( V7 ) #Equals #SemanticCastToInt ( V6 ) } 
(7) by 4 + 6 obtain #Bottom 

---

(1) { V1 ==Int V5 #Equals true }
(2) { V3 [ #SemanticCastToInt ( V1 ) ] #Equals #SemanticCastToInt ( V4 ) }
(3) { V3 [ #SemanticCastToInt ( V5 ) ] #Equals #SemanticCastToInt ( V6 ) }
(4) { V3 [ #SemanticCastToInt ( V1 ) <- V4 +Int 1 ] [ #SemanticCastToInt ( V5 ) ] #Equals #SemanticCastToInt ( V7 ) }
(5) { V6 +Int 1 ==Int V7 #Equals false }

Then we derive:

(6) by 1 + 2 + 3 obtain { #SemanticCastToInt ( V4 ) #Equals #SemanticCastToInt ( V6 ) }
(7) by 1 + 4 obtain {  V4 +Int 1 #Equals #SemanticCastToInt ( V7 ) }
(8) by 6 + 7 obtain { V6 +Int 1 #Equals #SemanticCastToInt ( V7 ) }
(9) by 5 + 8 obtain #Bottom

NOTE

this is a modified version of the original proof, which uses Int -> Int maps instead of String -> Int maps. In that version, V1 and V5 are both strings, and we replace ==Int between with ==String, etc...

[ttuegel]

Please run the backend with the --bug-report option so that we can reproduce this, e.g. env KORE_EXEC_OPTS='--bug-report issue-2089' krun ....

Even without reproducing this issue, the derivations you are quoting will need to be handled by the SMT solver. You should look at the queries sent to the solver and decide which symbols should be translated for the solver (KORE_EXEC_OPTS='--log-entries DebugSolverSend,DebugSolverRecv,DebugEvaluateCondition'). Because there is no discussion of it in your bug report, I assume you have not marked any symbols to be sent to the SMT solver.

In your derivations, it also seems that you are treating #SemanticCastToInt as an injective function when it is not.

[sskeirik]

Thanks for your helpful reply!

To address your first point: I didn't mark it very clearly; the link I attached above is the dump from --bug-report .... I will copy it here as well: https://drive.google.com/file/d/1kl_zBYApQdkx9En_merMW0NKkr9tEDEq/view?usp=sharing

To address your second point: It is not clear to me how K decides when to forward things to the SMT solver. As far as I understand, all of the above symbols are built-ins. From what you are saying, it seems that built-in symbols need to be explicitly sent as well. From reading the docs, it seems that I have to add smt... attributes to rules or syntax declarations to allow them to be forwarded. How do I do this for built-ins?

To address your third point: the values in question are either actual K Ints, or they have been extracted from a symbolic map (whose value sort is K of course) and I know the actual value type should be Int, though K cannot specify that directly. What is the best way to proceed in this case, to remove the downcast?

[ttuegel]

As far as I understand, all of the above symbols are built-ins.

I don't think #SemanticCastToInt is a built-in symbol, and it seems like the SMT solver would need to reason about this.

From reading the docs, it seems that I have to add smt... attributes to rules or syntax declarations to allow them to be forwarded. How do I do this for built-ins?

For built-ins, this is done in the domains.md file distributed with K.

To address your third point: the values in question are either actual K Ints, or they have been extracted from a symbolic map (whose value sort is K of course) and I know the actual value type should be Int, though K cannot specify that directly. What is the best way to proceed in this case, to remove the downcast?

You should ask someone who is directly involved in writing semantics. I think evm-semantics has a similar problem, though.

[ttuegel]

Duplicate of #1416. I am opening a separate issue to follow up on a problem subsequently discovered.