Skip loading circularity module for non-circularity proofs (#4860)

Some proofs we're loading are quite large in terms of the configuration
and the unevaluated functions in it. They end up taking a long time to
load the circularity module dynamically into the backend, even though it
won't be used.

This simply skips loading the circularities module for proofs that are
not marked as circularities. It should not affect the functionality of
the prover at all, and if it does it's likely a bug where we're using
the circularities module in a place we shouldn't.

This does mean, that for the pyk prover, circularities _must_ be marked
as such (like the sum-spec.k which is marked as such here), otherwise
they won't be included automatically as an axiom.

Author: ehildenb

pyk/regression-new/kprove-haskell/sum-spec.k

@@ -13,4 +13,5 @@ module SUM-SPEC
       N >=Int 0
     ensures
       ?S ==Int S +Int N *Int C +Int (N -Int 1) *Int N /Int 2
+    [circularity]
 endmodule

pyk/src/pyk/proof/reachability.py

@@ -188,7 +188,9 @@ def get_steps(self) -> list[APRProofStep]:
                         shortest_path.append(succ.source)
 
             nonzero_depth = self.nonzero_depth(node)
-            module_name = self.circularities_module_name if nonzero_depth else self.dependencies_module_name
+            module_name = (
+                self.circularities_module_name if nonzero_depth and self.circularity else self.dependencies_module_name
+            )
 
             predecessor_edges = self.kcfg.edges(target_id=node.id)
             predecessor_node_id: NodeIdLike | None = (
@@ -773,10 +775,11 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRule]) -
             if isinstance(subproof, APRProof)
             for rule in subproof.as_rules(priority=20, direct_rule=self.direct_subproof_rules)
         ]
-        circularity_rule = proof.as_rule(priority=20)
-
         _inject_module(proof.dependencies_module_name, main_module_name, dependencies_as_rules)
-        _inject_module(proof.circularities_module_name, proof.dependencies_module_name, [circularity_rule])
+
+        if proof.circularity:
+            circularity_rule = proof.as_rule(priority=20)
+            _inject_module(proof.circularities_module_name, proof.dependencies_module_name, [circularity_rule])
 
         for node_id in [proof.init, proof.target]:
             if self.kcfg_explore.kcfg_semantics.is_terminal(proof.kcfg.node(node_id).cterm):