feat(access-control-prover): 10.4 one judgment per path

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

@@ -186,7 +186,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with
   - _Requirements: 2.2, 2.5, 2.7, 2.8, 11.1_
   - _Boundary: Witness Matcher_
   - _Depends: 7.3, 10.1_
-- [ ] 10.4 Compute one judgment per complete or diagnostic path
+- [x] 10.4 Compute one judgment per complete or diagnostic path
   - Conjoin witness dimensions, aggregate witnesses per obligation and apply the mixed-obligation rule.
   - Emit discharged only for all-MUST, indeterminate for any MAY/UNKNOWN, and unguarded for at least one NO.
   - Done when MUST/NO, MAY/NO, UNKNOWN and empty-witness fixtures match the specified truth table.

src/openultrasast/semantic/obligations/judgment.py

@@ -0,0 +1,68 @@
+"""Task 10.4 -- one judgment per path (Reqs 4.1-4.3, 11.2-11.4).
+
+A witness governs an obligation only when every required relation is MUST.
+With complete evidence and no governing witness for a required kind the path
+is unguarded; any MAY or UNKNOWN among required relations, or an incomplete
+path enumeration, makes it indeterminate. Engine module: no target names.
+"""
+
+from collections.abc import Mapping
+
+from .abstract_domain import (
+    Completeness,
+    EvidenceRelation,
+    PairJudgment,
+    PathJudgment,
+    WitnessMatch,
+    aggregate_witnesses,
+)
+from .cfg_dominance import DominanceEvidence
+from .operations import Operation
+
+
+def judgment_for_path(
+    operation: Operation,
+    matches_by_kind: Mapping[str, tuple[tuple[WitnessMatch, DominanceEvidence], ...]],
+    completeness: Completeness,
+    *,
+    discovery_complete: bool = True,
+) -> PathJudgment:
+    """Conjoin witness and dominance evidence per kind and judge the path."""
+    matches = tuple(dict.fromkeys(match for pairs in matches_by_kind.values() for match, _ in pairs))
+    if not completeness.is_complete:
+        return PathJudgment(PairJudgment.INDETERMINATE, (), completeness, matches)
+    relations_by_kind = {kind: _kind_relation(pairs, discovery_complete) for kind, pairs in matches_by_kind.items()}
+    judgment, missing = _mixed_obligation(relations_by_kind)
+    return PathJudgment(judgment, missing, completeness, matches)
+
+
+def _conjoined(pair: tuple[WitnessMatch, DominanceEvidence]) -> EvidenceRelation:
+    match, dominance = pair
+    if match.relation is EvidenceRelation.NO or dominance.relation is EvidenceRelation.NO:
+        return EvidenceRelation.NO
+    if match.relation is EvidenceRelation.MUST and dominance.relation is EvidenceRelation.MUST:
+        return EvidenceRelation.MUST
+    return EvidenceRelation.UNKNOWN
+
+
+def _kind_relation(pairs: tuple[tuple[WitnessMatch, DominanceEvidence], ...], discovery_complete: bool) -> EvidenceRelation:
+    if not pairs:
+        return EvidenceRelation.NO if discovery_complete else EvidenceRelation.UNKNOWN
+    return aggregate_witnesses(tuple(_conjoined(pair) for pair in pairs), discovery_complete=True)
+
+
+def _mixed_obligation(
+    relations_by_kind: Mapping[str, EvidenceRelation],
+) -> tuple[PairJudgment, tuple[str, ...]]:
+    absent_kinds = sorted(kind for kind, relation in relations_by_kind.items() if relation is EvidenceRelation.NO)
+    undecidable = any(
+        relation is not EvidenceRelation.MUST and relation is not EvidenceRelation.NO for relation in relations_by_kind.values()
+    )
+    if undecidable:
+        return PairJudgment.INDETERMINATE, ()
+    if absent_kinds:
+        return PairJudgment.UNGUARDED, tuple(absent_kinds)
+    return PairJudgment.DISCHARGED, ()
+
+
+__all__ = ["judgment_for_path"]

tests/test_pair_judgment.py

@@ -0,0 +1,154 @@
+"""Task 10.4 -- one judgment per path (Reqs 4.1-4.3, 11.2-11.4).
+
+Fixtures build WitnessMatch and DominanceEvidence directly; the truth table
+pinned here is the design's: a witness governs only when every dimension is
+MUST; one definite NO with the rest definite makes the path unguarded; any
+MAY or UNKNOWN among required relations makes it indeterminate.
+"""
+
+import pytest
+
+from openultrasast.semantic.obligations.abstract_domain import (
+    Completeness,
+    EvidenceRelation,
+    PairJudgment,
+    WitnessMatch,
+)
+from openultrasast.semantic.obligations.cfg_dominance import DominanceEvidence
+from openultrasast.semantic.obligations.judgment import judgment_for_path
+from openultrasast.semantic.obligations.operations import Operation
+
+PATH = "src/C.java"
+
+
+def _operation() -> Operation:
+    return Operation(PATH, 4, "handle", "protected_read", "f:op", "book", ("path_guard", "ownership_check"))
+
+
+def _match(relation: EvidenceRelation) -> WitnessMatch:
+    return WitnessMatch(
+        relation=relation,
+        resource_relation=EvidenceRelation.MUST,
+        authority_relation=EvidenceRelation.MUST,
+        evidence=("witness:f:guard", "operation:f:op"),
+    )
+
+
+def _dominance(relation: EvidenceRelation) -> DominanceEvidence:
+    return DominanceEvidence(relation=relation, guard_effect="throws")
+
+
+def _complete() -> Completeness:
+    return Completeness(is_complete=True)
+
+
+def _matches_by_kind(
+    path_guard: tuple[tuple[WitnessMatch, DominanceEvidence], ...],
+    ownership_check: tuple[tuple[WitnessMatch, DominanceEvidence], ...],
+) -> dict[str, tuple[tuple[WitnessMatch, DominanceEvidence], ...]]:
+    return {"path_guard": path_guard, "ownership_check": ownership_check}
+
+
+def test_must_and_no_produce_unguarded_with_missing_kind() -> None:
+    judgment = judgment_for_path(
+        _operation(),
+        _matches_by_kind(((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),), ()),
+        _complete(),
+    )
+    assert judgment.judgment is PairJudgment.UNGUARDED
+    assert judgment.missing == ("ownership_check",)
+
+
+def test_all_must_produces_discharged() -> None:
+    pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
+    judgment = judgment_for_path(_operation(), _matches_by_kind(pairs, pairs), _complete())
+    assert judgment.judgment is PairJudgment.DISCHARGED
+    assert judgment.missing == ()
+
+
+def test_may_and_no_produce_indeterminate() -> None:
+    judgment = judgment_for_path(
+        _operation(),
+        _matches_by_kind(
+            ((_match(EvidenceRelation.MAY), _dominance(EvidenceRelation.MUST)),),
+            (),
+        ),
+        _complete(),
+    )
+    assert judgment.judgment is PairJudgment.INDETERMINATE
+
+
+def test_unknown_match_relation_produces_indeterminate() -> None:
+    judgment = judgment_for_path(
+        _operation(),
+        _matches_by_kind(
+            ((_match(EvidenceRelation.UNKNOWN), _dominance(EvidenceRelation.MUST)),),
+            (),
+        ),
+        _complete(),
+    )
+    assert judgment.judgment is PairJudgment.INDETERMINATE
+
+
+def test_unknown_dominance_produces_indeterminate() -> None:
+    judgment = judgment_for_path(
+        _operation(),
+        _matches_by_kind(
+            ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.UNKNOWN)),),
+            (),
+        ),
+        _complete(),
+    )
+    assert judgment.judgment is PairJudgment.INDETERMINATE
+
+
+def test_empty_witnesses_with_complete_discovery_are_unguarded() -> None:
+    judgment = judgment_for_path(_operation(), _matches_by_kind((), ()), _complete())
+    assert judgment.judgment is PairJudgment.UNGUARDED
+    assert judgment.missing == ("ownership_check", "path_guard")
+
+
+def test_empty_witnesses_without_discovery_are_indeterminate() -> None:
+    judgment = judgment_for_path(_operation(), _matches_by_kind((), ()), _complete(), discovery_complete=False)
+    assert judgment.judgment is PairJudgment.INDETERMINATE
+
+
+def test_incomplete_path_completeness_is_indeterminate() -> None:
+    pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
+    judgment = judgment_for_path(
+        _operation(),
+        _matches_by_kind(pairs, pairs),
+        Completeness(is_complete=False, reasons=("resolution:no_candidate",)),
+    )
+    assert judgment.judgment is PairJudgment.INDETERMINATE
+
+
+def test_matches_are_carried_in_the_judgment() -> None:
+    must_pair = (_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST))
+    judgment = judgment_for_path(_operation(), _matches_by_kind((must_pair,), (must_pair,)), _complete())
+    assert judgment.matches == (_match(EvidenceRelation.MUST),)
+    assert judgment.matches[0].evidence == ("witness:f:guard", "operation:f:op")
+
+
+def test_judgment_is_deterministic() -> None:
+    pairs = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
+    first = judgment_for_path(_operation(), _matches_by_kind(pairs, ()), _complete())
+    second = judgment_for_path(_operation(), _matches_by_kind(pairs, ()), _complete())
+    assert first == second
+
+
+def test_empty_requires_with_no_witnesses_is_discharged() -> None:
+    operation = Operation(PATH, 4, "handle", "protected_read", "f:op", "book", ())
+    judgment = judgment_for_path(operation, {}, _complete())
+    assert judgment.judgment is PairJudgment.DISCHARGED
+
+
+def test_no_witness_for_one_kind_only_reports_that_kind() -> None:
+    must_pair = ((_match(EvidenceRelation.MUST), _dominance(EvidenceRelation.MUST)),)
+    judgment = judgment_for_path(_operation(), _matches_by_kind(must_pair, ()), _complete())
+    assert judgment.judgment is PairJudgment.UNGUARDED
+    assert judgment.missing == ("ownership_check",)
+
+
+if __name__ == "__main__":  # pragma: no cover
+    pytest.main([__file__, "-q"])