Allow non-general init state for non-test functions

package/version

@@ -1 +1 @@
-0.1.172
+0.1.173

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.172"
+version = "0.1.173"
 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.172'
+VERSION: Final = '0.1.173'

src/kontrol/__main__.py

@@ -243,6 +243,7 @@ def exec_prove(
     maude_port: int | None = None,
     use_gas: bool = False,
     deployment_state_path: Path | None = None,
+    with_non_general_state: bool = False,
     **kwargs: Any,
 ) -> None:
     _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}')
@@ -279,6 +280,7 @@ def exec_prove(
         fail_fast=fail_fast,
         use_gas=use_gas,
         deployment_state_entries=deployment_state_entries,
+        active_symbolik=with_non_general_state,
     )
 
     rpc_options = RPCOptions(
@@ -797,6 +799,13 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
         action='append',
         help='Specify a summary to include as a lemma.',
     )
+    prove_args.add_argument(
+        '--with-non-general-state',
+        dest='with_non_general_state',
+        default=False,
+        action='store_true',
+        help='Flag used by Simbolik to initialise the state of a non test function as if it was a test function.',
+    )
 
     show_args = command_parser.add_parser(
         'show',

src/kontrol/options.py

@@ -31,6 +31,7 @@ class ProveOptions:
     reinit: bool
     use_gas: bool
     deployment_state_entries: Iterable[DeploymentStateEntry] | None
+    active_symbolik: bool
 
     def __init__(
         self,
@@ -53,6 +54,7 @@ def __init__(
         reinit: bool = False,
         use_gas: bool = False,
         deployment_state_entries: list[DeploymentStateEntry] | None = None,
+        active_symbolik: bool = False,
     ) -> None:
         object.__setattr__(self, 'auto_abstract_gas', auto_abstract_gas)
         object.__setattr__(self, 'bug_report', bug_report)
@@ -72,6 +74,7 @@ def __init__(
         object.__setattr__(self, 'reinit', reinit)
         object.__setattr__(self, 'use_gas', use_gas)
         object.__setattr__(self, 'deployment_state_entries', deployment_state_entries)
+        object.__setattr__(self, 'active_symbolik', active_symbolik)
 
 
 @dataclass(frozen=True)

src/kontrol/prove.py

@@ -227,6 +227,7 @@ def init_and_run_proof(test: FoundryTest) -> APRFailureInfo | None:
                 use_gas=prove_options.use_gas,
                 deployment_state_entries=prove_options.deployment_state_entries,
                 summary_ids=summary_ids,
+                active_symbolik=prove_options.active_symbolik,
             )
 
             cut_point_rules = KEVMSemantics.cut_point_rules(
@@ -282,6 +283,7 @@ def method_to_apr_proof(
     use_gas: bool = False,
     deployment_state_entries: Iterable[DeploymentStateEntry] | None = None,
     summary_ids: Iterable[str] = (),
+    active_symbolik: bool = False,
 ) -> APRProof:
     if Proof.proof_data_exists(test.id, foundry.proofs_dir):
         apr_proof = foundry.get_apr_proof(test.id)
@@ -305,6 +307,7 @@ def method_to_apr_proof(
         setup_proof=setup_proof,
         use_gas=use_gas,
         deployment_state_entries=deployment_state_entries,
+        active_symbolik=active_symbolik,
     )
 
     apr_proof = APRProof(
@@ -345,17 +348,13 @@ def _method_to_initialized_cfg(
     setup_proof: APRProof | None = None,
     use_gas: bool = False,
     deployment_state_entries: Iterable[DeploymentStateEntry] | None = None,
+    active_symbolik: bool = False,
 ) -> tuple[KCFG, int, int]:
     _LOGGER.info(f'Initializing KCFG for test: {test.id}')
 
     empty_config = foundry.kevm.definition.empty_config(GENERATED_TOP_CELL)
     kcfg, new_node_ids, init_node_id, target_node_id = _method_to_cfg(
-        empty_config,
-        test.contract,
-        test.method,
-        setup_proof,
-        use_gas,
-        deployment_state_entries,
+        empty_config, test.contract, test.method, setup_proof, use_gas, deployment_state_entries, active_symbolik
     )
 
     for node_id in new_node_ids:
@@ -386,6 +385,7 @@ def _method_to_cfg(
     setup_proof: APRProof | None,
     use_gas: bool,
     deployment_state_entries: Iterable[DeploymentStateEntry] | None,
+    active_symbolik: bool,
 ) -> tuple[KCFG, list[int], int, int]:
     calldata = None
     callvalue = None
@@ -408,6 +408,7 @@ def _method_to_cfg(
         calldata=calldata,
         callvalue=callvalue,
         is_constructor=isinstance(method, Contract.Constructor),
+        active_symbolik=active_symbolik,
     )
     new_node_ids = []
 
@@ -555,6 +556,7 @@ def _init_cterm(
     use_gas: bool,
     is_test: bool,
     is_setup: bool,
+    active_symbolik: bool,
     is_constructor: bool,
     *,
     calldata: KInner | None = None,
@@ -591,7 +593,7 @@ def _init_cterm(
         'MOCKCALLS_CELL': KApply('.MockCallCellMap'),
     }
 
-    if is_test or is_setup or is_constructor:
+    if is_test or is_setup or is_constructor or active_symbolik:
         init_account_list = _create_initial_account_list(program, deployment_state_entries)
         init_subst_test = {
             'OUTPUT_CELL': bytesToken(b''),