Enhance summary specification file generation for balance opcode

- Add function to replace LHS function with assignment in summary-balance specs
- Modify account ID representation in balance summary files
- Update regex transformation to simplify account ID constraints

Author: Stevengre

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

@@ -39,9 +39,7 @@ imports BUF
              <network>
                <accounts>
                  <account>
-                   <acctID>
-                     ACCTID 
-                   </acctID>
+                   <acctID> ACCTID_CELL_CELL </acctID>
                    <balance>
                      BALANCE_CELL:Int
                    </balance>
@@ -54,8 +52,8 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ACCTID ==Int  W0:Int modInt pow160
 
-      [priority(20), label(BASIC-BLOCK-1-TO-3)]
+      requires ACCTID_CELL_CELL ==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

@@ -39,9 +39,7 @@ imports BUF
              <network>
                <accounts>
                  <account>
-                   <acctID>
-                     ( W0:Int modInt pow160 )
-                   </acctID>
+                   <acctID> ACCTID_CELL_CELL </acctID>
                    <balance>
                      BALANCE_CELL:Int
                    </balance>
@@ -55,6 +53,7 @@ imports BUF
            ...
          </kevm>
 
-      [priority(20), label(BASIC-BLOCK-1-TO-3)]
+      requires ACCTID_CELL_CELL ==Int W0:Int modInt pow160
+[priority(20), label(BASIC-BLOCK-1-TO-3)]
 
 endmodule

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -608,6 +608,18 @@ def _use_legal_remainder(res_line: str) -> str:
             res_line_tmp = re.sub(r'(\()\s*andBool\s*([\s\S]*?)\s*(\))', r'\1\2\3', res_line_tmp)
             res_line_tmp = re.sub(r'andBool\s*\(\s*\)', r'', res_line_tmp)
             return res_line_tmp
+        
+        def replace_lhs_function_by_assignment(res_line: str) -> str:
+            # just for summary-balance
+            if not 'SUMMARY-BALANCE' in res_line:
+                return res_line
+            pattern = r'<acctID>\s*(\(\s*W0:Int modInt pow160\s*\))\s*</acctID>'
+            if re.search(pattern, res_line):
+                # 找到这个pattern的位置
+                replace_pattern = r'<acctID> ACCTID_CELL_CELL </acctID>'
+                res_line = re.sub(pattern, replace_pattern, res_line)
+                res_line = re.sub(r'(</kevm>\s*)', r'\1requires ACCTID_CELL_CELL ==Int W0:Int modInt pow160\n', res_line)
+            return res_line
 
         spec_name = f'summary-{proof.id.replace("_", "-").lower()}.k'
         with open(self.save_directory / spec_name, 'w') as f:
@@ -617,6 +629,7 @@ def _use_legal_remainder(res_line: str) -> str:
                     res_line = _remove_inf_gas(res_line)
                     res_line = _remove_dash_from_var(res_line)
                     res_line = _use_legal_remainder(res_line)
+                    res_line = replace_lhs_function_by_assignment(res_line)
                     f.write('requires "../evm.md"\n')
                     f.write('requires "../buf.md"\n\n')
                     lines = res_line.split('\n')