Skip to content

Commit 13cfef5

Browse files
StevengreStevengre
authored
Optimize summary rules (#2732)
* optimize the summary rules - remove unneccessary summaries with `statusCode` changes, like `EVM_STACK_OVERFLOW` - remove unneccessary constraints for the preconditions - remove ensures clauses that might not be satified by the preconditions. * fix error spec file name * Refactor stack functions to use opcode parameter instead of opcode_id - Updated the `stack_added`, `stack_needed`, and `stack_delta` functions to accept `opcode` as a parameter instead of `opcode_id`, improving clarity and consistency in the codebase.
1 parent 09a9572 commit 13cfef5

24 files changed

+214
-871
lines changed

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/address-summary.k

Lines changed: 7 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -4,34 +4,6 @@ module ADDRESS-SUMMARY
44
imports public EVM
55

66
rule [ADDRESS-SUMMARY-0]: <kevm>
7-
<k>
8-
( #next [ ADDRESS ] => #halt )
9-
~> K_CELL:K
10-
</k>
11-
<ethereum>
12-
<evm>
13-
<statusCode>
14-
( STATUSCODE_CELL:StatusCode => EVMC_STACK_OVERFLOW )
15-
</statusCode>
16-
<callState>
17-
<wordStack>
18-
WS:WordStack
19-
</wordStack>
20-
<gas>
21-
GAS_CELL:Int
22-
</gas>
23-
...
24-
</callState>
25-
...
26-
</evm>
27-
...
28-
</ethereum>
29-
...
30-
</kevm>
31-
requires 1023 <Int #sizeWordStack ( WS:WordStack , 0 )
32-
[priority(20), label(ADDRESS-SUMMARY-0)]
33-
34-
rule [ADDRESS-SUMMARY-1]: <kevm>
357
<k>
368
( #next [ ADDRESS ] ~> .K => .K )
379
~> K_CELL:K
@@ -66,14 +38,12 @@ module ADDRESS-SUMMARY
6638
...
6739
</kevm>
6840
requires ( USEGAS_CELL:Bool
69-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
70-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
41+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
7142
andBool ( Gbase < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
72-
))))
73-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
74-
[priority(20), label(ADDRESS-SUMMARY-1)]
43+
)))
44+
[priority(20), label(ADDRESS-SUMMARY-0)]
7545

76-
rule [ADDRESS-SUMMARY-2]: <kevm>
46+
rule [ADDRESS-SUMMARY-1]: <kevm>
7747
<k>
7848
( #next [ ADDRESS ] ~> .K => .K )
7949
~> K_CELL:K
@@ -105,10 +75,8 @@ module ADDRESS-SUMMARY
10575
...
10676
</kevm>
10777
requires ( ( notBool USEGAS_CELL:Bool )
108-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
109-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
110-
)))
111-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
112-
[priority(20), label(ADDRESS-SUMMARY-2)]
78+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
79+
))
80+
[priority(20), label(ADDRESS-SUMMARY-1)]
11381

11482
endmodule

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/calldatasize-summary.k

Lines changed: 7 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -4,34 +4,6 @@ module CALLDATASIZE-SUMMARY
44
imports public EVM
55

66
rule [CALLDATASIZE-SUMMARY-0]: <kevm>
7-
<k>
8-
( #next [ CALLDATASIZE ] => #halt )
9-
~> K_CELL:K
10-
</k>
11-
<ethereum>
12-
<evm>
13-
<statusCode>
14-
( STATUSCODE_CELL:StatusCode => EVMC_STACK_OVERFLOW )
15-
</statusCode>
16-
<callState>
17-
<wordStack>
18-
WS:WordStack
19-
</wordStack>
20-
<gas>
21-
GAS_CELL:Int
22-
</gas>
23-
...
24-
</callState>
25-
...
26-
</evm>
27-
...
28-
</ethereum>
29-
...
30-
</kevm>
31-
requires 1023 <Int #sizeWordStack ( WS:WordStack , 0 )
32-
[priority(20), label(CALLDATASIZE-SUMMARY-0)]
33-
34-
rule [CALLDATASIZE-SUMMARY-1]: <kevm>
357
<k>
368
( #next [ CALLDATASIZE ] ~> .K => .K )
379
~> K_CELL:K
@@ -66,14 +38,12 @@ module CALLDATASIZE-SUMMARY
6638
...
6739
</kevm>
6840
requires ( USEGAS_CELL:Bool
69-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
70-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
41+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
7142
andBool ( Gbase < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
72-
))))
73-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
74-
[priority(20), label(CALLDATASIZE-SUMMARY-1)]
43+
)))
44+
[priority(20), label(CALLDATASIZE-SUMMARY-0)]
7545

76-
rule [CALLDATASIZE-SUMMARY-2]: <kevm>
46+
rule [CALLDATASIZE-SUMMARY-1]: <kevm>
7747
<k>
7848
( #next [ CALLDATASIZE ] ~> .K => .K )
7949
~> K_CELL:K
@@ -105,10 +75,8 @@ module CALLDATASIZE-SUMMARY
10575
...
10676
</kevm>
10777
requires ( ( notBool USEGAS_CELL:Bool )
108-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
109-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
110-
)))
111-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
112-
[priority(20), label(CALLDATASIZE-SUMMARY-2)]
78+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
79+
))
80+
[priority(20), label(CALLDATASIZE-SUMMARY-1)]
11381

11482
endmodule

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/caller-summary.k

Lines changed: 7 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -4,34 +4,6 @@ module CALLER-SUMMARY
44
imports public EVM
55

66
rule [CALLER-SUMMARY-0]: <kevm>
7-
<k>
8-
( #next [ CALLER ] => #halt )
9-
~> K_CELL:K
10-
</k>
11-
<ethereum>
12-
<evm>
13-
<statusCode>
14-
( STATUSCODE_CELL:StatusCode => EVMC_STACK_OVERFLOW )
15-
</statusCode>
16-
<callState>
17-
<wordStack>
18-
WS:WordStack
19-
</wordStack>
20-
<gas>
21-
GAS_CELL:Int
22-
</gas>
23-
...
24-
</callState>
25-
...
26-
</evm>
27-
...
28-
</ethereum>
29-
...
30-
</kevm>
31-
requires 1023 <Int #sizeWordStack ( WS:WordStack , 0 )
32-
[priority(20), label(CALLER-SUMMARY-0)]
33-
34-
rule [CALLER-SUMMARY-1]: <kevm>
357
<k>
368
( #next [ CALLER ] ~> .K => .K )
379
~> K_CELL:K
@@ -66,14 +38,12 @@ module CALLER-SUMMARY
6638
...
6739
</kevm>
6840
requires ( USEGAS_CELL:Bool
69-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
70-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
41+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
7142
andBool ( Gbase < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
72-
))))
73-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
74-
[priority(20), label(CALLER-SUMMARY-1)]
43+
)))
44+
[priority(20), label(CALLER-SUMMARY-0)]
7545

76-
rule [CALLER-SUMMARY-2]: <kevm>
46+
rule [CALLER-SUMMARY-1]: <kevm>
7747
<k>
7848
( #next [ CALLER ] ~> .K => .K )
7949
~> K_CELL:K
@@ -105,10 +75,8 @@ module CALLER-SUMMARY
10575
...
10676
</kevm>
10777
requires ( ( notBool USEGAS_CELL:Bool )
108-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
109-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
110-
)))
111-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
112-
[priority(20), label(CALLER-SUMMARY-2)]
78+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
79+
))
80+
[priority(20), label(CALLER-SUMMARY-1)]
11381

11482
endmodule

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/chainid-summary.k

Lines changed: 7 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -4,34 +4,6 @@ module CHAINID-SUMMARY
44
imports public EVM
55

66
rule [CHAINID-SUMMARY-0]: <kevm>
7-
<k>
8-
( #next [ CHAINID ] => #halt )
9-
~> K_CELL:K
10-
</k>
11-
<ethereum>
12-
<evm>
13-
<statusCode>
14-
( STATUSCODE_CELL:StatusCode => EVMC_STACK_OVERFLOW )
15-
</statusCode>
16-
<callState>
17-
<wordStack>
18-
WS:WordStack
19-
</wordStack>
20-
<gas>
21-
GAS_CELL:Int
22-
</gas>
23-
...
24-
</callState>
25-
...
26-
</evm>
27-
...
28-
</ethereum>
29-
...
30-
</kevm>
31-
requires 1023 <Int #sizeWordStack ( WS:WordStack , 0 )
32-
[priority(20), label(CHAINID-SUMMARY-0)]
33-
34-
rule [CHAINID-SUMMARY-1]: <kevm>
357
<k>
368
( #next [ CHAINID ] ~> .K => .K )
379
~> K_CELL:K
@@ -68,14 +40,12 @@ module CHAINID-SUMMARY
6840
...
6941
</kevm>
7042
requires ( USEGAS_CELL:Bool
71-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
72-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
43+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
7344
andBool ( Gbase < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
74-
))))
75-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
76-
[priority(20), label(CHAINID-SUMMARY-1)]
45+
)))
46+
[priority(20), label(CHAINID-SUMMARY-0)]
7747

78-
rule [CHAINID-SUMMARY-2]: <kevm>
48+
rule [CHAINID-SUMMARY-1]: <kevm>
7949
<k>
8050
( #next [ CHAINID ] ~> .K => .K )
8151
~> K_CELL:K
@@ -109,10 +79,8 @@ module CHAINID-SUMMARY
10979
...
11080
</kevm>
11181
requires ( ( notBool USEGAS_CELL:Bool )
112-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
113-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
114-
)))
115-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
116-
[priority(20), label(CHAINID-SUMMARY-2)]
82+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
83+
))
84+
[priority(20), label(CHAINID-SUMMARY-1)]
11785

11886
endmodule

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/codesize-summary.k

Lines changed: 7 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -4,34 +4,6 @@ module CODESIZE-SUMMARY
44
imports public EVM
55

66
rule [CODESIZE-SUMMARY-0]: <kevm>
7-
<k>
8-
( #next [ CODESIZE ] => #halt )
9-
~> K_CELL:K
10-
</k>
11-
<ethereum>
12-
<evm>
13-
<statusCode>
14-
( STATUSCODE_CELL:StatusCode => EVMC_STACK_OVERFLOW )
15-
</statusCode>
16-
<callState>
17-
<wordStack>
18-
WS:WordStack
19-
</wordStack>
20-
<gas>
21-
GAS_CELL:Int
22-
</gas>
23-
...
24-
</callState>
25-
...
26-
</evm>
27-
...
28-
</ethereum>
29-
...
30-
</kevm>
31-
requires 1023 <Int #sizeWordStack ( WS:WordStack , 0 )
32-
[priority(20), label(CODESIZE-SUMMARY-0)]
33-
34-
rule [CODESIZE-SUMMARY-1]: <kevm>
357
<k>
368
( #next [ CODESIZE ] ~> .K => .K )
379
~> K_CELL:K
@@ -66,14 +38,12 @@ module CODESIZE-SUMMARY
6638
...
6739
</kevm>
6840
requires ( USEGAS_CELL:Bool
69-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
70-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
41+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
7142
andBool ( Gbase < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
72-
))))
73-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
74-
[priority(20), label(CODESIZE-SUMMARY-1)]
43+
)))
44+
[priority(20), label(CODESIZE-SUMMARY-0)]
7545

76-
rule [CODESIZE-SUMMARY-2]: <kevm>
46+
rule [CODESIZE-SUMMARY-1]: <kevm>
7747
<k>
7848
( #next [ CODESIZE ] ~> .K => .K )
7949
~> K_CELL:K
@@ -105,10 +75,8 @@ module CODESIZE-SUMMARY
10575
...
10676
</kevm>
10777
requires ( ( notBool USEGAS_CELL:Bool )
108-
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
109-
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
110-
)))
111-
ensures #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
112-
[priority(20), label(CODESIZE-SUMMARY-2)]
78+
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
79+
))
80+
[priority(20), label(CODESIZE-SUMMARY-1)]
11381

11482
endmodule

0 commit comments

Comments
 (0)