WordStack optimizations #2632

PetarMax · 2024-09-26T12:40:38Z

This PR introduces some optimizations that should allows us to manipulate word stacks more efficiently..

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k

optimizer/optimizations.md

…te rule matching

ehildenb · 2024-09-27T13:52:42Z

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

         <localMem> LM </localMem>
         <log> L => L ListItem({ ACCT | WordStack2List(#take(N, WS)) | #range(LM, MEMSTART, MEMWIDTH) }) </log>
      requires #sizeWordStack(WS) >=Int N
+      [preserves-definedness]
 ```


Why does this rule fail the preserves-definedness check in the first place?

Ah, it shouldn't anymore, there was an interim moment when it did. I'll remove that.

ehildenb · 2024-09-27T13:54:10Z

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md

+    syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)]
+ // ------------------------------------------------------------------------------------------------------------
+    rule [ws-size-00]: #sizeWordStack (.WordStack) => 0
+    rule [ws-size-01]: #sizeWordStack (_ : .WordStack) => 1
+    rule [ws-size-02]: #sizeWordStack (_ : _ : .WordStack) => 2
+    rule [ws-size-03]: #sizeWordStack (_ : _ : _ : .WordStack) => 3
+    rule [ws-size-04]: #sizeWordStack (_ : _ : _ : _ : .WordStack) => 4
+    rule [ws-size-05]: #sizeWordStack (_ : _ : _ : _ : _ : .WordStack) => 5
+    rule [ws-size-06]: #sizeWordStack (_ : _ : _ : _ : _ : _ : .WordStack) => 6
+    rule [ws-size-07]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : .WordStack) => 7
+    rule [ws-size-08]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 8
+    rule [ws-size-09]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 9
+    rule [ws-size-10]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 10
+    rule [ws-size-11]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 11
+    rule [ws-size-12]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 12
+    rule [ws-size-13]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 13
+    rule [ws-size-14]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 14
+    rule [ws-size-15]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 15
+    rule [ws-size-16]: #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : .WordStack) => 16
+    rule [ws-size-N]:  #sizeWordStack (_ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : _ : WS) => 16 +Int #sizeWordStack(WS)
+    rule [ws-size-O]:  #sizeWordStack (_ : WS) => 1 +Int #sizeWordStack(WS) [priority(75)]


I think the reason for how it was structured before was to keep the computation tail-recursive, which the LLVM backend requires for efficient memory/time usage. Can we check the LLVM backend performance on teh conformance test-suite here?

I don't like this, I've reverted back to just the simple tail recursion.

@ehildenb Do you remember why there was an auxiliary function here with two parameters instead of a direct computation?

evm-semantics/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md

Lines 398 to 401 in 3d7c9c2

syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)]

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

rule [ws-size-base]: #sizeWordStack (.WordStack) => 0

rule [ws-size-ind]: #sizeWordStack (_ : WS) => 1 +Int #sizeWordStack(WS)

This isn't tail recursive. It's doing an add operation after the call. That's why there was an auxiliary function with the extra parameter.

Ah yes yes, sorry, hm.

I will bring it back. It's not the thing that's breaking the proofs anyways and works well.

If we wanted to speed this calculation up, we can merge something like this.

ehildenb · 2024-09-27T13:55:31Z

optimizer/optimizations.md

+    claim
+    [optimized.add]:
+      <kevm>
+        <k>
+          ( #next[ ADD ] => .K ) ...
+        </k>
+        <schedule>
+          SCHED
+        </schedule>
+        <useGas>
+          USEGAS
+        </useGas>
+        <ethereum>
+          <evm>
+            <callState>
+              <wordStack>
+                ( W0 : W1 : WS => chop( ( W0 +Int W1 ) ) : WS )


Why is this added here?

We already have a test-harness that takes the rules in this file and discharges them as claims directly.

Oh, actually, this entire directory isn't used at all anymore. We really should delete it, but I left it for illustrative purposes. Any reason to add this?

Ah, that's a leftover of me trying to test a failing optimisation, will remove.

ehildenb · 2024-09-27T13:56:38Z

tests/failing-symbolic.haskell-booster-dev

+tests/specs/mcd/dai-adduu-fail-rough-spec.k
+tests/specs/mcd/flipper-addu48u48-fail-rough-spec.k
+tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k
+tests/specs/mcd-structured/flipper-addu48u48-fail-rough-spec.k


Well that's less than ideal I guess.....

It is, but the booster will adapt and be more expressive, as per this issue.

This might allow us to prove further tests using just booster-dev.

ehildenb · 2024-09-27T13:57:09Z

We really need some performance metrics posted here, both for Haskell and LLVM backend.

PetarMax · 2024-09-27T14:30:30Z

What would be the best way to get the metrics? For the LLVM backend, I guess the conformance test suite.

geo2a · 2024-09-28T08:07:58Z

@PetarMax regarding the performance metrics for the Haskell backend: please ask @anvacaru, I remember that he has adapted our Nix-based performance measurement script to vary the version of KEVM instead of HB. This thould get tou a table comparing KEVM master vs branch, while keeping the K and HB versions fixed.

PetarMax · 2024-09-28T08:32:00Z

Just to say regarding concrete execution and the LLVM backend - the moment that we have anything symbolic in the word stack, we cannot use the LLVM backend to compute anything over it, even if it doesn't depend on the symbolicness (say, length), and so any tail recursion optiimisations will only work for purely concrete word stacks.

anvacaru · 2024-09-28T09:32:15Z

Yes, I put something together from the Haskell Backend's test-performance-kevm.sh script.

I would run this profile-kevm script for both branches I'm interested in.

export KEVM_VERSION=master; profile-kevm
export KEVM_VERSION=wordstack-optimizations; profile-kevm

then I would use the compare_logs.py logfile_1 logfile_2 to generate the table with the time values.

I will give it a go in the background and post the results here.

anvacaru · 2024-09-28T12:46:23Z

It seems like these optimizations are causing a slowdown. @PetarMax can you confirm this?

Test	master-1bd8e09de time	wordstack-optimizations-3801e920c time	(master-1bd8e09de/wordstack-optimizations-3801e920c) time
examples/sum-to-n-spec.k	91.79	103.43	0.8874601179541719
mcd/end-subuu-pass-spec.k	55.36	60.03	0.9222055638847243
mcd-structured/end-subuu-pass-spec.k	55.54	59.61	0.9317228652910585
erc20/ds/transferFrom-failure-1-b-spec.k	122.0	130.18	0.937163926870487
mcd-structured/dai-adduu-fail-rough-spec.k	48.6	51.55	0.9427740058195927
kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k	63.9	67.69	0.9440094548677795
erc20/ds/transferFrom-failure-1-c-spec.k	99.87	105.54	0.9462762933484935
mcd/dai-adduu-fail-rough-spec.k	48.6	51.33	0.9468147282291058
benchmarks/functional-spec.k	357.99	376.78	0.9501300493656777
erc20/ds/transferFrom-failure-2-c-spec.k	47.24	49.7	0.9505030181086519
mcd-structured/flipper-addu48u48-fail-rough-spec.k	48.03	50.49	0.9512774806892453
kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k	47.64	50.05	0.951848151848152
mcd/flipper-addu48u48-fail-rough-spec.k	47.99	50.36	0.9529388403494837
erc20/ds/balanceOf-spec.k	46.33	48.55	0.9542739443872297
mcd-structured/functional-spec.k	324.39	339.38	0.9558312216394602
benchmarks/storagevar00-spec.k	42.9	44.76	0.9584450402144772
kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k	67.85	70.71	0.9595531042285391
benchmarks/overflow00-overflow-spec.k	43.72	45.55	0.9598243688254665
mcd-structured/cat-exhaustiveness-spec.k	104.35	108.7	0.9599816007359705
benchmarks/ecrecover00-sigvalid-spec.k	53.29	55.48	0.9605263157894737
mcd-structured/flopper-tick-pass-rough-spec.k	83.28	86.64	0.961218836565097
kontrol/test-countertest-testincrement-0-spec.k	85.3	88.7	0.9616685456595264
examples/solidity-code-spec.md	105.59	109.78	0.9618327564219348
kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k	63.52	66.04	0.9618413082980012
kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k	46.77	48.54	0.9635352286773795
benchmarks/requires01-a0le0-spec.k	43.32	44.95	0.9637374860956618
mcd/functional-spec.k	548.15	568.02	0.9650188373648815
mcd-structured/flopper-file-pass-rough-spec.k	17.9	17.28	1.0358796296296295
mcd/flopper-dent-guy-same-pass-rough-spec.k	641.56	610.61	1.0506870179001326
TOTAL	3452.77	3560.43	0.9697620792994105

PetarMax and others added 4 commits September 26, 2024 13:38

initial commit

f846164

Merge branch 'master' into wordstack-optimizations

7c9a7eb

corrections

3c3fa50

adding SMT lemmas

ceacb63

PetarMax self-assigned this Sep 26, 2024

PetarMax added the enhancement New feature or request label Sep 26, 2024

PetarMax added 4 commits September 26, 2024 16:29

more smt lemmas

a3a1a56

correction

5e89634

correction

1269317

formatting correction

7205c9b

PetarMax force-pushed the wordstack-optimizations branch 2 times, most recently from 6466343 to 7205c9b Compare September 26, 2024 20:47

PetarMax added 2 commits September 26, 2024 23:05

further lemmas

5e1f946

third lemma

e2fb909

gtrepta reviewed Sep 27, 2024

View reviewed changes

PetarMax added 8 commits September 27, 2024 07:31

corrections

b4dc91f

sizeWordStack

b554704

no owise

05cab84

rule enumeration

bccdb04

minor corrections

aaec015

documentation correction

ff6adbe

adding tests to booster-dev ignore until booster improves indetermina…

c0c088b

…te rule matching

correction

5acb050

PetarMax marked this pull request as ready for review September 27, 2024 13:41

ehildenb reviewed Sep 27, 2024

View reviewed changes

corrections

7899ab3

PetarMax added 2 commits September 27, 2024 15:32

tail-recursive sizeWordStack

3d7c9c2

reverting the computation of sizeWordStack

3801e92

PetarMax added 2 commits September 29, 2024 10:08

removing direct computations

f0bfa6e

bringing back booster tests

550111f

PetarMax closed this Oct 15, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

WordStack optimizations #2632

WordStack optimizations #2632

PetarMax commented Sep 26, 2024

ehildenb Sep 27, 2024

PetarMax Sep 27, 2024

PetarMax Sep 27, 2024

ehildenb Sep 27, 2024

PetarMax Sep 27, 2024

gtrepta Sep 27, 2024

PetarMax Sep 27, 2024 •

edited

Loading

PetarMax Sep 27, 2024

ehildenb Sep 27, 2024

ehildenb Sep 27, 2024

PetarMax Sep 27, 2024

PetarMax Sep 27, 2024

ehildenb Sep 27, 2024

PetarMax Sep 27, 2024

PetarMax Sep 27, 2024

ehildenb commented Sep 27, 2024

PetarMax commented Sep 27, 2024

geo2a commented Sep 28, 2024

PetarMax commented Sep 28, 2024

anvacaru commented Sep 28, 2024

anvacaru commented Sep 28, 2024

	syntax Int ::= #sizeWordStack ( WordStack ) [symbol(#sizeWordStack), function, total, smtlib(sizeWordStack)]
	// ------------------------------------------------------------------------------------------------------------
	rule [ws-size-base]: #sizeWordStack (.WordStack) => 0
	rule [ws-size-ind]: #sizeWordStack (_ : WS) => 1 +Int #sizeWordStack(WS)

WordStack optimizations #2632

WordStack optimizations #2632

Conversation

PetarMax commented Sep 26, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

PetarMax Sep 27, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ehildenb commented Sep 27, 2024

PetarMax commented Sep 27, 2024

geo2a commented Sep 28, 2024

PetarMax commented Sep 28, 2024

anvacaru commented Sep 28, 2024

anvacaru commented Sep 28, 2024

PetarMax Sep 27, 2024 •

edited

Loading