feat(access-control-prover): 9.3 summary caches and explicit exploration cutoffs

src/openultrasast/hunt/producers.py

@@ -15,8 +15,9 @@ from .. import mapping, source
 from ..model.taxonomy import DEFAULT_FAMILIES_PATH, load_families
 from ..preprocess import build_file_target, detect_language
 from ..semantic.facts import load_facts
-from ..semantic.ir import FileIR, parse_file
+from ..semantic.ir import FileIR, FunctionIR, parse_file
 from ..semantic.obligations import check_obligations, load_obligation_facts, resolution
+from ..semantic.obligations import summaries as summaries_module
 from ..semantic.obligations.dominance import OrderDominance
 from ..semantic.obligations.operations import covers, find_operations, valid_witness
 from .labels import label_rows
@@ -116,6 +117,20 @@ class Context:
             files.append((path, text, language))
         return resolution.SymbolIndex.build(files)
 
+    @cached_property
+    def summaries(self) -> tuple[summaries_module.FunctionSummary, ...]:
+        """Monotone function summaries over the product tree, computed once per change (Req 6.2)."""
+        functions_by_module: dict[str, list[FunctionIR]] = {}
+        for path in self.product_files:
+            try:
+                file_ir = self.ir(path)
+            except _Absent:
+                # Same guard as entry_points and symbol_index: an unreadable product file
+                # contributes no functions, not a failure of the summary cache.
+                continue
+            functions_by_module.setdefault(path, []).extend(file_ir.functions)
+        return summaries_module.monotone_summaries(functions_by_module, index=self.symbol_index)
+
     @cached_property
     def hunks(self) -> dict[str, list[list[int]]]:
         """Line ranges per file that the push changed or added, at head."""

src/openultrasast/semantic/obligations/summaries.py

@@ -5,18 +5,26 @@ operations, local witnesses, resolved calls and local completeness WITHOUT
 traversing callers. Task 9.2 (Reqs 3.7, 11.6): a monotone fixpoint over
 strongly connected call components unions callee evidence into callers until
 stable, so direct and mutual recursion terminate with the accumulated
-evidence. Summaries are deterministic and carry no target names beyond fact
-identifiers (Req 11.7).
+evidence. Task 9.3 (Reqs 3.8, 6.2, 6.3, 7.2): an exploration budget bounds
+the fixpoint; depth, fan-out and deadline cutoffs stop growth, record the
+exact cutoff reason and leave the affected summaries incomplete while
+preserving the evidence accumulated so far. Summaries are deterministic and
+carry no target names beyond fact identifiers (Req 11.7).
 """
 
 from collections.abc import Iterable, Iterator, Mapping
-from dataclasses import dataclass, field
+from dataclasses import dataclass, field, replace
+from time import monotonic
 
 from ..ir import FunctionIR
 from .abstract_domain import Completeness, join_completeness
 from .operations import Discharge, Operation
 from .resolution import CallTargetSet, SymbolId, SymbolIndex, resolve_call
 
+_DEPTH_CUTOFF = "summaries:depth_cutoff"
+_FAN_OUT_CUTOFF = "summaries:fan_out_cutoff"
+_DEADLINE_CUTOFF = "summaries:deadline_cutoff"
+
 
 @dataclass(frozen=True)
 class FunctionSummary:
@@ -29,6 +37,20 @@ class FunctionSummary:
     completeness: Completeness = field(default_factory=lambda: Completeness(is_complete=True))
 
 
+@dataclass(frozen=True)
+class ExplorationBudget:
+    """Work bounds for the summary fixpoint; ``None`` means unbounded.
+
+    Req 3.8: every bound that truncates exploration records its exact cutoff
+    reason and leaves affected summaries incomplete with the evidence
+    accumulated so far.
+    """
+
+    depth: int | None = None
+    fan_out: int | None = None
+    deadline: float | None = None
+
+
 def _enclosing_type(index: SymbolIndex, module: str, name: str) -> str | None:
     """Return the enclosing type of the function ``name`` declared in ``module``."""
     for symbol in index.by_name.get(name, ()):
@@ -245,22 +267,80 @@ def _propagated(summary: FunctionSummary, callees: Iterable[FunctionSummary]) ->
     )
 
 
+def _callees_for(
+    member_symbol: SymbolId,
+    edges: Mapping[SymbolId, tuple[SymbolId, ...]],
+    summaries_by_symbol: Mapping[SymbolId, FunctionSummary],
+    fan_out: int | None,
+) -> tuple[list[FunctionSummary], bool]:
+    """Resolve a member's exact callees, truncated to ``fan_out`` when set."""
+    callee_edges = [edge for edge in edges.get(member_symbol, ()) if edge in summaries_by_symbol]
+    truncated = fan_out is not None and len(callee_edges) > fan_out
+    if truncated:
+        callee_edges = callee_edges[:fan_out]
+    return [summaries_by_symbol[edge] for edge in callee_edges], truncated
+
+
+def _propagate_round(
+    members: tuple[FunctionSummary, ...],
+    summaries_by_symbol: dict[SymbolId, FunctionSummary],
+    edges: Mapping[SymbolId, tuple[SymbolId, ...]],
+    budget: ExplorationBudget,
+) -> bool:
+    """One union round over the component; returns whether anything changed."""
+    changed = False
+    for member in members:
+        current = summaries_by_symbol[member.symbol]
+        callees, truncated = _callees_for(member.symbol, edges, summaries_by_symbol, budget.fan_out)
+        propagated = _propagated(current, callees)
+        if truncated:
+            propagated = replace(
+                propagated,
+                completeness=join_completeness(
+                    propagated.completeness,
+                    Completeness(is_complete=False, reasons=(_FAN_OUT_CUTOFF,)),
+                ),
+            )
+        if propagated != current:
+            summaries_by_symbol[member.symbol] = propagated
+            changed = True
+    return changed
+
+
+def _apply_cutoff_reason(
+    members: tuple[FunctionSummary, ...],
+    summaries_by_symbol: dict[SymbolId, FunctionSummary],
+    reason: str,
+) -> None:
+    """Mark every member of a truncated component with the cutoff reason."""
+    for member in members:
+        current = summaries_by_symbol[member.symbol]
+        summaries_by_symbol[member.symbol] = replace(
+            current,
+            completeness=join_completeness(current.completeness, Completeness(is_complete=False, reasons=(reason,))),
+        )
+
+
 def _stabilise_component(
     members: tuple[FunctionSummary, ...],
     summaries_by_symbol: dict[SymbolId, FunctionSummary],
     edges: Mapping[SymbolId, tuple[SymbolId, ...]],
+    budget: ExplorationBudget,
 ) -> None:
-    """Iterate a component's members until every summary is stable."""
-    changed = True
-    while changed:
-        changed = False
-        for member in members:
-            current = summaries_by_symbol[member.symbol]
-            callees = [summaries_by_symbol[edge] for edge in edges.get(member.symbol, ()) if edge in summaries_by_symbol]
-            propagated = _propagated(current, callees)
-            if propagated != current:
-                summaries_by_symbol[member.symbol] = propagated
-                changed = True
+    """Iterate a component's members until stable or a budget bound fires."""
+    if not any(edges.get(member.symbol) for member in members):
+        return
+    rounds = 0
+    while True:
+        if budget.deadline is not None and monotonic() > budget.deadline:
+            _apply_cutoff_reason(members, summaries_by_symbol, _DEADLINE_CUTOFF)
+            return
+        if not _propagate_round(members, summaries_by_symbol, edges, budget):
+            return
+        rounds += 1
+        if budget.depth is not None and rounds >= budget.depth:
+            _apply_cutoff_reason(members, summaries_by_symbol, _DEPTH_CUTOFF)
+            return
 
 
 def monotone_summaries(
@@ -269,14 +349,18 @@ def monotone_summaries(
     *,
     operations_by_symbol: Mapping[SymbolId, tuple[Operation, ...]] | None = None,
     witnesses_by_symbol: Mapping[SymbolId, tuple[Discharge, ...]] | None = None,
+    budget: ExplorationBudget | None = None,
 ) -> tuple[FunctionSummary, ...]:
     """Summaries after the monotone fixpoint over strongly connected components.
 
     Local summaries first; then every component (callee components first) is
     iterated until union-stable, so recursion terminates with the accumulated
-    operations, witnesses and completeness reasons of its cycle. Output order
-    matches :func:`local_summaries`.
+    operations, witnesses and completeness reasons of its cycle. ``budget``
+    bounds the exploration (Req 3.8): a depth, fan-out or deadline cutoff
+    stops growth and leaves affected summaries incomplete with the exact
+    cutoff reason. Output order matches :func:`local_summaries`.
     """
+    bounded = budget if budget is not None else ExplorationBudget()
     local = local_summaries(
         functions_by_module,
         index,
@@ -287,5 +371,5 @@ def monotone_summaries(
     edges = _exact_caller_edges(summaries_by_symbol)
     for component in _sorted_scc_components(edges, summaries_by_symbol):
         members = tuple(summaries_by_symbol[member] for member in component)
-        _stabilise_component(members, summaries_by_symbol, edges)
+        _stabilise_component(members, summaries_by_symbol, edges, bounded)
     return tuple(summaries_by_symbol[summary.symbol] for summary in local)