#computeValidJumpDests from evm-semantics

[JKTKops]

This issue is for investigating the slow #computeValidJumpDests function from evm-semantics. Here it is minimized:

test.k:

module TEST
    imports COLLECTIONS
    imports BYTES
    imports K-REFLECTION

 // ---- for the proof --------------------------
    syntax KItem ::= run ( Step ) | done ( Step )
    syntax Step ::= Set

    rule <k> run(S) => done (S) ... </k>

 // ----------------------------------------------------------
    syntax Set ::= #computeValidJumpDests(Bytes)            [function, memo]
                 | #computeValidJumpDests(Bytes, Int, List) [function]

    rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, .List)

    syntax Set ::= #computeValidJumpDestsWithinBound(Bytes, Int, List) [function]

    rule #computeValidJumpDests(PGM, I, RESULT) => List2Set(RESULT) 
      requires I >=Int lengthBytes(PGM)
    rule #computeValidJumpDests(PGM, I, RESULT) => #computeValidJumpDestsWithinBound(PGM, I, RESULT)
      requires I <Int lengthBytes(PGM)

    rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => 
         #computeValidJumpDests(PGM, I +Int 1, RESULT ListItem(I)) 
      requires PGM [ I ] ==Int 91
    rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => 
         #computeValidJumpDests(PGM, I +Int 1, RESULT) 
      requires notBool PGM [ I ] ==Int 91

endmodule

test-spec.k

module TEST-SPEC
    imports TEST

 // ---------------------------------------------

    claim <k>
      run(#computeValidJumpDests(String2Bytes(
         [ascii string here]
      ))) => done( ?_ )
      ... </k>
           
endmodule

A typical program from KEVM (I selected one randomly) seems to be about 7000 bytes, so a 7000 character ascii string that demonstrates the problem can be found in the attached text file. Note that [ is special and represents the EVM opcode JUMPDEST. On this input, kprove takes about a minute.
ascii.txt
test-spec.k.txt (.txt extension is needed for github, just drop it)

This is on K version 5.1.0 and Kore version 0.49.0.0. To replicate:

$ kompile test.k --backend haskell
$ time kprove test-spec.k --backend haskell

[dopamane]

Here is a profile of test-spec.k:
valid-jump-prof.tar.gz
See kore-exec.eventlog.json for speedscope profile.
See kore-exec.prof.html for profiteur profile.

Command used to generate profile:
timeout -s INT 10m env GHCRTS='-p -l-au' kprove test-spec.k TEST --backend haskell --format-failures

[JKTKops]

This investigation seems complete. We expect that #2474 will improve the performance of #computeValidJumpDests.