feat(access-control-prover): 10.1 abstract dominance relations without prover fallback

.kiro/specs/access-control-prover/tasks.md

@@ -165,7 +165,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with
   - _Depends: 9.3_
 
 - [ ] 10. Strict authorization judgment
-- [ ] 10.1 Return abstract dominance relations without prover fallback
+- [x] 10.1 Return abstract dominance relations without prover fallback
   - Return MUST, MAY, NO or UNKNOWN with guard effect and control context.
   - Keep legacy order dominance unchanged, but return UNKNOWN in prover mode for unavailable graphs or line mappings.
   - Done when no prover fixture is discharged or flagged solely through textual-order fallback.

src/openultrasast/semantic/obligations/cfg_dominance.py

@@ -16,9 +16,11 @@ from __future__ import annotations
 
 import re
 from collections.abc import Mapping, Sequence
+from dataclasses import dataclass
 from typing import Any
 
 from ..cfg import ControlContext, FunctionCfg
+from .abstract_domain import EvidenceRelation
 from .dominance import Dominance, OrderDominance
 from .operations import Discharge, Operation
 
@@ -31,6 +33,15 @@ _EXIT_LINE = re.compile(r"^\s*(?P<word>return\b|raise\b|throw\b|abort\(|sys\.exi
 CfgEntry = FunctionCfg | Sequence[FunctionCfg] | None
 
 
+@dataclass(frozen=True)
+class DominanceEvidence:
+    """The strict dominance answer for prover mode: a relation, the guard's failure effect, and a reason when unknown."""
+
+    relation: EvidenceRelation
+    guard_effect: str | None = None
+    reason: str | None = None
+
+
 class CfgDominance:
     """Dominance over control-flow graphs keyed by (path, function), with order as the recorded fallback."""
 
@@ -83,6 +94,36 @@ class CfgDominance:
             return False
         return cfg.effect(witness.line, operation.line, throwing=witness.kind in _THROWING) != "value_only"
 
+    def evidence(self, witness: Discharge, operation: Operation) -> DominanceEvidence:
+        """Strict abstract relation (task 10.1): never falls back to order dominance.
+
+        Unavailable graphs, unmapped lines and cross-function witnesses return UNKNOWN with a
+        reason; the legacy boolean surface keeps its order fallback for non-opt-in callers.
+        """
+        decided = _pre_graph_evidence(witness, operation)
+        if decided is not None:
+            return decided
+        guard_line = witness.line
+        if guard_line is None:  # decided above; kept for line-type narrowing
+            return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:no_line")
+        cfg = self.graph(operation.path, operation.function, operation.line)
+        if cfg is None:
+            return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "cfg_unavailable")
+        found = cfg.relation(guard_line, operation.line)
+        if found is None:
+            return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "line_without_node")
+        if found == "all_paths":
+            effect = cfg.effect(guard_line, operation.line, throwing=witness.kind in _THROWING)
+            if effect == "value_only":
+                return DominanceEvidence(EvidenceRelation.NO, effect)
+            return DominanceEvidence(EvidenceRelation.MUST, effect)
+        if found == "some_paths":
+            effect = cfg.effect(guard_line, operation.line, throwing=witness.kind in _THROWING)
+            return DominanceEvidence(EvidenceRelation.MAY, effect)
+        if found in ("none", "after"):
+            return DominanceEvidence(EvidenceRelation.NO, None)
+        return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:unmapped_relation")
+
     def relation(self, witness: Discharge, operation: Operation) -> str:
         cfg = self._local(witness, operation)
         found = cfg.relation(witness.line, operation.line) if cfg is not None and witness.line is not None else None
@@ -112,6 +153,23 @@ class CfgDominance:
         return self.graph(operation.path, operation.function, operation.line)
 
 
+def _pre_graph_evidence(witness: Discharge, operation: Operation) -> DominanceEvidence | None:
+    """Relation facts that need no graph: scopes, in-operation kinds, cross-function witnesses, line order."""
+    if witness.scope in _SCOPED:
+        return DominanceEvidence(EvidenceRelation.MUST, "handler")
+    if witness.scope == "hop" or (witness.path, witness.function) != (operation.path, operation.function):
+        return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:cross_function")
+    if witness.kind in _IN_OPERATION:
+        if witness.line == operation.line:
+            return DominanceEvidence(EvidenceRelation.MUST, "constrains")
+        return DominanceEvidence(EvidenceRelation.NO, "constrains")
+    if witness.line is None:
+        return DominanceEvidence(EvidenceRelation.UNKNOWN, None, "dominance:no_line")
+    if witness.line >= operation.line:
+        return DominanceEvidence(EvidenceRelation.NO, None)
+    return None
+
+
 def describe(dominance: Dominance, witness: Discharge, operation: Operation, texts: Mapping[str, str]) -> tuple[str, str]:
     """A witness's relation to an operation and its failure effect, from the graph when the dominance has one."""
     relation = getattr(dominance, "relation", None)
@@ -154,4 +212,4 @@ def _order_effect(texts: Mapping[str, str], witness: Discharge, operation: Opera
     return "value_only"
 
 
-__all__ = ["CfgDominance", "describe", "operation_context"]
+__all__ = ["CfgDominance", "DominanceEvidence", "describe", "operation_context"]

tests/test_abstract_dominance.py

@@ -0,0 +1,189 @@
+"""Strict abstract-dominance relations over the CFG (Task 10.1, Reqs 10.1-10.7)."""
+
+import pytest
+
+from openultrasast.semantic.cfg import FunctionCfg
+from openultrasast.semantic.cst import parse_function_nodes
+from openultrasast.semantic.extra import grammar_for
+from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation
+from openultrasast.semantic.obligations.cfg_dominance import CfgDominance, DominanceEvidence
+from openultrasast.semantic.obligations.operations import Discharge, Operation
+
+PATH = "src/C.java"
+
+JAVA_GUARD = """class C {
+    void handle(Request request) {
+        if (!request.user.isAdmin()) { throw new IllegalStateException(); }
+        request.store.deleteAll();
+    }
+}
+"""
+
+JAVA_VALUE_ONLY = """class C {
+    void handle(Request request) {
+        boolean admin = request.user.isAdmin();
+        request.store.deleteAll();
+    }
+}
+"""
+
+JAVA_AFTER = """class C {
+    void handle(Request request) {
+        request.store.deleteAll();
+        if (!request.user.isAdmin()) { throw new IllegalStateException(); }
+    }
+}
+"""
+
+JAVA_SOME_PATHS = """class C {
+    void handle(Request request) {
+        if (request.flag) {
+            if (!request.user.isAdmin()) { throw new IllegalStateException(); }
+        }
+        request.store.deleteAll();
+    }
+}
+"""
+
+
+def _witness(line: int | None, *, kind: str = "path_guard", scope: str = "statement") -> Discharge:
+    return Discharge(
+        path=PATH,
+        line=line,
+        function="handle",
+        kind=kind,
+        fact_id="f:guard",
+        provenance="call",
+        scope=scope,
+        detail="",
+    )
+
+
+def _operation(line: int) -> Operation:
+    return Operation(
+        path=PATH,
+        line=line,
+        function="handle",
+        kind="protected_read",
+        fact_id="f:op",
+        resource="store",
+        requires=("path_guard",),
+    )
+
+
+def _dominance(text: str) -> CfgDominance:
+    if grammar_for("java") is None:
+        pytest.skip("no Java grammar installed")
+    nodes = parse_function_nodes(PATH, text, "java")
+    assert nodes, "the parser read no function"
+    cfg = FunctionCfg.from_cst(nodes[0], "java")
+    return CfgDominance({PATH: text}, {(PATH, "handle"): cfg})
+
+
+def _lines(text: str) -> dict[str, int]:
+    file_lines = text.splitlines()
+    return {
+        "guard": next(number for number, line_text in enumerate(file_lines, start=1) if "isAdmin" in line_text),
+        "operation": next(number for number, line_text in enumerate(file_lines, start=1) if "deleteAll" in line_text),
+    }
+
+
+def test_throwing_guard_on_all_paths_is_must() -> None:
+    dominance = _dominance(JAVA_GUARD)
+    lines = _lines(JAVA_GUARD)
+    evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.MUST
+    assert evidence.guard_effect == "throws"
+
+
+def test_value_only_guard_on_all_paths_is_no() -> None:
+    dominance = _dominance(JAVA_VALUE_ONLY)
+    lines = _lines(JAVA_VALUE_ONLY)
+    evidence = dominance.evidence(_witness(lines["guard"], kind="ownership_check"), _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.NO
+    assert evidence.guard_effect == "value_only"
+
+
+def test_guard_after_operation_is_no() -> None:
+    dominance = _dominance(JAVA_AFTER)
+    lines = _lines(JAVA_AFTER)
+    evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.NO
+
+
+def test_branch_conditional_guard_is_may() -> None:
+    dominance = _dominance(JAVA_SOME_PATHS)
+    lines = _lines(JAVA_SOME_PATHS)
+    evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.MAY
+
+
+def test_missing_graph_is_unknown_never_order_fallback() -> None:
+    dominance = CfgDominance({PATH: JAVA_GUARD}, {})
+    lines = _lines(JAVA_GUARD)
+    evidence = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.UNKNOWN
+    assert evidence.reason == "cfg_unavailable"
+
+
+def test_line_without_graph_node_is_unknown() -> None:
+    dominance = _dominance(JAVA_GUARD)
+    lines = _lines(JAVA_GUARD)
+    evidence = dominance.evidence(_witness(1), _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.UNKNOWN
+    assert evidence.reason == "line_without_node"
+
+
+def test_cross_function_witness_is_unknown_never_order() -> None:
+    dominance = _dominance(JAVA_GUARD)
+    lines = _lines(JAVA_GUARD)
+    cross_function_witness = Discharge(
+        path=PATH,
+        line=lines["guard"],
+        function="other",
+        kind="path_guard",
+        fact_id="f:guard",
+        provenance="call",
+        scope="hop",
+        detail="",
+    )
+    evidence = dominance.evidence(cross_function_witness, _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.UNKNOWN
+    assert evidence.reason == "dominance:cross_function"
+
+
+def test_scoped_witness_dominates_whole_handler() -> None:
+    dominance = _dominance(JAVA_GUARD)
+    lines = _lines(JAVA_GUARD)
+    scoped = _witness(None, scope="router")
+    evidence = dominance.evidence(scoped, _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.MUST
+
+
+def test_in_operation_witness_same_line_is_must() -> None:
+    dominance = _dominance(JAVA_GUARD)
+    lines = _lines(JAVA_GUARD)
+    constraint = _witness(lines["operation"], kind="identity_constraint")
+    evidence = dominance.evidence(constraint, _operation(lines["operation"]))
+    assert evidence.relation is EvidenceRelation.MUST
+
+
+def test_legacy_boolean_surface_unchanged() -> None:
+    dominance = CfgDominance({PATH: JAVA_GUARD}, {})
+    lines = _lines(JAVA_GUARD)
+    assert dominance.dominates(_witness(lines["guard"]), _operation(lines["operation"]), ()) is True
+    assert isinstance(dominance.relation(_witness(lines["guard"]), _operation(lines["operation"])), str)
+
+
+def test_dominance_evidence_is_frozen() -> None:
+    evidence = DominanceEvidence(relation=EvidenceRelation.MUST, guard_effect="throws", reason=None)
+    with pytest.raises(Exception):  # noqa: B017 - frozen dataclass raises on assignment
+        evidence.relation = EvidenceRelation.NO  # type: ignore[misc]
+
+
+def test_evidence_is_deterministic() -> None:
+    dominance = _dominance(JAVA_GUARD)
+    lines = _lines(JAVA_GUARD)
+    first = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"]))
+    second = dominance.evidence(_witness(lines["guard"]), _operation(lines["operation"]))
+    assert first == second