Add option to omit enum constraints (#687)

* Add option to omit enum constraints, to allow duplicate enums in different parts of codebase

* Set Version: 0.1.350

* Remove extra find_enums call

* Set Version: 0.1.351

* Remove extra find_enums call

* Set Version: 0.1.353

* Set Version: 0.1.356

* Invert option

* Set Version: 0.1.359

* Fix inversion of option

* Update src/kontrol/foundry.py

Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

* Set Version: 0.1.360

* Update contracts.k.expected

* Fix test, fix dict lookup crash

* Fix option not being set in build step in tests

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

src/kontrol/__main__.py

@@ -90,9 +90,19 @@ def _ignore_arg(args: dict[str, Any], arg: str, cli_option: str) -> None:
         args.pop(arg)
 
 
-def _load_foundry(foundry_root: Path, bug_report: BugReport | None = None, use_hex_encoding: bool = False) -> Foundry:
+def _load_foundry(
+    foundry_root: Path,
+    bug_report: BugReport | None = None,
+    use_hex_encoding: bool = False,
+    add_enum_constraints: bool = False,
+) -> Foundry:
     try:
-        foundry = Foundry(foundry_root=foundry_root, bug_report=bug_report, use_hex_encoding=use_hex_encoding)
+        foundry = Foundry(
+            foundry_root=foundry_root,
+            bug_report=bug_report,
+            use_hex_encoding=use_hex_encoding,
+            add_enum_constraints=add_enum_constraints,
+        )
     except FileNotFoundError:
         print(
             f'File foundry.toml not found in: {str(foundry_root)!r}. Are you running kontrol in a Foundry project?',
@@ -156,7 +166,7 @@ def _compare_versions(ver1: KVersion, ver2: KVersion) -> bool:
 def exec_load_state(options: LoadStateOptions) -> None:
     foundry_state_load(
         options=options,
-        foundry=_load_foundry(options.foundry_root),
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
     )
 
 
@@ -183,7 +193,7 @@ def exec_build(options: BuildOptions) -> None:
         console.print(building_message)
         foundry_kompile(
             options=options,
-            foundry=_load_foundry(options.foundry_root),
+            foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
         )
         console.print(
             ':white_heavy_check_mark: [bold green]Success![/bold green] [bold]Kontrol project built[/bold] :muscle:'
@@ -210,7 +220,9 @@ def exec_prove(options: ProveOptions) -> None:
     try:
         console.print(proving_message)
         results = foundry_prove(
-            foundry=_load_foundry(options.foundry_root, options.bug_report),
+            foundry=_load_foundry(
+                options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints
+            ),
             options=options,
             recorded_state_entries=recorded_dump_entries if recorded_dump_entries else recorded_diff_entries,
         )
@@ -255,14 +267,18 @@ def exec_prove(options: ProveOptions) -> None:
 
 def exec_show(options: ShowOptions) -> None:
     output = foundry_show(
-        foundry=_load_foundry(options.foundry_root, use_hex_encoding=options.use_hex_encoding),
+        foundry=_load_foundry(
+            options.foundry_root,
+            use_hex_encoding=options.use_hex_encoding,
+            add_enum_constraints=options.enum_constraints,
+        ),
         options=options,
     )
     print(output)
 
 
 def exec_refute_node(options: RefuteNodeOptions) -> None:
-    foundry = _load_foundry(options.foundry_root)
+    foundry = _load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints)
     refutation = foundry_refute_node(foundry=foundry, options=options)
 
     if refutation:
@@ -276,31 +292,34 @@ def exec_refute_node(options: RefuteNodeOptions) -> None:
 
 def exec_unrefute_node(options: UnrefuteNodeOptions) -> None:
     foundry_unrefute_node(
-        foundry=_load_foundry(options.foundry_root),
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
         options=options,
     )
 
 
 def exec_split_node(options: SplitNodeOptions) -> None:
     node_ids = foundry_split_node(
-        foundry=_load_foundry(options.foundry_root),
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
         options=options,
     )
 
     print(f'Node {options.node} has been split into {node_ids} on condition {options.branch_condition}.')
 
 
 def exec_to_dot(options: ToDotOptions) -> None:
-    foundry_to_dot(foundry=_load_foundry(options.foundry_root), options=options)
+    foundry_to_dot(
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
+        options=options,
+    )
 
 
 def exec_list(options: ListOptions) -> None:
-    stats = foundry_list(foundry=_load_foundry(options.foundry_root))
+    stats = foundry_list(foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints))
     print('\n'.join(stats))
 
 
 def exec_view_kcfg(options: ViewKcfgOptions) -> None:
-    foundry = _load_foundry(options.foundry_root, use_hex_encoding=True)
+    foundry = _load_foundry(options.foundry_root, use_hex_encoding=True, add_enum_constraints=options.enum_constraints)
     test_id = foundry.get_test_id(options.test, options.version)
     contract_name, _ = test_id.split('.')
     proof = foundry.get_apr_proof(test_id)
@@ -317,51 +336,54 @@ def _custom_view(elem: KCFGElem) -> Iterable[str]:
 
 
 def exec_minimize_proof(options: MinimizeProofOptions) -> None:
-    foundry_minimize_proof(foundry=_load_foundry(options.foundry_root), options=options)
+    foundry_minimize_proof(
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
+        options=options,
+    )
 
 
 def exec_remove_node(options: RemoveNodeOptions) -> None:
     foundry_remove_node(
-        foundry=_load_foundry(options.foundry_root),
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
         options=options,
     )
 
 
 def exec_simplify_node(options: SimplifyNodeOptions) -> None:
 
     pretty_term = foundry_simplify_node(
-        foundry=_load_foundry(options.foundry_root, options.bug_report),
+        foundry=_load_foundry(options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints),
         options=options,
     )
     print(f'Simplified:\n{pretty_term}')
 
 
 def exec_step_node(options: StepNodeOptions) -> None:
     foundry_step_node(
-        foundry=_load_foundry(options.foundry_root, options.bug_report),
+        foundry=_load_foundry(options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints),
         options=options,
     )
 
 
 def exec_merge_nodes(options: MergeNodesOptions) -> None:
     foundry_merge_nodes(
-        foundry=_load_foundry(options.foundry_root),
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
         options=options,
     )
 
 
 def exec_section_edge(options: SectionEdgeOptions) -> None:
 
     foundry_section_edge(
-        foundry=_load_foundry(options.foundry_root, options.bug_report),
+        foundry=_load_foundry(options.foundry_root, options.bug_report, add_enum_constraints=options.enum_constraints),
         options=options,
     )
 
 
 def exec_get_model(options: GetModelOptions) -> None:
 
     output = foundry_get_model(
-        foundry=_load_foundry(options.foundry_root),
+        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
         options=options,
     )
     print(output)

src/kontrol/cli.py

@@ -168,6 +168,13 @@ def foundry_args(self) -> ArgumentParser:
             type=dir_path,
             help='Path to Foundry project root directory.',
         )
+        args.add_argument(
+            '--enum-constraints',
+            dest='enum_constraints',
+            default=None,
+            action='store_true',
+            help='Add constraints for enum function arguments and storage slots.',
+        )
         return args
 
     @cached_property

src/kontrol/foundry.py

@@ -80,6 +80,8 @@ class Foundry:
     _toml: dict[str, Any]
     _bug_report: BugReport | None
     _use_hex_encoding: bool
+
+    add_enum_constraints: bool
     enums: dict[str, int]
 
     class Sorts:
@@ -90,12 +92,14 @@ def __init__(
         foundry_root: Path,
         bug_report: BugReport | None = None,
         use_hex_encoding: bool = False,
+        add_enum_constraints: bool = False,
     ) -> None:
         self._root = foundry_root
         with (foundry_root / 'foundry.toml').open('rb') as f:
             self._toml = tomlkit.load(f)
         self._bug_report = bug_report
         self._use_hex_encoding = use_hex_encoding
+        self.add_enum_constraints = add_enum_constraints
         self.enums = {}
 
     def lookup_full_contract_name(self, contract_name: str) -> str:
@@ -177,7 +181,7 @@ def find_enums(dct: dict) -> None:
                     enum_max = len([member['name'] for member in dct['members']])
                     if enum_name in self.enums and enum_max != self.enums[enum_name]:
                         raise ValueError(
-                            f'enum name conflict: {enum_name} exists more than once in the codebase with a different size, which is not supported.'
+                            f'enum name conflict: {enum_name} exists more than once in the codebase with a different size, which is not supported with --enum-constraints.'
                         )
                     self.enums[enum_name] = len([member['name'] for member in dct['members']])
                 for node in dct['nodes']:
@@ -187,12 +191,14 @@ def find_enums(dct: dict) -> None:
             contract_name = json_path.split('/')[-1]
             contract_json = json.loads(Path(json_path).read_text())
             contract_name = contract_name[0:-5] if contract_name.endswith('.json') else contract_name
+            contract = Contract(contract_name, contract_json, foundry=True)
+            if self.add_enum_constraints:
+                find_enums(contract_json['ast'])
             try:
                 contract = Contract(contract_name, contract_json, foundry=True)
             except KeyError:
                 _LOGGER.warning(f'Skipping non-compatible JSON file for contract: {contract_name} at {json_path}.')
                 continue
-            find_enums(contract_json['ast'])
 
             _contracts[contract.name_with_path] = contract  # noqa: B909
 

src/kontrol/options.py

@@ -26,11 +26,13 @@ class ConfigType(Enum):
 
 class FoundryOptions(Options):
     foundry_root: Path
+    enum_constraints: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
         return {
             'foundry_root': Path('.'),
+            'enum_constraints': False,
         }
 
     @staticmethod

src/kontrol/prove.py

@@ -1068,15 +1068,20 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner:
         field_name = contract_name + '_' + field.label.upper()
         if field.data_type.startswith('enum'):
             enum_name = field.data_type.split(' ')[1]
-            enum_max = foundry.enums[enum_name]
-            new_account_constraints.append(
-                mlEqualsTrue(
-                    ltInt(
-                        KEVM.lookup(storage_map, intToken(field.slot)),
-                        intToken(enum_max),
+            if enum_name not in foundry.enums:
+                _LOGGER.warning(
+                    f'Skipping adding constraint for {enum_name} because it is not tracked by kontrol. It can be automatically constrained to its possible values by adding --enum-constraints.'
+                )
+            else:
+                enum_max = foundry.enums[enum_name]
+                new_account_constraints.append(
+                    mlEqualsTrue(
+                        ltInt(
+                            KEVM.lookup(storage_map, intToken(field.slot)),
+                            intToken(enum_max),
+                        )
                     )
                 )
-            )
         # Processing of strings
         if field.data_type == 'string':
             string_contents = KVariable(field_name + '_S_CONTENTS', sort=KSort('Bytes'))

src/kontrol/solc_to_k.py

@@ -464,13 +464,18 @@ def encoded_args(self, enums: dict[str, int]) -> tuple[KInner, list[KInner]]:
                     type_constraints.append(rp)
                 if input.internal_type is not None and input.internal_type.startswith('enum '):
                     enum_name = input.internal_type.split(' ')[1]
-                    enum_max = enums[enum_name]
-                    type_constraints.append(
-                        ltInt(
-                            KVariable(input.arg_name),
-                            intToken(enum_max),
+                    if enum_name not in enums:
+                        _LOGGER.warning(
+                            f'Skipping adding constraint for {enum_name} because it is not tracked by kontrol. It can be automatically constrained to its possible values by adding --enum-constraints.'
+                        )
+                    else:
+                        enum_max = enums[enum_name]
+                        type_constraints.append(
+                            ltInt(
+                                KVariable(input.arg_name),
+                                intToken(enum_max),
+                            )
                         )
-                    )
             encoded_args = KApply('encodeArgs', [KEVM.typed_args(args)])
             return encoded_args, type_constraints
 
@@ -698,13 +703,18 @@ def rule(
                     conjuncts.append(rp)
                 if input.internal_type is not None and input.internal_type.startswith('enum '):
                     enum_name = input.internal_type.split(' ')[1]
-                    enum_max = enums[enum_name]
-                    conjuncts.append(
-                        ltInt(
-                            KVariable(input.arg_name),
-                            intToken(enum_max),
+                    if enum_name not in enums:
+                        _LOGGER.warning(
+                            f'Skipping adding constraint for {enum_name} because it is not tracked by kontrol. It can be automatically constrained to its possible values by adding --enum-constraints.'
+                        )
+                    else:
+                        enum_max = enums[enum_name]
+                        conjuncts.append(
+                            ltInt(
+                                KVariable(input.arg_name),
+                                intToken(enum_max),
+                            )
                         )
-                    )
             lhs = KApply(application_label, [contract, KApply(prod_klabel, arg_vars)])
             rhs = KEVM.abi_calldata(self.name, args)
             ensures = andBool(conjuncts)

src/tests/integration/conftest.py

@@ -54,7 +54,7 @@ def server(foundry: Foundry, no_use_booster: bool) -> Iterator[KoreServer]:
 @pytest.fixture(scope='session')
 def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, worker_id: str) -> Foundry:
     if foundry_root_dir:
-        return Foundry(foundry_root_dir)
+        return Foundry(foundry_root_dir, add_enum_constraints=True)
 
     if worker_id == 'master':
         root_tmp_dir = tmp_path_factory.getbasetemp()
@@ -90,11 +90,12 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
                             'PortalTest:PAUSABILITY-LEMMAS',
                             'ImmutableVarsTest:SYMBOLIC-BYTES-LEMMAS',
                         ],
+                        'enum_constraints': True,
                     }
                 ),
-                foundry=Foundry(foundry_root),
+                foundry=Foundry(foundry_root, add_enum_constraints=True),
             )
 
     session_foundry_root = tmp_path_factory.mktemp('foundry')
     copy_tree(str(foundry_root), str(session_foundry_root))
-    return Foundry(session_foundry_root)
+    return Foundry(session_foundry_root, add_enum_constraints=True)

src/tests/integration/test_kontrol_cse.py

@@ -69,6 +69,7 @@ def test_foundry_dependency_automated(
                 'config_type': config_type,
                 'run_constructor': run_constructor,
                 'force_sequential': force_sequential,
+                'enum_constraints': True,
             }
         ),
     )