Datetime & node id in console logs

src/kontrol/foundry.py

@@ -45,6 +45,7 @@
 from .solc_to_k import Contract, _contract_name_from_bytecode
 from .storage_generation import generate_setup_contract
 from .utils import (
+    _DATETIME_FORMAT,
     _read_digest_file,
     decode_log_message,
     empty_lemmas_file_contents,
@@ -158,7 +159,9 @@ def _console_log_pattern(self) -> KSequence:
     def _ffi_pattern(self) -> KSequence:
         return KSequence([KApply('ffi_shell', KVariable('###CMD')), KVariable('###CONTINUATION')])
 
-    def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
+    def _exec_rename_custom_step(
+        self, subst: Subst, cterm: CTerm, _c: CTermSymbolic, _node_id: int
+    ) -> KCFGExtendResult | None:
         # Extract the target var and new name from the substitution
         target_var = subst['###RENAME_TARGET']
         name_token = subst['###NEW_NAME']
@@ -182,7 +185,7 @@ def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic
         return Step(CTerm(new_cterm.config, constraints), 1, (), ['foundry_rename'], cut=True)
 
     def _exec_forget_custom_step(
-        self, subst: Subst, cterm: CTerm, cterm_symbolic: CTermSymbolic
+        self, subst: Subst, cterm: CTerm, cterm_symbolic: CTermSymbolic, _node_id: int
     ) -> KCFGExtendResult | None:
         """Remove the constraint at the top of K_CELL of a given CTerm from its path constraints,
            as part of the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
@@ -293,28 +296,33 @@ def _filter_constraints_by_simplification(
         new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
         return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True)
 
-    def _exec_console_log_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
+    def _exec_console_log_custom_step(
+        self, subst: Subst, cterm: CTerm, _c: CTermSymbolic, node_id: int
+    ) -> KCFGExtendResult | None:
         selector_token = subst['###SELECTOR']
         data = subst['###DATA']
         assert type(selector_token) is KToken
 
+        prefix = f'    [{node_id}] [{datetime.datetime.now().strftime(_DATETIME_FORMAT)}]'
         try:
             if type(data) is KToken:
                 selector = int(selector_token.token)
                 output = decode_log_message(data.token, selector)
                 if output is not None:
-                    print(f'    {output}')
+                    print(f'{prefix} {output}')
             else:
                 kevm = KEVM(kdist.get('kontrol.base'))
-                print(f'    {kevm.pretty_print(data)}')
+                print(f'{prefix} {kevm.pretty_print(data)}')
         except Exception as e:
             _LOGGER.warning(f'Console log decode error: {e}')
 
         # Update the K_CELL with the continuation
         new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
         return Step(CTerm(new_cterm.config, cterm.constraints), 1, (), ['console.log'], cut=True)
 
-    def _exec_ffi_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -> KCFGExtendResult | None:
+    def _exec_ffi_custom_step(
+        self, subst: Subst, cterm: CTerm, _c: CTermSymbolic, _node_id: int
+    ) -> KCFGExtendResult | None:
         """Execute vm.ffi() cheatcode by running external commands and encoding their output as ABI bytes.
 
         This function decodes the command from the ABI-encoded string array, executes it as a subprocess, and processes

src/kontrol/utils.py

@@ -27,6 +27,7 @@
 
 _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
 _LOGGER: Final = logging.getLogger(__name__)
+_DATETIME_FORMAT: Final = '%Y-%m-%d %H:%M:%S'
 
 
 def ensure_name_is_unique(name: str, cterm: CTerm) -> str: