Update balance summaries to ensure GAS_CELL is greater 0.

Author: Stevengre

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

@@ -110,8 +110,9 @@ module BALANCE-NORMAL-SUMMARY
       requires ( USEGAS_CELL:Bool
        andBool ( Ghasaccesslist << SCHEDULE_CELL:Schedule >>
        andBool ( #if ( W0:Int modInt pow160 ) in ACCESSEDACCOUNTS_CELL:Set #then Gwarmstorageread < SCHEDULE_CELL:Schedule > #else Gcoldaccountaccess < SCHEDULE_CELL:Schedule > #fi <=Int GAS_CELL:Int
+       andBool ( 0 <=Int GAS_CELL:Int
        andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
-               ))))
+               )))))
       [priority(20), label(BALANCE-NORMAL-SUMMARY-USEGAS-BERLIN)]
 
     rule [BALANCE-NORMAL-SUMMARY-USEGAS]: <kevm>

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

@@ -110,8 +110,9 @@ module BALANCE-OWISE-SUMMARY
       requires ( USEGAS_CELL:Bool
        andBool ( Ghasaccesslist << SCHEDULE_CELL:Schedule >>
        andBool ( #if ( W0:Int modInt pow160 ) in ACCESSEDACCOUNTS_CELL:Set #then Gwarmstorageread < SCHEDULE_CELL:Schedule > #else Gcoldaccountaccess < SCHEDULE_CELL:Schedule > #fi <=Int GAS_CELL:Int
+       andBool ( 0 <=Int GAS_CELL:Int
        andBool ( ( W0:Int modInt pow160 ) ==Int ACCTID:Int
-               ))))
+               )))))
       [priority(20), label(BALANCE-OWISE-SUMMARY-USEGAS-BERLIN)]
 
     rule [BALANCE-OWISE-SUMMARY-USEGAS]: <kevm>

kevm-pyk/src/kevm_pyk/summarizer.py

@@ -499,7 +499,7 @@ def _transform_inf_gas_aux(inner: KInner) -> KInner:
             ]
         )
 
-    if rule_id in ['BALANCE-NORMAL-SUMMARY-BERLIN', 'BALANCE-OWISE-SUMMARY-BERLIN']:
+    if rule_id in ['BALANCE-NORMAL-SUMMARY-USEGAS-BERLIN', 'BALANCE-OWISE-SUMMARY-USEGAS-BERLIN']:
         requires = andBool([requires, leInt(KToken('0', 'Int'), KVariable('GAS_CELL', 'Int'))])
 
     return body, requires