Skip to content

Commit db7d25e

Browse files
StevengreStevengre
authored
Update opcode summaries to standardize labels and improve clarity (#2737)
* Update opcode summaries to standardize labels and improve clarity - Changed labels for various opcode summaries to follow a consistent naming convention, replacing instances of `-1` with `-NOGAS` or `-USEGAS` where applicable. - This update enhances readability and maintains uniformity across the summary definitions, ensuring better understanding and maintenance of the codebase.
1 parent b634af4 commit db7d25e

71 files changed

Lines changed: 372 additions & 298 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module ADD-SUMMARY
44
imports public EVM
55

6-
rule [ADD-SUMMARY-0]: <kevm>
6+
rule [ADD-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ ADD ] ~> .K => .K )
99
~> K_CELL:K
@@ -37,9 +37,9 @@ module ADD-SUMMARY
3737
requires ( USEGAS_CELL:Bool
3838
andBool ( Gverylow < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
3939
))
40-
[priority(20), label(ADD-SUMMARY-0)]
40+
[priority(20), label(ADD-SUMMARY-USEGAS)]
4141

42-
rule [ADD-SUMMARY-1]: <kevm>
42+
rule [ADD-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ ADD ] ~> .K => .K )
4545
~> K_CELL:K
@@ -68,6 +68,6 @@ module ADD-SUMMARY
6868
...
6969
</kevm>
7070
requires ( notBool USEGAS_CELL:Bool )
71-
[priority(20), label(ADD-SUMMARY-1)]
71+
[priority(20), label(ADD-SUMMARY-NOGAS)]
7272

7373
endmodule

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module ADDMOD-SUMMARY
44
imports public EVM
55

6-
rule [ADDMOD-SUMMARY-0]: <kevm>
6+
rule [ADDMOD-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ ADDMOD ] ~> .K => .K )
99
~> K_CELL:K
@@ -37,9 +37,9 @@ module ADDMOD-SUMMARY
3737
requires ( USEGAS_CELL:Bool
3838
andBool ( Gmid < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
3939
))
40-
[priority(20), label(ADDMOD-SUMMARY-0)]
40+
[priority(20), label(ADDMOD-SUMMARY-USEGAS)]
4141

42-
rule [ADDMOD-SUMMARY-1]: <kevm>
42+
rule [ADDMOD-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ ADDMOD ] ~> .K => .K )
4545
~> K_CELL:K
@@ -68,6 +68,6 @@ module ADDMOD-SUMMARY
6868
...
6969
</kevm>
7070
requires ( notBool USEGAS_CELL:Bool )
71-
[priority(20), label(ADDMOD-SUMMARY-1)]
71+
[priority(20), label(ADDMOD-SUMMARY-NOGAS)]
7272

7373
endmodule

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module ADDRESS-SUMMARY
44
imports public EVM
55

6-
rule [ADDRESS-SUMMARY-0]: <kevm>
6+
rule [ADDRESS-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ ADDRESS ] ~> .K => .K )
99
~> K_CELL:K
@@ -41,9 +41,9 @@ module ADDRESS-SUMMARY
4141
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
4242
andBool ( Gbase < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
4343
)))
44-
[priority(20), label(ADDRESS-SUMMARY-0)]
44+
[priority(20), label(ADDRESS-SUMMARY-USEGAS)]
4545

46-
rule [ADDRESS-SUMMARY-1]: <kevm>
46+
rule [ADDRESS-SUMMARY-NOGAS]: <kevm>
4747
<k>
4848
( #next [ ADDRESS ] ~> .K => .K )
4949
~> K_CELL:K
@@ -77,6 +77,6 @@ module ADDRESS-SUMMARY
7777
requires ( ( notBool USEGAS_CELL:Bool )
7878
andBool ( #sizeWordStack ( WS:WordStack , 0 ) <=Int 1023
7979
))
80-
[priority(20), label(ADDRESS-SUMMARY-1)]
80+
[priority(20), label(ADDRESS-SUMMARY-NOGAS)]
8181

8282
endmodule

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module AND-SUMMARY
44
imports public EVM
55

6-
rule [AND-SUMMARY-0]: <kevm>
6+
rule [AND-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ AND ] ~> .K => .K )
99
~> K_CELL:K
@@ -37,9 +37,9 @@ module AND-SUMMARY
3737
requires ( USEGAS_CELL:Bool
3838
andBool ( Gverylow < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
3939
))
40-
[priority(20), label(AND-SUMMARY-0)]
40+
[priority(20), label(AND-SUMMARY-USEGAS)]
4141

42-
rule [AND-SUMMARY-1]: <kevm>
42+
rule [AND-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ AND ] ~> .K => .K )
4545
~> K_CELL:K
@@ -68,6 +68,6 @@ module AND-SUMMARY
6868
...
6969
</kevm>
7070
requires ( notBool USEGAS_CELL:Bool )
71-
[priority(20), label(AND-SUMMARY-1)]
71+
[priority(20), label(AND-SUMMARY-NOGAS)]
7272

7373
endmodule

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module BALANCE-NORMAL-SUMMARY
44
imports public EVM
55

6-
rule [BALANCE-NORMAL-SUMMARY-0]: <kevm>
6+
rule [BALANCE-NORMAL-SUMMARY-NOGAS-BERLIN]: <kevm>
77
<k>
88
( #next [ BALANCE ] ~> .K => .K )
99
~> K_CELL:K
@@ -54,9 +54,9 @@ module BALANCE-NORMAL-SUMMARY
5454
requires ( ( notBool USEGAS_CELL:Bool )
5555
andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
5656
))
57-
[priority(20), label(BALANCE-NORMAL-SUMMARY-0)]
57+
[priority(20), label(BALANCE-NORMAL-SUMMARY-NOGAS-BERLIN)]
5858

59-
rule [BALANCE-NORMAL-SUMMARY-1]: <kevm>
59+
rule [BALANCE-NORMAL-SUMMARY-USEGAS-BERLIN]: <kevm>
6060
<k>
6161
( #next [ BALANCE ] ~> .K => .K )
6262
~> K_CELL:K
@@ -113,9 +113,9 @@ module BALANCE-NORMAL-SUMMARY
113113
andBool ( 0 <=Int GAS_CELL:Int
114114
andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
115115
)))))
116-
[priority(20), label(BALANCE-NORMAL-SUMMARY-1)]
116+
[priority(20), label(BALANCE-NORMAL-SUMMARY-USEGAS-BERLIN)]
117117

118-
rule [BALANCE-NORMAL-SUMMARY-2]: <kevm>
118+
rule [BALANCE-NORMAL-SUMMARY-USEGAS]: <kevm>
119119
<k>
120120
( #next [ BALANCE ] ~> .K => .K )
121121
~> K_CELL:K
@@ -171,6 +171,6 @@ module BALANCE-NORMAL-SUMMARY
171171
andBool ( Gbalance < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
172172
andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
173173
))))
174-
[priority(20), label(BALANCE-NORMAL-SUMMARY-2)]
174+
[priority(20), label(BALANCE-NORMAL-SUMMARY-USEGAS)]
175175

176176
endmodule

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module BALANCE-OWISE-SUMMARY
44
imports public EVM
55

6-
rule [BALANCE-OWISE-SUMMARY-0]: <kevm>
6+
rule [BALANCE-OWISE-SUMMARY-NOGAS-BERLIN]: <kevm>
77
<k>
88
( #next [ BALANCE ] ~> .K => .K )
99
~> K_CELL:K
@@ -54,9 +54,9 @@ module BALANCE-OWISE-SUMMARY
5454
requires ( ( notBool USEGAS_CELL:Bool )
5555
andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
5656
))
57-
[priority(20), label(BALANCE-OWISE-SUMMARY-0)]
57+
[priority(20), label(BALANCE-OWISE-SUMMARY-NOGAS-BERLIN)]
5858

59-
rule [BALANCE-OWISE-SUMMARY-1]: <kevm>
59+
rule [BALANCE-OWISE-SUMMARY-USEGAS-BERLIN]: <kevm>
6060
<k>
6161
( #next [ BALANCE ] ~> .K => .K )
6262
~> K_CELL:K
@@ -113,9 +113,9 @@ module BALANCE-OWISE-SUMMARY
113113
andBool ( 0 <=Int GAS_CELL:Int
114114
andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
115115
)))))
116-
[priority(20), label(BALANCE-OWISE-SUMMARY-1)]
116+
[priority(20), label(BALANCE-OWISE-SUMMARY-USEGAS-BERLIN)]
117117

118-
rule [BALANCE-OWISE-SUMMARY-2]: <kevm>
118+
rule [BALANCE-OWISE-SUMMARY-USEGAS]: <kevm>
119119
<k>
120120
( #next [ BALANCE ] ~> .K => .K )
121121
~> K_CELL:K
@@ -171,6 +171,6 @@ module BALANCE-OWISE-SUMMARY
171171
andBool ( Gbalance < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
172172
andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
173173
))))
174-
[priority(20), label(BALANCE-OWISE-SUMMARY-2)]
174+
[priority(20), label(BALANCE-OWISE-SUMMARY-USEGAS)]
175175

176176
endmodule

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module BLOCKHASH-SUMMARY
44
imports public EVM
55

6-
rule [BLOCKHASH-SUMMARY-0]: <kevm>
6+
rule [BLOCKHASH-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ BLOCKHASH ] ~> .K => .K )
99
~> K_CELL:K
@@ -46,9 +46,9 @@ module BLOCKHASH-SUMMARY
4646
requires ( USEGAS_CELL:Bool
4747
andBool ( Gblockhash < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
4848
))
49-
[priority(20), label(BLOCKHASH-SUMMARY-0)]
49+
[priority(20), label(BLOCKHASH-SUMMARY-USEGAS)]
5050

51-
rule [BLOCKHASH-SUMMARY-1]: <kevm>
51+
rule [BLOCKHASH-SUMMARY-NOGAS]: <kevm>
5252
<k>
5353
( #next [ BLOCKHASH ] ~> .K => .K )
5454
~> K_CELL:K
@@ -86,6 +86,6 @@ module BLOCKHASH-SUMMARY
8686
...
8787
</kevm>
8888
requires ( notBool USEGAS_CELL:Bool )
89-
[priority(20), label(BLOCKHASH-SUMMARY-1)]
89+
[priority(20), label(BLOCKHASH-SUMMARY-NOGAS)]
9090

9191
endmodule

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module BYTE-SUMMARY
44
imports public EVM
55

6-
rule [BYTE-SUMMARY-0]: <kevm>
6+
rule [BYTE-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ BYTE ] ~> .K => .K )
99
~> K_CELL:K
@@ -37,9 +37,9 @@ module BYTE-SUMMARY
3737
requires ( USEGAS_CELL:Bool
3838
andBool ( Gverylow < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
3939
))
40-
[priority(20), label(BYTE-SUMMARY-0)]
40+
[priority(20), label(BYTE-SUMMARY-USEGAS)]
4141

42-
rule [BYTE-SUMMARY-1]: <kevm>
42+
rule [BYTE-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ BYTE ] ~> .K => .K )
4545
~> K_CELL:K
@@ -68,6 +68,6 @@ module BYTE-SUMMARY
6868
...
6969
</kevm>
7070
requires ( notBool USEGAS_CELL:Bool )
71-
[priority(20), label(BYTE-SUMMARY-1)]
71+
[priority(20), label(BYTE-SUMMARY-NOGAS)]
7272

7373
endmodule

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module CALLDATACOPY-SUMMARY
44
imports public EVM
55

6-
rule [CALLDATACOPY-SUMMARY-0]: <kevm>
6+
rule [CALLDATACOPY-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ CALLDATACOPY ] ~> .K => .K )
99
~> K_CELL:K
@@ -47,9 +47,9 @@ module CALLDATACOPY-SUMMARY
4747
andBool ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL:Int
4848
andBool ( ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) <=Int ( GAS_CELL:Int -Int ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) )
4949
)))
50-
[priority(20), label(CALLDATACOPY-SUMMARY-0)]
50+
[priority(20), label(CALLDATACOPY-SUMMARY-USEGAS)]
5151

52-
rule [CALLDATACOPY-SUMMARY-1]: <kevm>
52+
rule [CALLDATACOPY-SUMMARY-NOGAS]: <kevm>
5353
<k>
5454
( #next [ CALLDATACOPY ] ~> .K => .K )
5555
~> K_CELL:K
@@ -84,6 +84,6 @@ module CALLDATACOPY-SUMMARY
8484
...
8585
</kevm>
8686
requires ( notBool USEGAS_CELL:Bool )
87-
[priority(20), label(CALLDATACOPY-SUMMARY-1)]
87+
[priority(20), label(CALLDATACOPY-SUMMARY-NOGAS)]
8888

8989
endmodule

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ requires "../evm.md"
33
module CALLDATALOAD-SUMMARY
44
imports public EVM
55

6-
rule [CALLDATALOAD-SUMMARY-0]: <kevm>
6+
rule [CALLDATALOAD-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ CALLDATALOAD ] ~> .K => .K )
99
~> K_CELL:K
@@ -40,9 +40,9 @@ module CALLDATALOAD-SUMMARY
4040
requires ( USEGAS_CELL:Bool
4141
andBool ( Gverylow < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
4242
))
43-
[priority(20), label(CALLDATALOAD-SUMMARY-0)]
43+
[priority(20), label(CALLDATALOAD-SUMMARY-USEGAS)]
4444

45-
rule [CALLDATALOAD-SUMMARY-1]: <kevm>
45+
rule [CALLDATALOAD-SUMMARY-NOGAS]: <kevm>
4646
<k>
4747
( #next [ CALLDATALOAD ] ~> .K => .K )
4848
~> K_CELL:K
@@ -74,6 +74,6 @@ module CALLDATALOAD-SUMMARY
7474
...
7575
</kevm>
7676
requires ( notBool USEGAS_CELL:Bool )
77-
[priority(20), label(CALLDATALOAD-SUMMARY-1)]
77+
[priority(20), label(CALLDATALOAD-SUMMARY-NOGAS)]
7878

7979
endmodule

0 commit comments

Comments
 (0)