lint

src/halmos/__main__.py

@@ -61,6 +61,7 @@
     Path,
     SMTQuery,
     State,
+    StorageData,
     con_addr,
     jumpid_str,
     mnemonic,

src/halmos/cheatcodes.py

@@ -207,9 +207,9 @@ def symbolic_storage(ex, arg):
     account = uint160(arg.get_word(4))
 
     account_alias = account
-#   account_alias = sevm.resolve_address_alias(
-#       ex, account, stack, step_id, branching=False
-#   )
+    #   account_alias = sevm.resolve_address_alias(
+    #       ex, account, stack, step_id, branching=False
+    #   )
 
     ex.storage[account_alias].symbolic = True
 

src/halmos/sevm.py

@@ -760,7 +760,7 @@ def extend_path(self, path):
 @dataclass
 class StorageData:
     symbolic: bool = False
-    mapping: Dict = field(default_factory=dict)
+    mapping: dict = field(default_factory=dict)
 
 
 class Exec:  # an execution path
@@ -956,7 +956,9 @@ def check(self, cond: Any) -> Any:
 
         return self.path.check(cond)
 
-    def select(self, array: Any, key: Word, arrays: dict, symbolic: bool = False) -> Word:
+    def select(
+        self, array: Any, key: Word, arrays: dict, symbolic: bool = False
+    ) -> Word:
         if array in arrays:
             store = arrays[array]
             if store.decl().name() == "store" and store.num_args() == 3:
@@ -1180,7 +1182,10 @@ def load(cls, ex: Exec, addr: Any, loc: Word) -> Word:
                     Select(cls.empty(addr, slot, keys), concat(keys)) == ZERO
                 )
             return ex.select(
-                ex.storage[addr].mapping[slot][num_keys][size_keys], concat(keys), ex.storages, ex.storage[addr].symbolic
+                ex.storage[addr].mapping[slot][num_keys][size_keys],
+                concat(keys),
+                ex.storages,
+                ex.storage[addr].symbolic,
             )
 
     @classmethod
@@ -1293,7 +1298,12 @@ def load(cls, ex: Exec, addr: Any, loc: Word) -> Word:
         if not ex.storage[addr].symbolic:
             # generate emptyness axiom for each array index, instead of using quantified formula; see init()
             ex.path.append(Select(cls.empty(addr, loc), loc) == ZERO)
-        return ex.select(ex.storage[addr].mapping[loc.size()], loc, ex.storages, ex.storage[addr].symbolic)
+        return ex.select(
+            ex.storage[addr].mapping[loc.size()],
+            loc,
+            ex.storages,
+            ex.storage[addr].symbolic,
+        )
 
     @classmethod
     def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
@@ -2134,7 +2144,8 @@ def create(
 
         # setup new account
         ex.set_code(new_addr, Contract(b""))  # existing code must be empty
-        ex.storage[new_addr] = StorageData()  # existing storage may not be empty and reset here
+        # existing storage may not be empty and reset here
+        ex.storage[new_addr] = StorageData()
 
         # transfer value
         self.transfer_value(ex, pranked_caller, new_addr, value)
@@ -2526,7 +2537,12 @@ def finalize(ex: Exec):
                         or eq(account, console.address)
                     ):
                         # dummy arbitrary value, consistent with foundry
-                        codesize = 1 if eq(account, hevm_cheat_code.address) or eq(account, halmos_cheat_code.address) else 0
+                        codesize = (
+                            1
+                            if eq(account, hevm_cheat_code.address)
+                            or eq(account, halmos_cheat_code.address)
+                            else 0
+                        )
                     else:
                         codesize = 0
 

tests/test_config.py

@@ -159,9 +159,7 @@ def test_config_file_snake_case(config, toml_parser):
 
 def test_config_e2e(config, parser, toml_parser):
     # when we apply overrides to the default config
-    config_file_data = toml_parser.parse_str(
-        "[global]\nverbose = 42"
-    )
+    config_file_data = toml_parser.parse_str("[global]\nverbose = 42")
     config = config.with_overrides(source="halmos.toml", **config_file_data)
 
     args = parser.parse_args(["-vvv"])