@@ -158,7 +158,13 @@ def _console_log_pattern(self) -> KSequence:
158158 def _ffi_pattern (self ) -> KSequence :
159159 return KSequence ([KApply ('ffi_shell' , KVariable ('###CMD' )), KVariable ('###CONTINUATION' )])
160160
161- def _exec_rename_custom_step (self , subst : Subst , cterm : CTerm , _c : CTermSymbolic ) -> KCFGExtendResult | None :
161+ def _exec_rename_custom_step (
162+ self ,
163+ subst : Subst ,
164+ cterm : CTerm ,
165+ _c : CTermSymbolic ,
166+ _node_id : int ,
167+ ) -> KCFGExtendResult | None :
162168 # Extract the target var and new name from the substitution
163169 target_var = subst ['###RENAME_TARGET' ]
164170 name_token = subst ['###NEW_NAME' ]
@@ -182,12 +188,17 @@ def _exec_rename_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic
182188 return Step (CTerm (new_cterm .config , constraints ), 1 , (), ['foundry_rename' ], cut = True )
183189
184190 def _exec_forget_custom_step (
185- self , subst : Subst , cterm : CTerm , cterm_symbolic : CTermSymbolic
191+ self ,
192+ subst : Subst ,
193+ cterm : CTerm ,
194+ cterm_symbolic : CTermSymbolic ,
195+ _node_id : int ,
186196 ) -> KCFGExtendResult | None :
187197 """Remove the constraint at the top of K_CELL of a given CTerm from its path constraints,
188198 as part of the 'FOUNDRY-ACCOUNTS.forget' cut-rule.
189199 :param cterm: CTerm representing a proof node
190200 :param cterm_symbolic: CTermSymbolic instance
201+ :param _node_id: Current node id (unused)
191202 :return: A Step of depth 1 carrying a new configuration in which the constraint is consumed from the top
192203 of the K cell and is removed from the initial path constraints if it existed, together with
193204 information that the `cheatcode_forget` rule has been applied.
@@ -293,7 +304,13 @@ def _filter_constraints_by_simplification(
293304 new_cterm = CTerm .from_kast (set_cell (cterm .kast , 'K_CELL' , KSequence (subst ['###CONTINUATION' ])))
294305 return Step (CTerm (new_cterm .config , new_constraints ), 1 , (), ['cheatcode_forget' ], cut = True )
295306
296- def _exec_console_log_custom_step (self , subst : Subst , cterm : CTerm , _c : CTermSymbolic ) -> KCFGExtendResult | None :
307+ def _exec_console_log_custom_step (
308+ self ,
309+ subst : Subst ,
310+ cterm : CTerm ,
311+ _c : CTermSymbolic ,
312+ _node_id : int ,
313+ ) -> KCFGExtendResult | None :
297314 selector_token = subst ['###SELECTOR' ]
298315 data = subst ['###DATA' ]
299316 assert type (selector_token ) is KToken
@@ -314,7 +331,13 @@ def _exec_console_log_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSym
314331 new_cterm = CTerm .from_kast (set_cell (cterm .kast , 'K_CELL' , KSequence (subst ['###CONTINUATION' ])))
315332 return Step (CTerm (new_cterm .config , cterm .constraints ), 1 , (), ['console.log' ], cut = True )
316333
317- def _exec_ffi_custom_step (self , subst : Subst , cterm : CTerm , _c : CTermSymbolic ) -> KCFGExtendResult | None :
334+ def _exec_ffi_custom_step (
335+ self ,
336+ subst : Subst ,
337+ cterm : CTerm ,
338+ _c : CTermSymbolic ,
339+ _node_id : int ,
340+ ) -> KCFGExtendResult | None :
318341 """Execute vm.ffi() cheatcode by running external commands and encoding their output as ABI bytes.
319342
320343 This function decodes the command from the ABI-encoded string array, executes it as a subprocess, and processes
@@ -325,6 +348,7 @@ def _exec_ffi_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic) -
325348 :param subst: Substitution containing the values obtained by matching the `self._ffi_pattern`.
326349 :param cterm: Current configuration term representing the EVM state.
327350 :param _c: Symbolic configuration term (unused).
351+ :param _node_id: Current node id (unused).
328352 :return: None if FFI is disabled. Otherwise, Step with OUTPUT_CELL set to ABI-encoded result and updated K_CELL
329353 continuation, tagged with 'kontrol.ffi.success'.
330354 """
0 commit comments