Further optimisation of valid jump destination computation

Currently, we are computing jump destinations AOT, with the help of pyk. This allows us to handle programs with symbolic parts (such as immutable variables), but is slightly slower than the original approach that was fully integrated with the semantics.

We also have a PR open in KEVM that enables JIT computation, and which is much faster, but incomplete in that it does not account for cases when a jump is made into PUSH data, which should result in a EVMC_BAD_JUMP_DESTINATION error. Extending that PR to account for these cases as well is likely to end up being slower, since what we would need to do is, given a check for a jump destination I:

• take the 32 bytes of the program preceding I;
• check, for each of these bytes, from left to right, if the corresponding opcode is a PUSH-N, such that I is included in the N following bytes;
• make sure to skip all push data found in the process that does not include I.

In general, the assumption that no JUMP/JUMPI lands in PUSH data does not hold for arbitrary EVM code. However, it could be safe in the case of Kontrol, since we are working exclusively with EVM code coming from the compilation of Solidity files. Since the EVM execution never continues if such a jump occurs, I can't think of a use case for the compiler do be doing this deliberately. Perhaps we could ask the developers for their opinion.

If we think that this assumption will be safe, we could implement a layer in Kontrol only that always sets the jump destinations to .Set and only does a basic JIT check. This should give us a solid speed-up.

Alternatively, we could think of automatically generating K rules that capture valid jump destinations for each contract. These rules should be handled very efficiently by the LLVM backend.

Start by reviewing the open KEVM PR 2112 and the issue’s two proposed approaches: JIT handling of jumps into PUSH data or generated K rules for each contract. Consult Solidity developers about whether jumps into PUSH data can be excluded for compiled contracts. The issue does not define a selected approach or concrete completion criteria.