Master branch fails KEVM proof-suite

[ehildenb]

On K master (* 72d33ae0e0 - Update dependency: haskell-backend/src/main/native/haskell-backend (#2016)), which is immediately after merging this PR: https://github.com/kframework/k/pull/2016

I have a proof that loops. This comes from KEVM, prior to this it takes about 25s for this proof to run, but now it times out with a time limit of 50min.

Here is the minimized example test.k:

requires "domains.md"

module EVM
    imports INT

    configuration
        <k> $PGM:EthereumSimulation </k>
    syntax EthereumSimulation

endmodule

module INFINITE-GAS
    imports EVM

    syntax Int ::= #gas ( Int ) [function, functional, no-evaluators, klabel(infGas), symbol, smtlib(infGas)]
 // ---------------------------------------------------------------------------------------------------------
    rule #gas(_) <Int I          => false requires I <=Int 1                                       [simplification]
    rule #gas(G) <Int I +Int I'  => false requires notBool (#gas(G) <Int I orBool #gas(G) <Int I') [simplification]

endmodule

module VERIFICATION
    imports INFINITE-GAS

    syntax KItem ::= runLemma ( Step ) | doneLemma ( Step )
 // -------------------------------------------------------
    rule <k> runLemma(S) => doneLemma(S) ... </k>

    syntax Step ::= Bool
 // --------------------

endmodule

module INFINITE-GAS-SPEC
    imports VERIFICATION

    claim <k> runLemma(#gas(GAVAIL) <Int log2Int(G0) +Int 1)  => doneLemma(false) ... </k> requires 0 <Int G0 andBool G0 <=Int 1

endmodule

To reproduce the looping behavior, run:

kompile --backend haskell test.k --main-module VERIFICATION --syntax-module VERIFICATION
timeout 120 kprove test.k --def-module VERIFICATION --spec-module INFINITE-GAS-SPEC

Note the 120s timeout here. If you remove either of the lemmas in INFINITE-GAS-SPEC, it fails very quickly (4s or so).

On KEVM master, the proof that inspired this minimized example (it's been mangled a bunch to minimize it) passes in about 25s.

[ana-pantilie]

Since this passes with a version of the backend which is ~1 month old, I'm not that sure anymore that this is related to the predicate simplification loop (this is an older issue). So I think we could take a look at this before we get the predicate simplifier fixed. We should at least identify the version of the backend this starts failing, or check that this isn't actually an issue with the spec/semantics itself.

[MirceaS]

This issue was introduced by commit 67d4d23698551ba29228864fdff55a15d86f3d55

[ana-pantilie]

Hmm, that's weird! Could something have been broken in Bool unification?

[ana-pantilie]

@ttuegel Suggests to run with the equation debug logs and see if it gets stuck while simplifying the side condition.