Disable gas computations in Kontrol (#252)

* add suport for kevm nogas

* hardcode use-gas for profiling

* test

* Set Version: 0.1.100

* Set Version: 0.1.101

* set kevm version tag

* remove space

* set use_gas to false by default

* Revert "hardcode use-gas for profiling"

This reverts commit 0ba7b82.

* Set Version: 0.1.103

* remove duplicated  substitution

* update expected output

* use gas for GasTests

* Set Version: 0.1.104

* set init gas cells to 0

* update expected output for callData and refund cells

---------

Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>

Author: 4 people

package/version

@@ -1 +1 @@
-0.1.103
+0.1.104

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.103"
+version = "0.1.104"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.103'
+VERSION: Final = '0.1.104'

src/kontrol/__main__.py

@@ -229,6 +229,7 @@ def exec_prove(
     fail_fast: bool = False,
     port: int | None = None,
     maude_port: int | None = None,
+    use_gas: bool = False,
     **kwargs: Any,
 ) -> None:
     _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}')
@@ -258,6 +259,7 @@ def exec_prove(
         max_iterations=max_iterations,
         run_constructor=run_constructor,
         fail_fast=fail_fast,
+        use_gas=use_gas,
     )
 
     rpc_options = RPCOptions(
@@ -724,6 +726,9 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
         action='store_true',
         help='Include the contract constructor in the test execution.',
     )
+    prove_args.add_argument(
+        '--use-gas', dest='use_gas', default=False, action='store_true', help='Enables gas computation in KEVM.'
+    )
 
     show_args = command_parser.add_parser(
         'show',

src/kontrol/options.py

@@ -24,6 +24,7 @@ class ProveOptions:
     run_constructor: bool
     fail_fast: bool
     reinit: bool
+    use_gas: bool
 
     def __init__(
         self,
@@ -41,6 +42,7 @@ def __init__(
         run_constructor: bool = False,
         fail_fast: bool = True,
         reinit: bool = False,
+        use_gas: bool = False,
     ) -> None:
         object.__setattr__(self, 'auto_abstract_gas', auto_abstract_gas)
         object.__setattr__(self, 'bug_report', bug_report)
@@ -55,6 +57,7 @@ def __init__(
         object.__setattr__(self, 'run_constructor', run_constructor)
         object.__setattr__(self, 'fail_fast', fail_fast)
         object.__setattr__(self, 'reinit', reinit)
+        object.__setattr__(self, 'use_gas', use_gas)
 
 
 @dataclass(frozen=True)

src/kontrol/prove.py

@@ -204,6 +204,7 @@ def init_and_run_proof(test: FoundryTest) -> Proof:
                 kcfg_explore=kcfg_explore,
                 bmc_depth=prove_options.bmc_depth,
                 run_constructor=prove_options.run_constructor,
+                use_gas=prove_options.use_gas,
             )
 
             run_prover(
@@ -238,6 +239,7 @@ def method_to_apr_proof(
     kcfg_explore: KCFGExplore,
     bmc_depth: int | None = None,
     run_constructor: bool = False,
+    use_gas: bool = False,
 ) -> APRProof | APRBMCProof:
     if Proof.proof_data_exists(test.id, foundry.proofs_dir):
         apr_proof = foundry.get_apr_proof(test.id)
@@ -259,6 +261,7 @@ def method_to_apr_proof(
         test=test,
         kcfg_explore=kcfg_explore,
         setup_proof=setup_proof,
+        use_gas=use_gas,
     )
 
     if bmc_depth is not None:
@@ -299,6 +302,7 @@ def _method_to_initialized_cfg(
     kcfg_explore: KCFGExplore,
     *,
     setup_proof: APRProof | None = None,
+    use_gas: bool = False,
 ) -> tuple[KCFG, int, int]:
     _LOGGER.info(f'Initializing KCFG for test: {test.id}')
 
@@ -308,6 +312,7 @@ def _method_to_initialized_cfg(
         test.contract,
         test.method,
         setup_proof,
+        use_gas,
     )
 
     for node_id in new_node_ids:
@@ -336,6 +341,7 @@ def _method_to_cfg(
     contract: Contract,
     method: Contract.Method | Contract.Constructor,
     setup_proof: APRProof | None,
+    use_gas: bool,
 ) -> tuple[KCFG, list[int], int, int]:
     calldata = None
     callvalue = None
@@ -356,6 +362,7 @@ def _method_to_cfg(
         program=program,
         calldata=calldata,
         callvalue=callvalue,
+        use_gas=use_gas,
     )
     new_node_ids = []
 
@@ -417,6 +424,7 @@ def _init_cterm(
     empty_config: KInner,
     contract_name: str,
     program: KInner,
+    use_gas: bool,
     *,
     setup_cterm: CTerm | None = None,
     calldata: KInner | None = None,
@@ -432,8 +440,8 @@ def _init_cterm(
     )
     init_subst = {
         'MODE_CELL': KApply('NORMAL'),
+        'USEGAS_CELL': TRUE if use_gas else FALSE,
         'SCHEDULE_CELL': KApply('SHANGHAI_EVM'),
-        'USEGAS_CELL': TRUE,
         'STATUSCODE_CELL': KVariable('STATUSCODE'),
         'CALLSTACK_CELL': KApply('.List'),
         'CALLDEPTH_CELL': intToken(0),
@@ -487,6 +495,11 @@ def _init_cterm(
     if callvalue is not None:
         init_subst['CALLVALUE_CELL'] = callvalue
 
+    if not use_gas:
+        init_subst['GAS_CELL'] = intToken(0)
+        init_subst['CALLGAS_CELL'] = intToken(0)
+        init_subst['REFUND_CELL'] = intToken(0)
+
     init_term = Subst(init_subst)(empty_config)
     init_cterm = CTerm.from_kast(init_term)
     init_cterm = KEVM.add_invariant(init_cterm)

src/tests/integration/test-data/foundry-prove-with-gas

@@ -0,0 +1,8 @@
+GasTest.testInfiniteGas()
+GasTest.testSetGas()
+StoreTest.testGasLoadColdVM()
+StoreTest.testGasLoadWarmUp()
+StoreTest.testGasLoadWarmVM()
+StoreTest.testGasStoreColdVM()
+StoreTest.testGasStoreWarmUp()
+StoreTest.testGasStoreWarmVM()