Integrate summaries of opcode automatically into the evm semantics

.github/workflows/test-pr.yml

@@ -132,7 +132,7 @@ jobs:
       - name: 'Build kevm-pyk'
         run: docker exec -u github-user kevm-ci-haskell-${{ matrix.test-suite }}-${{ github.sha }} /bin/bash -c 'make poetry'
       - name: 'Build distribution'
-        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'
+        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.summarize'
       - name: 'Run proofs'
         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 }}"
       - name: 'Tear down Docker'

Makefile

@@ -77,6 +77,9 @@ test-prove-functional: poetry
 test-prove-optimizations: poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_optimizations"
 
+test-prove-summaries: poetry
+	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_summaries"
+
 test-prove-dss: poetry
 	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_prove_dss"
 

kevm-pyk/.gitignore

@@ -1,5 +1,4 @@
 /dist/
 __pycache__/
 .coverage
-proofs/
-summaries/
+proofs/

kevm-pyk/src/kevm_pyk/__main__.py

@@ -32,10 +32,15 @@
 from pyk.proof.tui import APRProofViewer
 from pyk.utils import FrozenDict, hash_str, single
 
-from kevm_pyk.summarizer import batch_summarize
+from kevm_pyk.summarizer import batch_summarize, clear_proofs, summarize
 
 from . import VERSION, config
-from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
+from .cli import (
+    _create_argument_parser,
+    generate_options,
+    get_argument_type_setter,
+    get_option_string_destination,
+)
 from .gst_to_kore import SORT_ETHEREUM_SIMULATION, filter_gst_keys, gst_to_kore, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile
@@ -65,6 +70,7 @@
         RunOptions,
         SectionEdgeOptions,
         ShowKCFGOptions,
+        SummarizeOptions,
         VersionOptions,
         ViewKCFGOptions,
     )
@@ -636,10 +642,14 @@ def exec_kast(options: KastOptions) -> None:
     print(output_text)
 
 
-def exec_summarize(options: ProveOptions) -> None:
-    # TODO: provide options to summarize specific opcodes using `summarize(opcode)`
+def exec_summarize(options: SummarizeOptions) -> None:
     # TODO: provide options to analyze a specific proof using `analyze_proof(opcode, node_id)`
-    batch_summarize()
+    if options.clear:
+        clear_proofs()
+    if options.opcode is None:
+        batch_summarize()
+    else:
+        summarize(options.opcode)
 
 
 # Helpers

kevm-pyk/src/kevm_pyk/cli.py

@@ -77,7 +77,7 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions:
         case 'run':
             return RunOptions(args)
         case 'summarize':
-            return ProveOptions(args)
+            return SummarizeOptions(args)
         case _:
             raise ValueError(f'Unrecognized command: {command}')
 
@@ -104,7 +104,7 @@ def get_option_string_destination(command: str, option_string: str) -> str:
         case 'run':
             option_string_destinations = RunOptions.from_option_string()
         case 'summarize':
-            option_string_destinations = ProveOptions.from_option_string()
+            option_string_destinations = SummarizeOptions.from_option_string()
 
     return option_string_destinations.get(option_string, option_string.replace('-', '_'))
 
@@ -134,7 +134,7 @@ def func(par: str) -> str:
         case 'run':
             option_types = RunOptions.get_argument_type()
         case 'summarize':
-            option_types = ProveOptions.get_argument_type()
+            option_types = SummarizeOptions.get_argument_type()
 
     return option_types.get(option_string, func)
 
@@ -191,22 +191,27 @@ def _create_argument_parser() -> ArgumentParser:
         help='Maximum worker threads to use on a single proof to explore separate branches in parallel.',
     )
 
-    command_parser.add_parser(
+    summarize_args = command_parser.add_parser(
         'summarize',
         help='Summarize an Opcode to execute in a single rewrite step.',
         parents=[
             kevm_cli_args.logging_args,
-            kevm_cli_args.parallel_args,
             kevm_cli_args.k_args,
-            kevm_cli_args.kprove_args,
-            kevm_cli_args.rpc_args,
-            kevm_cli_args.bug_report_args,
-            kevm_cli_args.smt_args,
-            kevm_cli_args.explore_args,
-            # kevm_cli_args.spec_args,
-            config_args.config_args,
         ],
     )
+    summarize_args.add_argument(
+        'opcode',
+        type=str,
+        nargs='?',
+        help='Opcode to summarize. If not provided, all supported opcodes will be summarized.',
+    )
+    summarize_args.add_argument(
+        '--clear',
+        dest='clear',
+        default=False,
+        action='store_true',
+        help='Clear all existing proofs and re-run the summarization process.',
+    )
 
     prune_args = command_parser.add_parser(
         'prune',
@@ -620,6 +625,23 @@ def get_argument_type() -> dict[str, Callable]:
         )
 
 
+class SummarizeOptions(LoggingOptions, KOptions):
+    clear: bool
+    opcode: str | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {'clear': False, 'opcode': None}
+
+    @staticmethod
+    def from_option_string() -> dict[str, str]:
+        return LoggingOptions.from_option_string() | KOptions.from_option_string()
+
+    @staticmethod
+    def get_argument_type() -> dict[str, Callable]:
+        return LoggingOptions.get_argument_type() | KOptions.get_argument_type()
+
+
 class PruneOptions(LoggingOptions, KOptions, SpecOptions):
     node: NodeIdLike
 
@@ -833,7 +855,9 @@ class KEVMCLIArgs(KCLIArgs):
     @cached_property
     def target_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)
-        args.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry'])
+        args.add_argument(
+            '--target', choices=['llvm', 'llvm-summary', 'haskell', 'haskell-standalone', 'haskell-summary', 'foundry']
+        )
         return args
 
     @cached_property

kevm-pyk/src/kevm_pyk/interpreter.py

@@ -1,9 +1,11 @@
 from __future__ import annotations
 
+from subprocess import CalledProcessError
 from typing import TYPE_CHECKING
 
 from pyk.kdist import kdist
 from pyk.kore.parser import KoreParser
+from pyk.ktool.krun import llvm_interpret_raw
 from pyk.utils import run_process_2
 
 from .gst_to_kore import filter_gst_keys, gst_to_kore
@@ -16,18 +18,18 @@
 
 
 def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool, *, check: bool = True) -> Pattern:
-    proc_res = _interpret(gst_data, schedule, mode, chainid, usegas)
+    try:
+        res = _interpret(gst_data, schedule, mode, chainid, usegas, check)
+    except CalledProcessError as err:
+        raise RuntimeError(f'Interpreter failed with status {err.returncode}: {err.stderr}') from err
 
-    if check:
-        proc_res.check_returncode()
+    if res.stdout == '':
+        raise RuntimeError(f'Interpreter returned empty stdout: {res.stderr}')
 
-    kore = KoreParser(proc_res.stdout).pattern()
-    return kore
+    return KoreParser(res.stdout).pattern()
 
 
-def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool) -> CompletedProcess:
+def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool, check: bool) -> CompletedProcess:
     gst_data_filtered = filter_gst_keys(gst_data)
-    interpreter = kdist.get('evm-semantics.llvm') / 'interpreter'
     init_kore = gst_to_kore(gst_data_filtered, schedule, mode, chainid, usegas)
-    proc_res = run_process_2([str(interpreter), '/dev/stdin', '-1', '/dev/stdout'], input=init_kore.text, check=False)
-    return proc_res
+    return llvm_interpret_raw(kdist.get('evm-semantics.llvm-summary'), init_kore.text, check=check)

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

@@ -115,12 +115,29 @@ def context(self) -> dict[str, str]:
             'syntax_module': 'EDSL',
         },
     ),
-    'summary': KEVMTarget(
+    'summarize': KEVMTarget(
         {
             'target': KompileTarget.HASKELL,
             'main_file': config.EVM_SEMANTICS_DIR / 'edsl.md',
-            'main_module': 'EDSL-SUM',
-            'syntax_module': 'EDSL-SUM',
+            'main_module': 'EDSL-SUMMARIZE',
+            'syntax_module': 'EDSL-SUMMARIZE',
+        },
+    ),
+    'llvm-summary': KEVMTarget(
+        {
+            'target': KompileTarget.LLVM,
+            'main_file': config.EVM_SEMANTICS_DIR / 'driver.md',
+            'main_module': 'ETHEREUM-SIMULATION-SUMMARY',
+            'syntax_module': 'ETHEREUM-SIMULATION-SUMMARY',
+            'optimization': 3,
+        },
+    ),
+    'haskell-summary': KEVMTarget(
+        {
+            'target': KompileTarget.HASKELL,
+            'main_file': config.EVM_SEMANTICS_DIR / 'edsl.md',
+            'main_module': 'EDSL-SUMMARY',
+            'syntax_module': 'EDSL-SUMMARY',
         },
     ),
     'haskell-standalone': KEVMTarget(

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

@@ -9,10 +9,20 @@ requires "evm.md"
 requires "optimizations.md"
 requires "asm.md"
 requires "state-utils.md"
+requires "summaries/summary.k"
+
+module ETHEREUM-SIMULATION-SUMMARY
+    imports ETHEREUM-SIMULATION-PURE
+    imports SUMMARY
+endmodule
 
 module ETHEREUM-SIMULATION
-    imports EVM
+    imports ETHEREUM-SIMULATION-PURE
     imports EVM-OPTIMIZATIONS
+endmodule
+
+module ETHEREUM-SIMULATION-PURE
+    imports EVM
     imports EVM-ASSEMBLY
     imports STATE-UTILS
 ```

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

@@ -14,8 +14,14 @@ requires "gas.md"
 requires "optimizations.md"
 requires "lemmas/lemmas.k"
 requires "lemmas/summarization-simplification.k"
+requires "summaries/summary.k"
 
-module EDSL-SUM
+module EDSL-SUMMARY
+    imports EDSL-PURE
+    imports SUMMARY
+endmodule
+
+module EDSL-SUMMARIZE
     imports EDSL-PURE
     imports LEMMAS
     imports SUMMARIZATION-SIMPLIFICATION

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

@@ -0,0 +1,74 @@
+requires "../evm.md"
+requires "../buf.md"
+
+module SUMMARY-ADD-2-SPEC
+imports EVM
+imports BUF
+
+
+    rule [BASIC-BLOCK-21-TO-20]: <kevm>
+           <k>
+             ( #next [ ADD ] ~> .K => .K )
+             ~> K_CELL:K
+           </k>
+           <schedule>
+             SCHEDULE_CELL:Schedule
+           </schedule>
+           <useGas>
+             ( USEGAS_CELL:Bool => true )
+           </useGas>
+           <ethereum>
+             <evm>
+               <callState>
+                 <wordStack>
+                   ( ( W0:Int => chop ( ( W0:Int +Int W1:Int ) ) ) : ( ( W1:Int : WS:WordStack ) => WS:WordStack ) )
+                 </wordStack>
+                 <pc>
+                   ( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
+                 </pc>
+                 <gas>
+                    ( ( GAS_CELL:Int => ( GAS_CELL:Int -Int Gverylow < SCHEDULE_CELL:Schedule > ) ) )
+                 </gas>
+                 ...
+               </callState>
+               ...
+             </evm>
+             ...
+           </ethereum>
+           ...
+         </kevm>
+      requires USEGAS_CELL:Bool  andBool ( ( ( Gverylow < SCHEDULE_CELL:Schedule > ) ) ) <=Int GAS_CELL 
+      [priority(20), label(BASIC-BLOCK-21-TO-20)]
+
+    rule [BASIC-BLOCK-22-TO-15]: <kevm>
+           <k>
+             ( #next [ ADD ] ~> .K => .K )
+             ~> K_CELL:K
+           </k>
+           <useGas>
+             ( USEGAS_CELL:Bool => false )
+           </useGas>
+           <ethereum>
+             <evm>
+               <callState>
+                 <wordStack>
+                   ( ( W0:Int => chop ( ( W0:Int +Int W1:Int ) ) ) : ( ( W1:Int : WS:WordStack ) => WS:WordStack ) )
+                 </wordStack>
+                 <pc>
+                   ( PC_CELL:Int => ( PC_CELL:Int +Int 1 ) )
+                 </pc>
+                 <gas>
+                    ( GAS_CELL:Int )
+                 </gas>
+                 ...
+               </callState>
+               ...
+             </evm>
+             ...
+           </ethereum>
+           ...
+         </kevm>
+      requires ( notBool USEGAS_CELL:Bool )
+      [priority(20), label(BASIC-BLOCK-22-TO-15)]
+
+endmodule