From c13fd74b08b4a2b98cae9609e2e89e72e436d322 Mon Sep 17 00:00:00 2001 From: Julian Kuners Date: Fri, 27 Mar 2026 13:11:51 +0100 Subject: [PATCH 1/3] add datetime to printed console logs --- src/kontrol/foundry.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 5ebd4e314..8320d713f 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -84,6 +84,7 @@ ) _LOGGER: Final = logging.getLogger(__name__) +_CONSOLE_LOG_DATETIME_FORMAT: Final = '%Y-%m-%d %H:%M:%S' class KontrolSemantics(KEVMSemantics): @@ -303,10 +304,12 @@ def _exec_console_log_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSym selector = int(selector_token.token) output = decode_log_message(data.token, selector) if output is not None: - print(f' {output}') + print(f' [{datetime.datetime.now().strftime(_CONSOLE_LOG_DATETIME_FORMAT)}] {output}') else: kevm = KEVM(kdist.get('kontrol.base')) - print(f' {kevm.pretty_print(data)}') + print( + f' [{datetime.datetime.now().strftime(_CONSOLE_LOG_DATETIME_FORMAT)}] {kevm.pretty_print(data)}' + ) except Exception as e: _LOGGER.warning(f'Console log decode error: {e}') From 840ab8e245e4fe5b6f4868a318828ec0120ac143 Mon Sep 17 00:00:00 2001 From: Julian Kuners Date: Wed, 8 Apr 2026 10:26:30 +0200 Subject: [PATCH 2/3] print node id in console logs --- src/kontrol/foundry.py | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 8320d713f..d99d5db5c 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -159,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'] @@ -183,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. @@ -294,22 +296,23 @@ 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(_CONSOLE_LOG_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' [{datetime.datetime.now().strftime(_CONSOLE_LOG_DATETIME_FORMAT)}] {output}') + print(f'{prefix} {output}') else: kevm = KEVM(kdist.get('kontrol.base')) - print( - f' [{datetime.datetime.now().strftime(_CONSOLE_LOG_DATETIME_FORMAT)}] {kevm.pretty_print(data)}' - ) + print(f'{prefix} {kevm.pretty_print(data)}') except Exception as e: _LOGGER.warning(f'Console log decode error: {e}') @@ -317,7 +320,9 @@ def _exec_console_log_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSym 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 From 5341353d4b2cbf8a677ec4527fa8f85d90e36190 Mon Sep 17 00:00:00 2001 From: Julian Kuners Date: Thu, 9 Apr 2026 12:08:04 +0200 Subject: [PATCH 3/3] move `_DATETIME_FORMAT` to `utils.py` --- src/kontrol/foundry.py | 4 ++-- src/kontrol/utils.py | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index d99d5db5c..dd436edc1 100644 --- a/src/kontrol/foundry.py +++ b/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, @@ -84,7 +85,6 @@ ) _LOGGER: Final = logging.getLogger(__name__) -_CONSOLE_LOG_DATETIME_FORMAT: Final = '%Y-%m-%d %H:%M:%S' class KontrolSemantics(KEVMSemantics): @@ -303,7 +303,7 @@ def _exec_console_log_custom_step( data = subst['###DATA'] assert type(selector_token) is KToken - prefix = f' [{node_id}] [{datetime.datetime.now().strftime(_CONSOLE_LOG_DATETIME_FORMAT)}]' + prefix = f' [{node_id}] [{datetime.datetime.now().strftime(_DATETIME_FORMAT)}]' try: if type(data) is KToken: selector = int(selector_token.token) diff --git a/src/kontrol/utils.py b/src/kontrol/utils.py index 74612da3e..f88ee0226 100644 --- a/src/kontrol/utils.py +++ b/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: