Fix automatic gas abstraction re-applying (#1923)

* Fix automatic gas abstraction applying to nodes that were already abstracted * Fix automatic gas abstraction applying to nodes that were already abstracted * Set Version: 1.0.218 * Set Version: 1.0.219 * Add golden file test for automatic infinite gas abstraction option * Formatting * Set Version: 1.0.220 * Update kevm-pyk/src/kevm_pyk/kevm.py Co-authored-by: Everett Hildenbrandt <[email protected]> * Update kevm-pyk/src/tests/integration/test_foundry_prove.py Co-authored-by: Everett Hildenbrandt <[email protected]> * Fix formatting * Set Version: 1.0.221 * Update kevm-pyk/src/kevm_pyk/kevm.py Co-authored-by: Everett Hildenbrandt <[email protected]> * Set Version: 1.0.221 * Update expected file * Set Version: 1.0.223 * Set Version: 1.0.224 * Set Version: 1.0.225 * Set Version: 1.0.226 * Update expected output * Set Version: 1.0.228 * Set Version: 1.0.229 * Set Version: 1.0.230 * Set Version: 1.0.231 * Change k version * Set Version: 1.0.232 * Revert k release update * Set Version: 1.0.235 * Update expected output --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Jul 19, 2023 · 7276704 · 7276704
1 parent 287b659
commit 7276704
Show file tree

Hide file tree

Showing 6 changed files with 1,504 additions and 6 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.234"
+version = "1.0.235"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -380,11 +380,16 @@ def _replace(term: KInner) -> KInner:
             if type(term) is KApply and term.label.name == '<gas>':
                 gas_term = term.args[0]
                 if type(gas_term) is KApply and gas_term.label.name == 'infGas':
-                    result = KApply('<gas>', KApply('infGas', abstract_term_safely(term)))
-                    return result
+                    if type(gas_term.args[0]) is KVariable:
+                        return term
+                    return KApply(
+                        '<gas>', KApply('infGas', abstract_term_safely(term, base_name='VGAS', sort=KSort('Int')))
+                    )
                 return term
             elif type(term) is KApply and term.label.name == '<refund>':
-                return KApply('<refund>', KVariable('ABSTRACTED_REFUND', KSort('Int')))
+                if type(term.args[0]) is KVariable:
+                    return term
+                return KApply('<refund>', abstract_term_safely(term, base_name='VREFUND', sort=KSort('Int')))
             else:
                 return term