Simplification rule with `symbolic` attribute applied on concrete input

[geo2a]

The issue is reported by @lucasmt pn Slack, see the thread. I'm quoting the message here:

This is really weird, I tried adding the normalization rule suggested for *Int:

rule A *Int B => B *Int A [concrete(A), symbolic(B), simplification(40)]

But now there's something odd happening when calling the freshUInt cheatcode. The ensures clause should be introducing the constraint ?WORD <Int 2 ^Int (8 *Int #asWord(ARGS)). But when calling kevm.freshUInt(32), it looks like this constraint is getting simplified to ?WORD <Int #powByteLen(32), which then causes the tool to crash. But this shouldn't be happening because the rule that introduces #powByteLen should only apply when the size is symbolic:

rule 2 ^Int (SIZE *Int 8) => #powByteLen(SIZE) [symbolic(SIZE), simplification]

Is it possible the the backend is ignoring the symbolic attribute?

[ehildenb]

~Looking at this rule, it looks to me like SIZE is concrete, it's 8.~ My mistake reading, it needs to be symbolic.

Perhaps the rule introducing fresh variables can be rewritten now that we're not needing ot commute the mulitplication in the first place?

?Word <Int 2 ^Int (#asWord(ARGS) *Int 8)

Then we don't get the "race" condition on the rules? @lucasmt can you try it?

[lucasmt]

For now we can work around this by using less general lemmas instead of A *Int B => B *Int A, for example

rule A -Int (X *Int Y) +Int (Y *Int X) => A [simplification]

So we are not blocked by this issue.

[lucasmt]

I've pushed a branch with a minimal reproducible example here: https://github.com/runtimeverification/evm-semantics/tree/reproduce-fresh-uint

The example can be reproduced by running the reproduce.sh script: https://github.com/runtimeverification/evm-semantics/blob/reproduce-fresh-uint/tests/foundry/reproduce.sh

[jberthold]

I have some problems reproducing this via the given branch reproduce-fresh-uint. Compilation with foundry-kompile (the one from reproduce.sh as well as a simple poetry run -C kevm-pyk -- kevm foundry-kompile --foundry-project-root tests/foundry --with-llvm-library --regen) fail with ValueError: Unsupported evm base sort type: int128 inside this function.

[jberthold]

For the record: After commenting out all int128 occurrences in tests/foundry/test/FreshInt.t.sol (in fact all except the test test_uint256), sol-to-k compilation succeeds on this (need to remove the tests/foundry/out directory to avoid stale data).

Investigation revealed that it is in fact not booster but kore-rpc that adds a constraint ?WORD <Int #powByteLen ( 32 ) with a concrete argument to #powByteLen. This makes booster call the LLVM backend with #powByteLen(32), leading to a crash.

The error can be triggered by running this execute request which calls freshUInt, taking a single rewrite step .

• kore-rpc will return a result that contains a constraint with #powByteLen(32)
• kore-rpc-booster will (fall back to kore-rpc and) crash on evaluating this constraint while simplifying the result

Next steps:

• The LLVM backend library should be modified to not crash the entire program in such cases
• The ticket is transferred to the haskell-backend repository because the erroneous simplification happens there.
• Further investigation is needed.

[jberthold]

• the translation to LLVM data structures should check for the no-evaluators attribute and refuse to translate function names that have this attribute. This could be implemented by modifying the (computed) attribute that checks whether a term is fully concrete to return False for such function calls.

[jberthold]

As mentioned, this wrong simplification happens inside kore-rpc execution, triggered by executing the freshUInt cheat code (the json request attached above)

A run with DebugApplyEquation logging shows the following log entries:

kore-rpc: [24889123] Debug (DebugApplyEquation):
    applied equation at /home/jost/work/RV/code/evm-semantics-with-deps/tests/foundry/out/kompiled/requires/normalizat
ion-lemmas.k:6:10-6:30 with result:
        \and{SortInt{}}(
            /* term: */
            /* T Fn D Spa */
            Lbl'UndsStar'Int'Unds'{}(
                /* T Fn D Sfa */
                Lbl'Hash'asWord'LParUndsRParUnds'EVM-TYPES'Unds'Int'Unds'Bytes{}(
                    /* T Fn D Sfa */ RuleVarARGS:SortBytes{}
                ),
                /* T Fn D Sfa Cl */ \dv{SortInt{}}("8")
            ),
        \and{SortInt{}}(
            /* predicate: */
            /* D Sfa */ \top{SortInt{}}(),
            /* substitution: */
            \top{SortInt{}}()
        ))
kore-rpc: [24890004] Debug (DebugApplyEquation):
    applied equation at /home/jost/work/RV/code/evm-semantics-with-deps/.build/usr/lib/kevm/include/kframework/buf.md:
40:10-40:51 with result:
        \and{SortInt{}}(
            /* term: */
            /* Fn Spa */
            Lbl'Hash'powByteLen'LParUndsRParUnds'BUF'Unds'Int'Unds'Int{}(
                /* T Fn D Sfa */
                Lbl'Hash'asWord'LParUndsRParUnds'EVM-TYPES'Unds'Int'Unds'Bytes{}(
                    /* T Fn D Sfa */ RuleVarARGS:SortBytes{}
                )
            ),
        \and{SortInt{}}(
            /* predicate: */
            /* D Sfa */ \top{SortInt{}}(),
            /* substitution: */
            \top{SortInt{}}()
        ))

I.e., the rule that introduces #powByteLen is applied when the argument of this function is #asWord(RuleVarARGS). Before the result is returned, this argument is somehow evaluated to 32, it is not clear yet how exactly this happens. Maybe the simplification happens before the bindings from unifying the rule and the input term are applied but it would be surprising that this did not surface earlier.

Postponing this for now, as we can avoid falling back to kore-rpc by modifying the freshUInt implementation, see https://github.com/runtimeverification/evm-semantics/issues/2038