Constructor calls with symbolic parameters

[RaoulSchaffranek]

KEVM currently doesn't handle constructor calls with symbolic parameters.
The problem is that the parameters are appended to the init code, and #computeValidJumpDests will start branching on them to collect all JUMPDEST locations. The branching leads to a path-explosion problem and eventually produces the following error message: Error internalising cterm: [PredicateExpected ....

Notice that the parameters are just data and not executable bytecode.
The init code will utilize a CODECOPY operation to copy the data from the init code to the memory.
Hence, looking for JUMPDESTS in this data is not needed.

We solved this issue by replacing the ahead-of-time computation of the valid jump destinations with a just-in-time algorithm. See: #2112

We also needed the following lemma to lookup opcodes in partially symbolic init code:

    rule [bytes-concat-left-lookup]:
        (A:Bytes +Bytes B:Bytes) [I] => A [I] requires 0 <=Int I andBool I <Int lengthBytes(A) [simplification]

[ehildenb]

The lemma can be added to KEVM as well as a test of it, in its own PR now, so that we can avoid that problem in the future.

[palinatolmach]

Closed as completed by runtimeverification/kontrol#596.