rename FOUNDRYSemantics to KontrolSemantics

runtimeverification · Dec 5, 2024 · 88de162 · 88de162
1 parent ae0ceb0
commit 88de162
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 12 deletions.
diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
@@ -94,7 +94,7 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-class FOUNDRYSemantics(KEVMSemantics):
+class KontrolSemantics(KEVMSemantics):
 
     def _check_forget_pattern(self, cterm: CTerm) -> bool:
         """Given a CTerm, check if the rule 'FOUNDRY-ACCOUNTS.forget' is at the top of the K_CELL.
@@ -922,7 +922,7 @@ def foundry_show(
     if options.failure_info:
         with legacy_explore(
             foundry.kevm,
-            kcfg_semantics=FOUNDRYSemantics(),
+            kcfg_semantics=KontrolSemantics(),
             id=test_id,
             smt_timeout=options.smt_timeout,
             smt_retry_limit=options.smt_retry_limit,
@@ -989,7 +989,7 @@ def _collect_klabel(_k: KInner) -> None:
         ]
         sentences = [sent for sent in sentences if not _contains_foundry_klabel(sent.body)]
         sentences = [
-            sent for sent in sentences if not FOUNDRYSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body)))
+            sent for sent in sentences if not KontrolSemantics().is_terminal(CTerm.from_kast(extract_lhs(sent.body)))
         ]
         if len(sentences) == 0:
             _LOGGER.warning(f'No claims or rules retained for proof {proof.id}')
@@ -1179,7 +1179,7 @@ def foundry_simplify_node(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1227,7 +1227,7 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
     check_cells_ne = [check_cell for check_cell in check_cells if not check_cells_equal(check_cell, nodes)]
 
     if check_cells_ne:
-        if not all(FOUNDRYSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes):
+        if not all(KontrolSemantics().same_loop(nodes[0].cterm, nd.cterm) for nd in nodes):
             raise ValueError(f'Nodes {options.nodes} cannot be merged because they differ in: {check_cells_ne}')
 
     anti_unification = nodes[0].cterm
@@ -1267,7 +1267,7 @@ def foundry_step_node(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1343,7 +1343,7 @@ def foundry_section_edge(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=apr_proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,
@@ -1394,7 +1394,7 @@ def foundry_get_model(
 
     with legacy_explore(
         foundry.kevm,
-        kcfg_semantics=FOUNDRYSemantics(),
+        kcfg_semantics=KontrolSemantics(),
         id=proof.id,
         bug_report=options.bug_report,
         kore_rpc_command=kore_rpc_command,

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -35,7 +35,7 @@
 from pyk.utils import hash_str, run_process_2, single, unique
 from rich.progress import Progress, SpinnerColumn, TaskID, TextColumn, TimeElapsedColumn
 
-from .foundry import Foundry, FOUNDRYSemantics, foundry_to_xml
+from .foundry import Foundry, KontrolSemantics, foundry_to_xml
 from .hevm import Hevm
 from .options import ConfigType, TraceOptions
 from .solc_to_k import Contract, hex_string_to_int
@@ -381,7 +381,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 )
                 return KCFGExplore(
                     cterm_symbolic,
-                    kcfg_semantics=FOUNDRYSemantics(auto_abstract_gas=options.auto_abstract_gas),
+                    kcfg_semantics=KontrolSemantics(auto_abstract_gas=options.auto_abstract_gas),
                     id=test.id,
                 )
 
@@ -425,7 +425,7 @@ def create_kcfg_explore() -> KCFGExplore:
                         }
                     ),
                 )
-            cut_point_rules = FOUNDRYSemantics.cut_point_rules(
+            cut_point_rules = KontrolSemantics.cut_point_rules(
                 options.break_on_jumpi,
                 options.break_on_jump,
                 options.break_on_calls,
@@ -467,7 +467,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 max_depth=options.max_depth,
                 max_iterations=options.max_iterations,
                 cut_point_rules=cut_point_rules,
-                terminal_rules=FOUNDRYSemantics.terminal_rules(options.break_every_step),
+                terminal_rules=KontrolSemantics.terminal_rules(options.break_every_step),
                 counterexample_info=options.counterexample_info,
                 max_frontier_parallel=options.max_frontier_parallel,
                 fail_fast=options.fail_fast,