Merge master into branch

package/version

@@ -1 +1 @@
-0.1.353
+0.1.367

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.353"
+version = "0.1.367"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kontrol/__init__.py

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

src/kontrol/prove.py

@@ -462,19 +462,19 @@ def create_kcfg_explore() -> KCFGExplore:
                     rule.label for rule in foundry.kevm.definition.all_modules_dict['KONTROL-ASSERTIONS'].rules
                 )
 
-            def create_apr_prover() -> APRProver:
-                return KontrolAPRProver(
-                    create_kcfg_explore(),
-                    accounts=['abc', 'def', 'ghi'],
-                    execute_depth=options.max_depth,
-                    terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step),
-                    cut_point_rules=cut_point_rules,
-                    counterexample_info=options.counterexample_info,
-                )
+#              def create_apr_prover() -> APRProver:
+#                  return KontrolAPRProver(
+#                      create_kcfg_explore(),
+#                      accounts=['abc', 'def', 'ghi'],
+#                      execute_depth=options.max_depth,
+#                      terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step),
+#                      cut_point_rules=cut_point_rules,
+#                      counterexample_info=options.counterexample_info,
+#                  )
             run_prover(
                 proof,
                 create_kcfg_explore=create_kcfg_explore,
-                create_apr_prover=create_apr_prover,
+#                  create_apr_prover=create_apr_prover,
                 max_depth=options.max_depth,
                 max_iterations=options.max_iterations,
                 cut_point_rules=cut_point_rules,
@@ -1131,9 +1131,9 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner:
 
     for field in storage_fields:
 
-        for constraint in field.data_type.compute_constraints(storage_map):
-            new_account_constraints.append(constraint)
-            print(constraint)
+#          for constraint in field.data_type.compute_constraints(storage_map):
+#              new_account_constraints.append(constraint)
+#              print(constraint)
 #              print(field.data_type.slot_vars())
 
 #          if isinstance(field.data_type, StorageFieldMappingType):
@@ -1142,12 +1142,18 @@ def extend_storage(map: KInner, slot: int, value: KInner) -> KInner:
         field_name = contract_name + '_' + field.label.upper()
         if field.data_type.name.startswith('enum'):
             enum_name = field.data_type.name.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