Collect Data on Rule Traces and Performance Across Proof Suite

[ehildenb]

Modify the Makefile to dump the output of each proof after 100 steps.

Inspect the output for unsimplified functions we can add functional lemmas for.

See further discussion below.

[JKTKops]

Per discussion we went with depth 150 and a timeout of 2000s. If a file is empty then the test likely timed out. Tarball is attached.
depth150.tar.gz

[ehildenb]

make tests/specs/evm-optimizations-spec.md.prove TEST_SYMBOLIC_BACKEND=haskell

each claim will take about 10-15 K steps, so we should make sure the log for this file gets split into the individual rule traces.

Then we want to analyze (in the rest of the proof-suite) how "often" these rule traces occur in the other traces present in the system.

[JKTKops]

Here's some output from a first pass at using the new one-line logs to extract information about which steps of a proof are slow.

The proof used was tests/specs/benchmarks/storagevar00-spec.k, specifically chosen because it passes fairly quickly so it would have less turnaround time. Therefore the data probably isn't very interesting 😅.

test.txt

[ehildenb]

@JKTKops looks great. It might be interesting to do some different types of passes over the data. Can you try:

• Dedupe the rules (so use teh average duration as the duration for the rules). Look for outliers.
• Look for outliers among different applications of the same rule. If rule X normally takes 2s, but the 13th application, it takes 50s, that's interesting.

[ehildenb]

Also, here is just raw frequency of occurance given the data you posted above:

      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1042:10-1043:25
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1064:10-1066:35
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1082:10-1083:35
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1087:10-1088:35
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1227:10-1233:20
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1977:10-1977:71
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1981:10-1981:69
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1988:10-1988:73
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1989:10-1989:73
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2012:10-2012:76
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2013:10-2013:76
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2021:10-2021:76
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2031:10-2031:72
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:257:10-260:40
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:263:10-263:47
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:276:18-276:55
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:895:10-895:54
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:903:10-903:56
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:938:10-938:56
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:975:10-975:79
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/optimizations.md:124:6-152:72
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/optimizations.md:156:6-184:72
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/optimizations.md:188:6-216:60
      1 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/optimizations.md:220:6-248:73
      2 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1045:10-1046:26
      2 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2022:10-2022:76
      2 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2023:10-2023:76
      2 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2041:10-2041:64
      2 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:874:10-875:35
      2 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:879:10-880:91
      3 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:2044:10-2044:68
      4 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1027:10-1027:36
      4 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1031:10-1034:29
      4 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1050:10-1050:56
      4 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1051:10-1051:56
      4 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1976:10-1976:71
      4 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1998:10-1998:73
      4 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:853:10-853:33
      5 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1812:10-1813:39
      5 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1818:10-1819:75
      5 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1821:10-1821:67
      6 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:428:10-428:108
      6 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/optimizations.md:91:6-120:98
      7 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/optimizations.md:58:6-87:70
      8 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:445:10-445:155
      9 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:732:10-732:82
     11 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:444:10-444:155
     16 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/optimizations.md:23:6-54:91
     20 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:520:10-521:55
     25 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1803:10-1807:13
     25 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1809:10-1810:38
     25 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:303:10-312:64
     25 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:484:10-485:62
     30 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:1823:10-1823:128
     58 /home/max/evm-semantics/.build/usr/lib/kevm/include/kframework/evm.md:277:18-281:47

[JKTKops]

Out of interest in bytes00 specifically, I decided to take a first shot at deduping using a log from that one. Under each rule is a list of all the steps at which it was applied along with the duration of that step. It appears that there is no one single step that took the whole runtime, rather several steps that are slow sometimes.

bytes00.deduped.txt

edit: based on Tom's feedback in the meeting today, I think the duration data here is mostly meaningless. However the frequency data would still be meaningful.

[ehildenb]

Putting this data through grep 'median' | sort -h -k4, it seems that POP rules (for the EVM opcode POP, that is), take a long time to apply. That seems really strange, given that POP is such a simple opcode.

We should look for this trend in the fixed data. POP isn't executed that frequently, but I think it's weird that it's so slow to execute those rules.

[JKTKops]

For reference, this is currently blocked on runtimeverification/haskell-backend#2682 which I'm working on.