Skip to content

Commit bf5a247

Browse files
StevengreStevengre
authored
Integrate opcode semantics summaries (#2728)
* Integrate opcode semantics summaries - Refactored the summarize function to print correct and compilable k definitions for summaries. - Added new summary targets for LLVM and Haskell backend in the KEVM plugin. - Updated the Makefile to include a new test target for `test-prove-summaries`. - Refactored the test suite to validate opcode summaries. - Adjusted imports in the driver and EDSL modules to incorporate the new summaries. - Cleaned up the `.gitignore` to ensure proper tracking of relevant files. * make test-integration PYTEST_ARGS+="--update-expected-output" * Enhance target options in CLI by adding new summary targets for LLVM and Haskell. This update expands the choices available for the `--target` argument to include `llvm-summary` and `haskell-summary`. * Update test suite configuration in GitHub Actions workflow - Changed the test suite for the 'Summarization' job from 'test-summarize' to 'test-prove-summaries'. - Adjusted timeout and parallel execution settings for the 'Summarization' job to improve performance. - Updated the build command for the distribution to include 'evm-semantics.haskell-summary' instead of 'evm-semantics.summary'. * Pulling nested transformation functions to module level & move model instantiation out of the context manager's scope. * convert `_transform` functions into module functions; extract helper functions to get the summary kdefinition for printing.
1 parent ebad50f commit bf5a247

Some content is hidden

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

82 files changed

+7225
-100
lines changed

‎.github/workflows/test-pr.yml

+4-4
Original file line numberDiff line numberDiff line change
@@ -108,10 +108,10 @@ jobs:
108108
timeout: 45
109109
parallel: 1
110110
- name: 'Summarization'
111-
test-suite: 'test-summarize'
111+
test-suite: 'test-prove-summaries'
112112
test-args:
113-
timeout: 30
114-
parallel: 6
113+
timeout: 45
114+
parallel: 4
115115
- name: 'DSS'
116116
test-suite: 'test-prove-dss'
117117
test-args:
@@ -132,7 +132,7 @@ jobs:
132132
- name: 'Build kevm-pyk'
133133
run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
134134
- name: 'Build distribution'
135-
run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell evm-semantics.summary'
135+
run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'CXX=clang++-14 poetry -C kevm-pyk run kdist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell evm-semantics.haskell-summary'
136136
- name: 'Run proofs'
137137
run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c "make ${{ matrix.test-suite }} PYTEST_ARGS='-vv ${{ matrix.test-args }}' PYTEST_PARALLEL=${{ matrix.parallel }}"
138138
- name: 'Tear down Docker'

‎Makefile

+3
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,9 @@ test-prove-functional: poetry
7777
test-prove-optimizations: poetry
7878
$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_optimizations"
7979

80+
test-prove-summaries: poetry
81+
$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_summaries"
82+
8083
test-prove-dss: poetry
8184
$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_dss"
8285

‎kevm-pyk/.gitignore

+1-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
/dist/
22
__pycache__/
33
.coverage
4-
proofs/
5-
summaries/
4+
proofs/

‎kevm-pyk/src/kevm_pyk/cli.py

+3-1
Original file line numberDiff line numberDiff line change
@@ -855,7 +855,9 @@ class KEVMCLIArgs(KCLIArgs):
855855
@cached_property
856856
def target_args(self) -> ArgumentParser:
857857
args = ArgumentParser(add_help=False)
858-
args.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry'])
858+
args.add_argument(
859+
'--target', choices=['llvm', 'haskell', 'llvm-summary', 'haskell-summary', 'haskell-standalone', 'foundry']
860+
)
859861
return args
860862

861863
@cached_property

‎kevm-pyk/src/kevm_pyk/kdist/plugin.py

+17
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,23 @@ def context(self) -> dict[str, str]:
123123
'syntax_module': 'EDSL-SUM',
124124
},
125125
),
126+
'llvm-summary': KEVMTarget(
127+
{
128+
'target': KompileTarget.LLVM,
129+
'main_file': config.EVM_SEMANTICS_DIR / 'driver.md',
130+
'main_module': 'ETHEREUM-SIMULATION-SUMMARY',
131+
'syntax_module': 'ETHEREUM-SIMULATION-SUMMARY',
132+
'optimization': 3,
133+
},
134+
),
135+
'haskell-summary': KEVMTarget(
136+
{
137+
'target': KompileTarget.HASKELL,
138+
'main_file': config.EVM_SEMANTICS_DIR / 'edsl.md',
139+
'main_module': 'EDSL-SUMMARY',
140+
'syntax_module': 'EDSL-SUMMARY',
141+
},
142+
),
126143
'haskell-standalone': KEVMTarget(
127144
{
128145
'target': KompileTarget.HASKELL,

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

+11-1
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,20 @@ requires "evm.md"
99
requires "optimizations.md"
1010
requires "asm.md"
1111
requires "state-utils.md"
12+
requires "summaries/summaries.k"
13+
14+
module ETHEREUM-SIMULATION-SUMMARY
15+
imports ETHEREUM-SIMULATION-PURE
16+
imports KEVM-SUMMARIES
17+
endmodule
1218
1319
module ETHEREUM-SIMULATION
14-
imports EVM
20+
imports ETHEREUM-SIMULATION-PURE
1521
imports EVM-OPTIMIZATIONS
22+
endmodule
23+
24+
module ETHEREUM-SIMULATION-PURE
25+
imports EVM
1626
imports EVM-ASSEMBLY
1727
imports STATE-UTILS
1828
```

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

+6
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,12 @@ requires "gas.md"
1414
requires "optimizations.md"
1515
requires "lemmas/lemmas.k"
1616
requires "lemmas/summarization-simplification.k"
17+
requires "summaries/summaries.k"
18+
19+
module EDSL-SUMMARY
20+
imports EDSL-PURE
21+
imports KEVM-SUMMARIES
22+
endmodule
1723
1824
module EDSL-SUM
1925
imports EDSL-PURE

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

+73
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
requires "../evm.md"
2+
3+
module ADD-SUMMARY
4+
imports public EVM
5+
6+
rule [ADD-SUMMARY-0]: <kevm>
7+
<k>
8+
( #next [ ADD ] ~> .K => .K )
9+
~> K_CELL:K
10+
</k>
11+
<schedule>
12+
SCHEDULE_CELL:Schedule
13+
</schedule>
14+
<useGas>
15+
( USEGAS_CELL:Bool => true )
16+
</useGas>
17+
<ethereum>
18+
<evm>
19+
<callState>
20+
<wordStack>
21+
( ( W0:Int => chop ( ( W0:Int +Int W1:Int ) ) ) : ( ( W1:Int : WS:WordStack ) => WS:WordStack ) )
22+
</wordStack>
23+
<pc>
24+
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
25+
</pc>
26+
<gas>
27+
( GAS_CELL:Int => ( GAS_CELL:Int -Int Gverylow < SCHEDULE_CELL:Schedule > ) )
28+
</gas>
29+
...
30+
</callState>
31+
...
32+
</evm>
33+
...
34+
</ethereum>
35+
...
36+
</kevm>
37+
requires ( USEGAS_CELL:Bool
38+
andBool ( Gverylow < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
39+
))
40+
[priority(20), label(ADD-SUMMARY-0)]
41+
42+
rule [ADD-SUMMARY-1]: <kevm>
43+
<k>
44+
( #next [ ADD ] ~> .K => .K )
45+
~> K_CELL:K
46+
</k>
47+
<useGas>
48+
( USEGAS_CELL:Bool => false )
49+
</useGas>
50+
<ethereum>
51+
<evm>
52+
<callState>
53+
<wordStack>
54+
( ( W0:Int => chop ( ( W0:Int +Int W1:Int ) ) ) : ( ( W1:Int : WS:WordStack ) => WS:WordStack ) )
55+
</wordStack>
56+
<pc>
57+
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
58+
</pc>
59+
<gas>
60+
GAS_CELL:Int
61+
</gas>
62+
...
63+
</callState>
64+
...
65+
</evm>
66+
...
67+
</ethereum>
68+
...
69+
</kevm>
70+
requires ( notBool USEGAS_CELL:Bool )
71+
[priority(20), label(ADD-SUMMARY-1)]
72+
73+
endmodule

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

+73
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
requires "../evm.md"
2+
3+
module ADDMOD-SUMMARY
4+
imports public EVM
5+
6+
rule [ADDMOD-SUMMARY-0]: <kevm>
7+
<k>
8+
( #next [ ADDMOD ] ~> .K => .K )
9+
~> K_CELL:K
10+
</k>
11+
<schedule>
12+
SCHEDULE_CELL:Schedule
13+
</schedule>
14+
<useGas>
15+
( USEGAS_CELL:Bool => true )
16+
</useGas>
17+
<ethereum>
18+
<evm>
19+
<callState>
20+
<wordStack>
21+
( ( W0:Int => ( W0:Int +Int W1:Int ) %Word W2:Int ) : ( ( W1:Int : ( W2:Int : WS:WordStack ) ) => WS:WordStack ) )
22+
</wordStack>
23+
<pc>
24+
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
25+
</pc>
26+
<gas>
27+
( GAS_CELL:Int => ( GAS_CELL:Int -Int Gmid < SCHEDULE_CELL:Schedule > ) )
28+
</gas>
29+
...
30+
</callState>
31+
...
32+
</evm>
33+
...
34+
</ethereum>
35+
...
36+
</kevm>
37+
requires ( USEGAS_CELL:Bool
38+
andBool ( Gmid < SCHEDULE_CELL:Schedule > <=Int GAS_CELL:Int
39+
))
40+
[priority(20), label(ADDMOD-SUMMARY-0)]
41+
42+
rule [ADDMOD-SUMMARY-1]: <kevm>
43+
<k>
44+
( #next [ ADDMOD ] ~> .K => .K )
45+
~> K_CELL:K
46+
</k>
47+
<useGas>
48+
( USEGAS_CELL:Bool => false )
49+
</useGas>
50+
<ethereum>
51+
<evm>
52+
<callState>
53+
<wordStack>
54+
( ( W0:Int => ( W0:Int +Int W1:Int ) %Word W2:Int ) : ( ( W1:Int : ( W2:Int : WS:WordStack ) ) => WS:WordStack ) )
55+
</wordStack>
56+
<pc>
57+
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
58+
</pc>
59+
<gas>
60+
GAS_CELL:Int
61+
</gas>
62+
...
63+
</callState>
64+
...
65+
</evm>
66+
...
67+
</ethereum>
68+
...
69+
</kevm>
70+
requires ( notBool USEGAS_CELL:Bool )
71+
[priority(20), label(ADDMOD-SUMMARY-1)]
72+
73+
endmodule

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

+114
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
requires "../evm.md"
2+
3+
module ADDRESS-SUMMARY
4+
imports public EVM
5+
6+
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>
35+
<k>
36+
( #next [ ADDRESS ] ~> .K => .K )
37+
~> K_CELL:K
38+
</k>
39+
<schedule>
40+
SCHEDULE_CELL:Schedule
41+
</schedule>
42+
<useGas>
43+
( USEGAS_CELL:Bool => true )
44+
</useGas>
45+
<ethereum>
46+
<evm>
47+
<callState>
48+
<id>
49+
ID_CELL:Int
50+
</id>
51+
<wordStack>
52+
( WS:WordStack => ( ID_CELL:Int : WS:WordStack ) )
53+
</wordStack>
54+
<pc>
55+
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
56+
</pc>
57+
<gas>
58+
( GAS_CELL:Int => ( GAS_CELL:Int -Int Gbase < SCHEDULE_CELL:Schedule > ) )
59+
</gas>
60+
...
61+
</callState>
62+
...
63+
</evm>
64+
...
65+
</ethereum>
66+
...
67+
</kevm>
68+
requires ( USEGAS_CELL:Bool
69+
andBool ( ( notBool #sizeWordStack ( WS:WordStack , 0 ) <Int 0 )
70+
andBool ( ( notBool 1023 <Int #sizeWordStack ( WS:WordStack , 0 ) )
71+
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)]
75+
76+
rule [ADDRESS-SUMMARY-2]: <kevm>
77+
<k>
78+
( #next [ ADDRESS ] ~> .K => .K )
79+
~> K_CELL:K
80+
</k>
81+
<useGas>
82+
( USEGAS_CELL:Bool => false )
83+
</useGas>
84+
<ethereum>
85+
<evm>
86+
<callState>
87+
<id>
88+
ID_CELL:Int
89+
</id>
90+
<wordStack>
91+
( WS:WordStack => ( ID_CELL:Int : WS:WordStack ) )
92+
</wordStack>
93+
<pc>
94+
( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
95+
</pc>
96+
<gas>
97+
GAS_CELL:Int
98+
</gas>
99+
...
100+
</callState>
101+
...
102+
</evm>
103+
...
104+
</ethereum>
105+
...
106+
</kevm>
107+
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)]
113+
114+
endmodule

0 commit comments

Comments
 (0)