Generate summary specification files for multiple EVM opcodes

- Update summary files for numerous EVM opcodes
- Modify basic block rules in summary specification files
- Systematically process and generate summary files for various EVM instructions

Author: Stevengre

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

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-ADD-2-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-8-TO-6]: <kevm>

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

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-ADDMOD-3-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-8-TO-6]: <kevm>

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

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-ADDRESS-0-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-3-TO-8]: <kevm>

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

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-AND-2-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-8-TO-7]: <kevm>

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-balance-normal-1-spec.k

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-BALANCE-NORMAL-1-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-1-TO-3]: <kevm>
@@ -38,7 +40,7 @@ imports EVM
                <accounts>
                  <account>
                    <acctID>
-                     ( W0:Int modInt pow160 )
+                     ACCTID 
                    </acctID>
                    <balance>
                      BALANCE_CELL:Int
@@ -52,9 +54,8 @@ imports EVM
            </ethereum>
            ...
          </kevm>
-      requires ( notBool <acctID>
-        ( W0:Int modInt pow160 )
-      </acctID> in_keys ( DotAccountVar:AccountCellMap ) )
+      requires ACCTID ==Int  W0:Int modInt pow160
+       
       [priority(20), label(BASIC-BLOCK-1-TO-3)]
 
 endmodule

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-balance-owise-1-spec.k

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-BALANCE-OWISE-1-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-1-TO-3]: <kevm>
@@ -52,9 +54,7 @@ imports EVM
            </ethereum>
            ...
          </kevm>
-      requires ( notBool <acctID>
-        ( W0:Int modInt pow160 )
-      </acctID> in_keys ( DotAccountVar:AccountCellMap ) )
+       
       [priority(20), label(BASIC-BLOCK-1-TO-3)]
 
 endmodule

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-blockhash-1-spec.k

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-BLOCKHASH-1-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-8-TO-7]: <kevm>

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

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-BYTE-2-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-8-TO-6]: <kevm>

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-calldatacopy-3-spec.k

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-CALLDATACOPY-3-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-8-TO-7]: <kevm>

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-calldataload-1-spec.k

@@ -1,7 +1,9 @@
 requires "../evm.md"
+requires "../buf.md"
 
 module SUMMARY-CALLDATALOAD-1-SPEC
 imports EVM
+imports BUF
 
 
     rule [BASIC-BLOCK-8-TO-6]: <kevm>