recover the definition and create a new target for summarization

runtimeverification · Jan 23, 2025 · 40207c6 · 40207c6
1 parent 8ececbf
commit 40207c6
Show file tree

Hide file tree

Showing 5 changed files with 48 additions and 5 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py
@@ -115,6 +115,14 @@ def context(self) -> dict[str, str]:
             'syntax_module': 'EDSL',
         },
     ),
+    'summary': KEVMTarget(
+        {
+            'target': KompileTarget.HASKELL,
+            'main_file': config.EVM_SEMANTICS_DIR / 'edsl-sum.md',
+            'main_module': 'EDSL',
+            'syntax_module': 'EDSL',
+        },
+    ),
     'haskell-standalone': KEVMTarget(
         {
             'target': KompileTarget.HASKELL,

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -6,13 +6,13 @@ Actual execution of the EVM is defined in [the EVM file](../evm).
 
 ```k
 requires "evm.md"
-// requires "optimizations.md"
+requires "optimizations.md"
 requires "asm.md"
 requires "state-utils.md"
 
 module ETHEREUM-SIMULATION
     imports EVM
-//    imports EVM-OPTIMIZATIONS
+    imports EVM-OPTIMIZATIONS
     imports EVM-ASSEMBLY
     imports STATE-UTILS
 ```

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl-sum.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl-sum.md
@@ -0,0 +1,35 @@
+eDSL High-Level Notations
+=========================
+
+The eDSL high-level notations make the EVM specifications more succinct and closer to their high-level specifications.
+The succinctness increases the readability, and the closeness helps "eye-ball validation" of the specification refinement.
+The high-level notations are defined by translation to the corresponding EVM terms, and thus can be freely used with other EVM terms.
+The notations are inspired by the production compilers of the smart contract languages like Solidity and Vyper, and their definition is derived by formalizing the corresponding translation made by the compilers.
+
+```k
+requires "buf.md"
+requires "hashed-locations.md"
+requires "abi.md"
+requires "gas.md"
+requires "lemmas/lemmas.k"
+
+module EDSL
+    imports BUF
+    imports HASHED-LOCATIONS
+    imports SOLIDITY-FIELDS
+    imports EVM-ABI
+    imports INFINITE-GAS
+    imports BIN-RUNTIME
+    imports LEMMAS
+endmodule
+
+module BIN-RUNTIME
+    imports EVM-ABI
+
+    syntax Contract
+    syntax Bytes ::= #binRuntime ( Contract )   [alias, symbol(binRuntime)  , function, no-evaluators]
+                   | #initBytecode ( Contract ) [alias, symbol(initBytecode), function, no-evaluators]
+ // --------------------------------------------------------------------------------------------------
+
+endmodule
+```
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md
@@ -11,15 +11,15 @@ requires "buf.md"
 requires "hashed-locations.md"
 requires "abi.md"
 requires "gas.md"
-// requires "optimizations.md"
+requires "optimizations.md"
 requires "lemmas/lemmas.k"
 
 module EDSL
     imports BUF
     imports HASHED-LOCATIONS
     imports SOLIDITY-FIELDS
     imports EVM-ABI
-//    imports EVM-OPTIMIZATIONS
+    imports EVM-OPTIMIZATIONS
     imports INFINITE-GAS
     imports BIN-RUNTIME
     imports LEMMAS

diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py
@@ -352,7 +352,7 @@ class KEVMSummarizer:
     save_directory: Path
 
     def __init__(self, proof_dir: Path, save_directory: Path) -> None:
-        self.kevm = KEVM(kdist.get('evm-semantics.haskell'))
+        self.kevm = KEVM(kdist.get('evm-semantics.summary'))
         self.proof_dir = proof_dir
         self.save_directory = save_directory