make test-prove-summaries passed

Stevengre · Stevengre · commit 6ae2c015a6d3 · 2025-03-14T16:23:24.000Z
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-calldatacopy-3-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-calldatacopy-3-spec.k
@@ -46,7 +46,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL 
+      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL
       [priority(20), label(BASIC-BLOCK-22-TO-21)]
     
     rule [BASIC-BLOCK-23-TO-13]: <kevm>
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-codecopy-3-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-codecopy-3-spec.k
@@ -46,7 +46,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL 
+      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL
       [priority(20), label(BASIC-BLOCK-22-TO-21)]
     
     rule [BASIC-BLOCK-23-TO-13]: <kevm>
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-2-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-2-spec.k
@@ -86,7 +86,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) ) ) ) <=Int GAS_CELL  
+      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL 
        andBool ( ( notBool STATIC_CELL:Bool )
                ))
       [priority(20), label(BASIC-BLOCK-26-TO-25)]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-3-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-3-spec.k
@@ -86,7 +86,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) <=Int GAS_CELL  
+      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL 
        andBool ( ( notBool STATIC_CELL:Bool )
                ))
       [priority(20), label(BASIC-BLOCK-26-TO-25)]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-4-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-4-spec.k
@@ -86,7 +86,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int ( 2 *Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) ) <=Int GAS_CELL  
+      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int ( 2 *Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL 
        andBool ( ( notBool STATIC_CELL:Bool )
                ))
       [priority(20), label(BASIC-BLOCK-26-TO-25)]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-5-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-5-spec.k
@@ -86,7 +86,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int ( 3 *Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) ) <=Int GAS_CELL  
+      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int ( 3 *Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL 
        andBool ( ( notBool STATIC_CELL:Bool )
                ))
       [priority(20), label(BASIC-BLOCK-26-TO-25)]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-6-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-log-6-spec.k
@@ -86,7 +86,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int ( 4 *Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) ) <=Int GAS_CELL  
+      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( ( Glog < SCHEDULE_CELL:Schedule > +Int ( Glogdata < SCHEDULE_CELL:Schedule > *Int W1:Int ) ) +Int ( 4 *Int Glogtopic < SCHEDULE_CELL:Schedule > ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL 
        andBool ( ( notBool STATIC_CELL:Bool )
                ))
       [priority(20), label(BASIC-BLOCK-26-TO-25)]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-mcopy-3-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-mcopy-3-spec.k
@@ -43,7 +43,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , maxInt ( W0:Int , W1:Int ) , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL 
+      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , maxInt ( W0:Int , W1:Int ) , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , maxInt ( W0:Int , W1:Int ) , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL
       [priority(20), label(BASIC-BLOCK-22-TO-21)]
     
     rule [BASIC-BLOCK-23-TO-13]: <kevm>
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-mstore-2-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-mstore-2-spec.k
@@ -43,7 +43,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , 32 ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int Gverylow < SCHEDULE_CELL:Schedule > ) ) ) <=Int GAS_CELL 
+      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , 32 ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int Gverylow < SCHEDULE_CELL:Schedule > ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , 32 ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL
       [priority(20), label(BASIC-BLOCK-22-TO-21)]
     
     rule [BASIC-BLOCK-23-TO-13]: <kevm>
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-return-2-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-return-2-spec.k
@@ -46,7 +46,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int Gzero < SCHEDULE_CELL:Schedule > ) ) ) <=Int GAS_CELL 
+      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int Gzero < SCHEDULE_CELL:Schedule > ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL
       [priority(20), label(BASIC-BLOCK-24-TO-23)]
     
     rule [BASIC-BLOCK-25-TO-14]: <kevm>
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-returndatacopy-3-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-returndatacopy-3-spec.k
@@ -121,7 +121,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  
+      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL 
        andBool ( ( W1:Int +Int W2:Int ) <=Int lengthBytes ( OUTPUT_CELL:Bytes )
                ))
       [priority(20), label(BASIC-BLOCK-38-TO-30)]
@@ -163,7 +163,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  
+      requires ( USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gverylow < SCHEDULE_CELL:Schedule > +Int ( Gcopy < SCHEDULE_CELL:Schedule > *Int ( W2:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL 
        andBool ( lengthBytes ( OUTPUT_CELL:Bytes ) <Int ( W1:Int +Int W2:Int )
                ))
       [priority(20), label(BASIC-BLOCK-39-TO-31)]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-revert-2-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-revert-2-spec.k
@@ -46,7 +46,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int Gzero < SCHEDULE_CELL:Schedule > ) ) ) <=Int GAS_CELL 
+      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int Gzero < SCHEDULE_CELL:Schedule > ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL
       [priority(20), label(BASIC-BLOCK-24-TO-23)]
     
     rule [BASIC-BLOCK-25-TO-15]: <kevm>
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-sha3-2-spec.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries/summary-sha3-2-spec.k
@@ -43,7 +43,7 @@ imports BUF
            </ethereum>
            ...
          </kevm>
-      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gsha3 < SCHEDULE_CELL:Schedule > +Int ( Gsha3word < SCHEDULE_CELL:Schedule > *Int ( W1:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL 
+      requires USEGAS_CELL:Bool  andBool ( ( ( ( ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) ) +Int ( Gsha3 < SCHEDULE_CELL:Schedule > +Int ( Gsha3word < SCHEDULE_CELL:Schedule > *Int ( W1:Int up/Int 32 ) ) ) ) ) ) <=Int GAS_CELL  andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL
       [priority(20), label(BASIC-BLOCK-24-TO-23)]
     
     rule [BASIC-BLOCK-25-TO-14]: <kevm>
diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py
@@ -628,7 +628,14 @@ def _remove_inf_gas(original_str: str) -> str:
                         continue
                     i += 1
                 gas_guard = f' andBool {gas_usage} <=Int GAS_CELL '
-                
+                if '( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) )' in gas_usage:
+                    gas_guard += ' andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL'
+                if '( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) )' in gas_usage:
+                    gas_guard += ' andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , W1:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL'
+                if '( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , maxInt ( W0:Int , W1:Int ) , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) )' in gas_usage:
+                    gas_guard += ' andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , maxInt ( W0:Int , W1:Int ) , W2:Int ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL'
+                if '( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , 32 ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) )' in gas_usage:
+                    gas_guard += ' andBool ( Cmem ( SCHEDULE_CELL:Schedule , #memoryUsageUpdate ( MEMORYUSED_CELL:Int , W0:Int , 32 ) ) -Int Cmem ( SCHEDULE_CELL:Schedule , MEMORYUSED_CELL:Int ) ) <=Int GAS_CELL'
                 # Find first requires USEGAS_CELL pattern
                 usegas_match = re.search(r'requires (\( )?USEGAS_CELL:Bool', left_str)
                 if not usegas_match:
diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
@@ -455,7 +455,6 @@ def test_prove_optimizations(
     for path in (REPO_ROOT / 'kevm-pyk/src/kevm_pyk/kproj/evm-semantics/summaries').glob('*.k') 
     if path.name != 'summary.k'
 ]
-# SUMMARY_MODULES = ['SUMMARY-RETURN-2-SPEC']
 
 
 @pytest.mark.parametrize(
diff --git a/tests/specs/opcodes/verification.k b/tests/specs/opcodes/verification.k
@@ -1,10 +1,11 @@
 requires "evm.md"
 requires "lemmas/int-simplification.k"
+requires "buf.md"
 
 module VERIFICATION
     imports EVM
     imports INT-SIMPLIFICATION
-
+    imports BUF
     rule #sizeWordStack(WS           , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0                [simplification]
     rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N)        requires I <Int #sizeWordStack(WS) [simplification]
     rule 0 <=Int #sizeWordStack(_ , 0)    => true                                                            [simplification]
