Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WordStack optimizations #2632

Closed
wants to merge 23 commits into from
Closed

WordStack optimizations #2632

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
f846164
initial commit
PetarMax Sep 26, 2024
7c9a7eb
Merge branch 'master' into wordstack-optimizations
PetarMax Sep 26, 2024
3c3fa50
corrections
PetarMax Sep 26, 2024
ceacb63
adding SMT lemmas
PetarMax Sep 26, 2024
a3a1a56
more smt lemmas
PetarMax Sep 26, 2024
5e89634
correction
PetarMax Sep 26, 2024
1269317
correction
PetarMax Sep 26, 2024
7205c9b
formatting correction
PetarMax Sep 26, 2024
5e1f946
further lemmas
PetarMax Sep 26, 2024
e2fb909
third lemma
PetarMax Sep 26, 2024
b4dc91f
corrections
PetarMax Sep 27, 2024
b554704
sizeWordStack
PetarMax Sep 27, 2024
05cab84
no owise
PetarMax Sep 27, 2024
bccdb04
rule enumeration
PetarMax Sep 27, 2024
aaec015
minor corrections
PetarMax Sep 27, 2024
ff6adbe
documentation correction
PetarMax Sep 27, 2024
c0c088b
adding tests to booster-dev ignore until booster improves indetermina…
PetarMax Sep 27, 2024
5acb050
correction
PetarMax Sep 27, 2024
7899ab3
corrections
PetarMax Sep 27, 2024
3d7c9c2
tail-recursive sizeWordStack
PetarMax Sep 27, 2024
3801e92
reverting the computation of sizeWordStack
PetarMax Sep 27, 2024
f0bfa6e
removing direct computations
PetarMax Sep 29, 2024
550111f
bringing back booster tests
PetarMax Sep 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
194 changes: 154 additions & 40 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
View file
Open in desktop

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1171,6 +1171,7 @@ These operators query about the current return data buffer.
<localMem> LM </localMem>
<log> L => L ListItem({ ACCT | WordStack2List(#take(N, WS)) | #range(LM, MEMSTART, MEMWIDTH) }) </log>
requires #sizeWordStack(WS) >=Int N
[preserves-definedness]
```
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed.


Ethereum Network OpCodes
Expand Down
4 changes: 3 additions & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,9 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
// Word Reasoning
// ########################

rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]
rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I <Int #sizeWordStack(WS) [simplification]
gtrepta marked this conversation as resolved.
Show resolved Hide resolved
rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma]
rule #sizeWordStack(_) <Int N => false requires N <=Int 0 [simplification, smt-lemma]

// #newAddr range
rule 0 <=Int #newAddr(_,_) => true [simplification]
Expand Down
5 changes: 4 additions & 1 deletion kevm-pyk/src/tests/integration/test_prove.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -425,7 +425,10 @@ def _get_optimization_proofs() -> list[APRProof]:
kore_rpc_command = ('booster-dev',) if use_booster_dev else ('kore-rpc-booster',)

with legacy_explore(
kevm, kcfg_semantics=KEVMSemantics(allow_symbolic_program=True), kore_rpc_command=kore_rpc_command
kevm,
kcfg_semantics=KEVMSemantics(allow_symbolic_program=True),
kore_rpc_command=kore_rpc_command,
smt_timeout=1000,
) as kcfg_explore:
prover = APRProver(
kcfg_explore,
Expand Down
43 changes: 37 additions & 6 deletions optimizer/optimizations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,9 @@ requires "lemmas/int-simplification.k"
module EVM-OPTIMIZATIONS-LEMMAS [symbolic]
imports EVM

rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification]
rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I <Int #sizeWordStack(WS) [simplification]
rule 0 <=Int #sizeWordStack(_ , 0) => true [simplification]
rule #sizeWordStack(_ , 0) <Int N => false requires N <=Int 0 [simplification]
rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS, N) requires I <Int #sizeWordStack(WS) [simplification]
gtrepta marked this conversation as resolved.
Show resolved Hide resolved
rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma]
rule #sizeWordStack(_) <Int N => false requires N <=Int 0 [simplification, smt-lemma]

endmodule

Expand All @@ -23,8 +22,40 @@ module EVM-OPTIMIZATIONS
imports INT-SIMPLIFICATION


// {OPTIMIZATIONS}

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 )
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this added here?

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed.

</wordStack>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
</gas>
...
</callState>
...
</evm>
...
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )

endmodule
```
11 changes: 0 additions & 11 deletions tests/specs/benchmarks/verification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,17 +62,6 @@ module VERIFICATION

rule 0 <=Int #memoryUsageUpdate(_MU, _START, _WIDTH) => true [simplification]

// ########################
// Buffer Reasoning
// ########################

rule #sizeWordStack(WS, N) <Int SIZE => #sizeWordStack(WS, 0) +Int N <Int SIZE requires N =/=Int 0 [simplification]

rule SIZELIMIT <Int #sizeWordStack(WS, N) +Int DELTA => SIZELIMIT <Int (#sizeWordStack(WS, 0) +Int N) +Int DELTA requires N =/=Int 0 [simplification]
rule SIZELIMIT <Int #sizeWordStack(WS, N) => SIZELIMIT <Int #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification]

rule #sizeWordStack(WS, N) <=Int SIZE => #sizeWordStack(WS, 0) +Int N <=Int SIZE requires N =/=Int 0 [simplification]

// ########################
// Range
// ########################
Expand Down
6 changes: 0 additions & 6 deletions tests/specs/examples/sum-to-n-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,16 +5,10 @@ module VERIFICATION
imports EVM-ASSEMBLY
imports LEMMAS

rule #sizeWordStack ( WS , N:Int )
=> N +Int #sizeWordStack ( WS , 0 )
requires N =/=K 0 [simplification]

rule bool2Word(A) ==K 0 => notBool(A) [simplification]

rule chop(I) => I requires #rangeUInt(256, I) [simplification]

rule 0 <=Int #sizeWordStack ( _ , _ ) => true [simplification, smt-lemma]

syntax Bytes ::= "sumToN" [macro]
// -------------------------------------
rule sumToN
Expand Down
2 changes: 0 additions & 2 deletions tests/specs/mcd-structured/verification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,8 +142,6 @@ module LEMMAS-MCD [symbolic]
// Word Reasoning
// ########################

rule #sizeWordStack(WS, N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification]

// ### vat-addui-fail-rough
//
// Proof:
Expand Down
2 changes: 0 additions & 2 deletions tests/specs/mcd/verification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,8 +147,6 @@ module LEMMAS-MCD [symbolic]
// Word Reasoning
// ########################

rule #sizeWordStack(WS, N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification]

// ### vat-addui-fail-rough
//
// Proof:
Expand Down
8 changes: 4 additions & 4 deletions tests/specs/opcodes/verification.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ module VERIFICATION
imports EVM
imports INT-SIMPLIFICATION

rule #sizeWordStack(WS , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0 [simplification]
rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N) requires I <Int #sizeWordStack(WS) [simplification]
rule 0 <=Int #sizeWordStack(_ , 0) => true [simplification]
rule #sizeWordStack(_ , 0) <Int N => false requires N <=Int 0 [simplification]
rule #sizeWordStack(WS [ I := _ ]) => #sizeWordStack(WS) requires I <Int #sizeWordStack(WS) [simplification]
rule 0 <=Int #sizeWordStack(_) => true [simplification, smt-lemma]
rule #sizeWordStack(_) <Int N => false requires N <=Int 0 [simplification, smt-lemma]

endmodule
Loading