From 05a772c47e19147395de21150fe2bde9b37dd66a 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 e39fd5d6d4..b53dc37b9d 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