Fix KEVM regression

[ana-pantilie]

https://github.com/runtimeverification/haskell-backend/pull/3398 has broken some KEVM tests:

make: *** [Makefile:544: tests/specs/mcd/vat-move-diff-rough-spec.k.prove] Error 1
make: *** [Makefile:544: tests/specs/mcd/vow-flog-fail-rough-spec.k.prove] Error 1
make: *** [Makefile:544: tests/specs/mcd/vow-fess-fail-rough-spec.k.prove] Error 1

We need to investigate. If there is a quick fix we can push that but otherwise we should first revert the problematic PR.

[ehildenb]

All coming from here; https://github.com/runtimeverification/evm-semantics/tree/master/tests/specs/mcd

Make heavy use of trusted claims (eg.): https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/mcd/vat-move-diff-rough-spec.k#L123

For example, here we are using #computeValidJumpdests(...), which we expect to be simplified for the rule to apply: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/mcd/vat-move-diff-rough-spec.k#L137

So somehow, the thing where we say "don't simplify the trusted claims" is too aggresive. Perhaps instead we need to say "don't simplify the trusted claims in ways that lead to case splits", or we need an annotation which allows users to specify components that should be simplified, or claims that should be simplified.

[ana-pantilie]

The tests/specs/mcd/vat-move-diff-rough-spec.k.prove spec is failing with the following error. I am investigating the cause. Edit: it's because Set concat is defined as total, the proof passes if I manually modify the Kore definition

anapantilie@Anas-MacBook-Pro: ~/RV/evm-semantics/mcd-var-move master!
$ ./kore-exec.sh                                                                                                                                                                                        [13:41:01]
kore-exec: [198331810] Error (ErrorBottomTotalFunction):
    Evaluating total function
        /* Fn Spa */
        Lbl'Unds'Set'Unds'{}(
            /* Fl Fn D Sfa */
            /* InternalSet: */ /* element: */ LblSetItem{}(
                /* Fl Fn D Sfa */
                /* Inj: */ inj{SortInt{}, SortKItem{}}(
                    /* Fl Fn D Sfa */ VarACCT'Unds'ID:SortInt{}
                )
            ),
            /* Fn Sfa */
            /* InternalSet: */ Lbl'Unds'Set'Unds'{}(
                /* element: */ LblSetItem{}(
                    /* Fl Fn D Sfa */
                    /* Inj: */ inj{SortInt{}, SortKItem{}}(
                        /* Fl Fn D Sfa */ VarACCT'Unds'ID:SortInt{}
                    )
                ),
                /* opaque child: */ /* Fl Fn D Sfa */ VarAC3'Unds':SortSet{}
            )
        )
    has resulted in \bottom.
Context:
    (InfoAttemptUnification) while attempting unification