Description
Versions:
$ kompile --version
K version: v6.0.57-0-ga91e8fd25a-dirty
Build date: Jo aug 31 13:43:29 EEST 2023
$ kore-repl --version
Kore version 0.60.0.0
Git:
revision: 3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
branch: HEAD
last commit: Tue Aug 1 15:57:31 2023 +0100
Minimized example:
a.k:
module A-SYNTAX
imports BOOL
syntax A ::= "a" | "b" | split(Bool)
endmodule
module A
import A-SYNTAX
import BOOL
import INT
syntax Bool ::= f(Int, Int) [function, total, no-evaluators]
syntax Int ::= g(Int, Int) [function, total, no-evaluators]
syntax Int ::= h(Int, Int) [function, total, no-evaluators]
rule VAL1 +Int VAL2 <Int MAX => true requires VAL1 <Int MAX andBool VAL2 <Int MAX andBool f(VAL1, VAL2) [simplification]
rule split(B:Bool) => .K requires B
rule split(B:Bool) => .K requires notBool B
rule h(Val, Max) => h(Val +Int Max, Max) requires Val <Int 0 andBool 0 <Int Max
endmodule
spec.k:
module SPEC
imports A
claim split(M <=Int Z) => .K
requires X ==Int Y *Int M +Int Z
andBool g(X, M) ==Int g(Z, M)
andBool Y ==Int h(X -Int Z, M)
andBool 0 <Int M
endmodule
Command line:
$ kompile a.k --backend haskell && kprove spec.k
As far as I can tell, executing the split produces a remainder with M <=Int Z and #Not(M <=Int Z) and the backend tries to prune the remainder branch.
However, when doing that, it tries first to simplify h(X -Int Z, M). When simplifying, the Haskell backend may or may not check that the side condition is satisfiable (it is, anyway), but then it checks that the rule does not leave a remainder. When doing that, it checks that (not <rule-condition>) and <side-condition> is not satisfiable, which is not, since the side condition is #bottom. This makes the backend apply the simplification rule. After that, the backend attempts to simplify the result, which means that it attempts to apply the same simplification rule, which succeeds, which causes an infinite loop.