Skip to content

Commit 1d02e19

Browse files
StevengreStevengre
authored
Use _XXX for unused variables for summary rules. (#2744)
1 parent b3de342 commit 1d02e19

Some content is hidden

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

71 files changed

+257
-257
lines changed

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module ADD-SUMMARY
66
rule [ADD-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ ADD ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -42,7 +42,7 @@ module ADD-SUMMARY
4242
rule [ADD-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ ADD ] ~> .K => .K )
45-
~> K_CELL:K
45+
~> _K_CELL:K
4646
</k>
4747
<useGas>
4848
( USEGAS_CELL:Bool => false )
@@ -57,7 +57,7 @@ module ADD-SUMMARY
5757
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
5858
</pc>
5959
<gas>
60-
GAS_CELL:Int
60+
_GAS_CELL:Int
6161
</gas>
6262
...
6363
</callState>

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module ADDMOD-SUMMARY
66
rule [ADDMOD-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ ADDMOD ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -42,7 +42,7 @@ module ADDMOD-SUMMARY
4242
rule [ADDMOD-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ ADDMOD ] ~> .K => .K )
45-
~> K_CELL:K
45+
~> _K_CELL:K
4646
</k>
4747
<useGas>
4848
( USEGAS_CELL:Bool => false )
@@ -57,7 +57,7 @@ module ADDMOD-SUMMARY
5757
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
5858
</pc>
5959
<gas>
60-
GAS_CELL:Int
60+
_GAS_CELL:Int
6161
</gas>
6262
...
6363
</callState>

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module ADDRESS-SUMMARY
66
rule [ADDRESS-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ ADDRESS ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -46,7 +46,7 @@ module ADDRESS-SUMMARY
4646
rule [ADDRESS-SUMMARY-NOGAS]: <kevm>
4747
<k>
4848
( #next [ ADDRESS ] ~> .K => .K )
49-
~> K_CELL:K
49+
~> _K_CELL:K
5050
</k>
5151
<useGas>
5252
( USEGAS_CELL:Bool => false )
@@ -64,7 +64,7 @@ module ADDRESS-SUMMARY
6464
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
6565
</pc>
6666
<gas>
67-
GAS_CELL:Int
67+
_GAS_CELL:Int
6868
</gas>
6969
...
7070
</callState>

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module AND-SUMMARY
66
rule [AND-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ AND ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -42,7 +42,7 @@ module AND-SUMMARY
4242
rule [AND-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ AND ] ~> .K => .K )
45-
~> K_CELL:K
45+
~> _K_CELL:K
4646
</k>
4747
<useGas>
4848
( USEGAS_CELL:Bool => false )
@@ -57,7 +57,7 @@ module AND-SUMMARY
5757
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
5858
</pc>
5959
<gas>
60-
GAS_CELL:Int
60+
_GAS_CELL:Int
6161
</gas>
6262
...
6363
</callState>

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module BALANCE-NORMAL-SUMMARY
66
rule [BALANCE-NORMAL-SUMMARY-NOGAS-BERLIN]: <kevm>
77
<k>
88
( #next [ BALANCE ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<useGas>
1212
( USEGAS_CELL:Bool => false )
@@ -15,13 +15,13 @@ module BALANCE-NORMAL-SUMMARY
1515
<evm>
1616
<callState>
1717
<wordStack>
18-
( ( W0:Int => BALANCE_CELL:Int ) : WS:WordStack )
18+
( ( W0:Int => BALANCE_CELL:Int ) : _WS:WordStack )
1919
</wordStack>
2020
<pc>
2121
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
2222
</pc>
2323
<gas>
24-
GAS_CELL:Int
24+
_GAS_CELL:Int
2525
</gas>
2626
...
2727
</callState>
@@ -59,7 +59,7 @@ module BALANCE-NORMAL-SUMMARY
5959
rule [BALANCE-NORMAL-SUMMARY-USEGAS-BERLIN]: <kevm>
6060
<k>
6161
( #next [ BALANCE ] ~> .K => .K )
62-
~> K_CELL:K
62+
~> _K_CELL:K
6363
</k>
6464
<schedule>
6565
SCHEDULE_CELL:Schedule
@@ -71,7 +71,7 @@ module BALANCE-NORMAL-SUMMARY
7171
<evm>
7272
<callState>
7373
<wordStack>
74-
( ( W0:Int => BALANCE_CELL:Int ) : WS:WordStack )
74+
( ( W0:Int => BALANCE_CELL:Int ) : _WS:WordStack )
7575
</wordStack>
7676
<pc>
7777
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
@@ -118,7 +118,7 @@ module BALANCE-NORMAL-SUMMARY
118118
rule [BALANCE-NORMAL-SUMMARY-USEGAS]: <kevm>
119119
<k>
120120
( #next [ BALANCE ] ~> .K => .K )
121-
~> K_CELL:K
121+
~> _K_CELL:K
122122
</k>
123123
<schedule>
124124
SCHEDULE_CELL:Schedule
@@ -130,7 +130,7 @@ module BALANCE-NORMAL-SUMMARY
130130
<evm>
131131
<callState>
132132
<wordStack>
133-
( ( W0:Int => BALANCE_CELL:Int ) : WS:WordStack )
133+
( ( W0:Int => BALANCE_CELL:Int ) : _WS:WordStack )
134134
</wordStack>
135135
<pc>
136136
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module BALANCE-OWISE-SUMMARY
66
rule [BALANCE-OWISE-SUMMARY-NOGAS-BERLIN]: <kevm>
77
<k>
88
( #next [ BALANCE ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<useGas>
1212
( USEGAS_CELL:Bool => false )
@@ -15,13 +15,13 @@ module BALANCE-OWISE-SUMMARY
1515
<evm>
1616
<callState>
1717
<wordStack>
18-
( ( W0:Int => BALANCE_CELL:Int ) : WS:WordStack )
18+
( ( W0:Int => BALANCE_CELL:Int ) : _WS:WordStack )
1919
</wordStack>
2020
<pc>
2121
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
2222
</pc>
2323
<gas>
24-
GAS_CELL:Int
24+
_GAS_CELL:Int
2525
</gas>
2626
...
2727
</callState>
@@ -59,7 +59,7 @@ module BALANCE-OWISE-SUMMARY
5959
rule [BALANCE-OWISE-SUMMARY-USEGAS-BERLIN]: <kevm>
6060
<k>
6161
( #next [ BALANCE ] ~> .K => .K )
62-
~> K_CELL:K
62+
~> _K_CELL:K
6363
</k>
6464
<schedule>
6565
SCHEDULE_CELL:Schedule
@@ -71,7 +71,7 @@ module BALANCE-OWISE-SUMMARY
7171
<evm>
7272
<callState>
7373
<wordStack>
74-
( ( W0:Int => BALANCE_CELL:Int ) : WS:WordStack )
74+
( ( W0:Int => BALANCE_CELL:Int ) : _WS:WordStack )
7575
</wordStack>
7676
<pc>
7777
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
@@ -118,7 +118,7 @@ module BALANCE-OWISE-SUMMARY
118118
rule [BALANCE-OWISE-SUMMARY-USEGAS]: <kevm>
119119
<k>
120120
( #next [ BALANCE ] ~> .K => .K )
121-
~> K_CELL:K
121+
~> _K_CELL:K
122122
</k>
123123
<schedule>
124124
SCHEDULE_CELL:Schedule
@@ -130,7 +130,7 @@ module BALANCE-OWISE-SUMMARY
130130
<evm>
131131
<callState>
132132
<wordStack>
133-
( ( W0:Int => BALANCE_CELL:Int ) : WS:WordStack )
133+
( ( W0:Int => BALANCE_CELL:Int ) : _WS:WordStack )
134134
</wordStack>
135135
<pc>
136136
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module BLOCKHASH-SUMMARY
66
rule [BLOCKHASH-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ BLOCKHASH ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -18,7 +18,7 @@ module BLOCKHASH-SUMMARY
1818
<evm>
1919
<callState>
2020
<wordStack>
21-
( ( W0:Int => #blockhash ( BLOCKHASHES_CELL:List , W0:Int , ( NUMBER_CELL:Int +Int -1 ) , 0 ) ) : WS:WordStack )
21+
( ( W0:Int => #blockhash ( BLOCKHASHES_CELL:List , W0:Int , ( NUMBER_CELL:Int +Int -1 ) , 0 ) ) : _WS:WordStack )
2222
</wordStack>
2323
<pc>
2424
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
@@ -51,7 +51,7 @@ module BLOCKHASH-SUMMARY
5151
rule [BLOCKHASH-SUMMARY-NOGAS]: <kevm>
5252
<k>
5353
( #next [ BLOCKHASH ] ~> .K => .K )
54-
~> K_CELL:K
54+
~> _K_CELL:K
5555
</k>
5656
<useGas>
5757
( USEGAS_CELL:Bool => false )
@@ -60,13 +60,13 @@ module BLOCKHASH-SUMMARY
6060
<evm>
6161
<callState>
6262
<wordStack>
63-
( ( W0:Int => #blockhash ( BLOCKHASHES_CELL:List , W0:Int , ( NUMBER_CELL:Int +Int -1 ) , 0 ) ) : WS:WordStack )
63+
( ( W0:Int => #blockhash ( BLOCKHASHES_CELL:List , W0:Int , ( NUMBER_CELL:Int +Int -1 ) , 0 ) ) : _WS:WordStack )
6464
</wordStack>
6565
<pc>
6666
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
6767
</pc>
6868
<gas>
69-
GAS_CELL:Int
69+
_GAS_CELL:Int
7070
</gas>
7171
...
7272
</callState>

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module BYTE-SUMMARY
66
rule [BYTE-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ BYTE ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -42,7 +42,7 @@ module BYTE-SUMMARY
4242
rule [BYTE-SUMMARY-NOGAS]: <kevm>
4343
<k>
4444
( #next [ BYTE ] ~> .K => .K )
45-
~> K_CELL:K
45+
~> _K_CELL:K
4646
</k>
4747
<useGas>
4848
( USEGAS_CELL:Bool => false )
@@ -57,7 +57,7 @@ module BYTE-SUMMARY
5757
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
5858
</pc>
5959
<gas>
60-
GAS_CELL:Int
60+
_GAS_CELL:Int
6161
</gas>
6262
...
6363
</callState>

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module CALLDATACOPY-SUMMARY
66
rule [CALLDATACOPY-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ CALLDATACOPY ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -52,7 +52,7 @@ module CALLDATACOPY-SUMMARY
5252
rule [CALLDATACOPY-SUMMARY-NOGAS]: <kevm>
5353
<k>
5454
( #next [ CALLDATACOPY ] ~> .K => .K )
55-
~> K_CELL:K
55+
~> _K_CELL:K
5656
</k>
5757
<useGas>
5858
( USEGAS_CELL:Bool => false )
@@ -73,7 +73,7 @@ module CALLDATACOPY-SUMMARY
7373
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
7474
</pc>
7575
<gas>
76-
GAS_CELL:Int
76+
_GAS_CELL:Int
7777
</gas>
7878
...
7979
</callState>

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module CALLDATALOAD-SUMMARY
66
rule [CALLDATALOAD-SUMMARY-USEGAS]: <kevm>
77
<k>
88
( #next [ CALLDATALOAD ] ~> .K => .K )
9-
~> K_CELL:K
9+
~> _K_CELL:K
1010
</k>
1111
<schedule>
1212
SCHEDULE_CELL:Schedule
@@ -21,7 +21,7 @@ module CALLDATALOAD-SUMMARY
2121
CALLDATA_CELL:Bytes
2222
</callData>
2323
<wordStack>
24-
( ( W0:Int => #asWord ( #range ( CALLDATA_CELL:Bytes , W0:Int , 32 ) ) ) : WS:WordStack )
24+
( ( W0:Int => #asWord ( #range ( CALLDATA_CELL:Bytes , W0:Int , 32 ) ) ) : _WS:WordStack )
2525
</wordStack>
2626
<pc>
2727
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
@@ -45,7 +45,7 @@ module CALLDATALOAD-SUMMARY
4545
rule [CALLDATALOAD-SUMMARY-NOGAS]: <kevm>
4646
<k>
4747
( #next [ CALLDATALOAD ] ~> .K => .K )
48-
~> K_CELL:K
48+
~> _K_CELL:K
4949
</k>
5050
<useGas>
5151
( USEGAS_CELL:Bool => false )
@@ -57,13 +57,13 @@ module CALLDATALOAD-SUMMARY
5757
CALLDATA_CELL:Bytes
5858
</callData>
5959
<wordStack>
60-
( ( W0:Int => #asWord ( #range ( CALLDATA_CELL:Bytes , W0:Int , 32 ) ) ) : WS:WordStack )
60+
( ( W0:Int => #asWord ( #range ( CALLDATA_CELL:Bytes , W0:Int , 32 ) ) ) : _WS:WordStack )
6161
</wordStack>
6262
<pc>
6363
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
6464
</pc>
6565
<gas>
66-
GAS_CELL:Int
66+
_GAS_CELL:Int
6767
</gas>
6868
...
6969
</callState>

0 commit comments

Comments
 (0)