From 40207c61d9e503b07e3640feb3e9808adcd6d24a Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Thu, 23 Jan 2025 14:47:12 +0000
Subject: [PATCH] recover the definition and create a new target for
 summarization

---
 kevm-pyk/src/kevm_pyk/kdist/plugin.py         |  8 +++++
 .../kevm_pyk/kproj/evm-semantics/driver.md    |  4 +--
 .../kevm_pyk/kproj/evm-semantics/edsl-sum.md  | 35 +++++++++++++++++++
 .../src/kevm_pyk/kproj/evm-semantics/edsl.md  |  4 +--
 kevm-pyk/src/kevm_pyk/summarizer.py           |  2 +-
 5 files changed, 48 insertions(+), 5 deletions(-)
 create mode 100644 kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl-sum.md

diff --git a/kevm-pyk/src/kevm_pyk/kdist/plugin.py b/kevm-pyk/src/kevm_pyk/kdist/plugin.py
index 184679b4d4..7a0f4e88b3 100644
--- 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
index 114646b241..d53577b5ea 100644
--- 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
new file mode 100644
index 0000000000..2e225766b7
--- /dev/null
+++ 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
index 0749e200d5..ce631b3183 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md
@@ -11,7 +11,7 @@ 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
@@ -19,7 +19,7 @@ module EDSL
     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
index 6725d728b8..fd24f23e7a 100644
--- 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