diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index d89beae..05cf960 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -193,7 +193,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Requirements: 4.1, 4.2, 4.3, 11.2, 11.3, 11.4_ - _Boundary: Pair Judgment_ - _Depends: 10.2, 10.3_ -- [ ] 10.5 Aggregate multiple paths in the opt-in checker mode +- [x] 10.5 Aggregate multiple paths in the opt-in checker mode - Return unguarded if any complete path is unguarded, discharged only for complete all-discharged enumeration, and indeterminate otherwise. - Keep the legacy checker API and defaults unchanged. diff --git a/src/openultrasast/semantic/obligations/judgment.py b/src/openultrasast/semantic/obligations/judgment.py index 1e16050..7da9fcd 100644 --- a/src/openultrasast/semantic/obligations/judgment.py +++ b/src/openultrasast/semantic/obligations/judgment.py @@ -1,9 +1,12 @@ -"""Task 10.4 -- one judgment per path (Reqs 4.1-4.3, 11.2-11.4). +"""Tasks 10.4-10.5 -- per-path judgment and multi-path aggregation (Reqs 4.1-4.5, 11.2-11.5). 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. +path enumeration, makes it indeterminate. Aggregation over paths: any +complete unguarded path is unguarded; a complete enumeration with every path +discharged is discharged; otherwise indeterminate. Engine module: no target +names. """ from collections.abc import Mapping @@ -15,6 +18,7 @@ from .abstract_domain import ( PathJudgment, WitnessMatch, aggregate_witnesses, + join_completeness, ) from .cfg_dominance import DominanceEvidence from .operations import Operation @@ -36,6 +40,40 @@ def judgment_for_path( return PathJudgment(judgment, missing, completeness, matches) +def aggregate_judgments(judgments: tuple[PathJudgment, ...]) -> PathJudgment: + """Aggregate path judgments: Reqs 3.10, 4.1-4.5, 11.5 (task 10.5). + + Any complete unguarded path decides unguarded; a complete enumeration + with every path discharged decides discharged; anything else, including + an empty enumeration, stays indeterminate. + """ + completeness = _joined_completeness(judgments) + matches = tuple(dict.fromkeys(match for judgment in judgments for match in judgment.matches)) + for judgment in judgments: + if judgment.judgment is PairJudgment.UNGUARDED and judgment.completeness.is_complete: + missing = tuple( + sorted( + { + kind + for other in judgments + if other.judgment is PairJudgment.UNGUARDED and other.completeness.is_complete + for kind in other.missing + } + ) + ) + return PathJudgment(PairJudgment.UNGUARDED, missing, completeness, matches) + if judgments and all(judgment.judgment is PairJudgment.DISCHARGED and judgment.completeness.is_complete for judgment in judgments): + return PathJudgment(PairJudgment.DISCHARGED, (), completeness, matches) + return PathJudgment(PairJudgment.INDETERMINATE, (), completeness, matches) + + +def _joined_completeness(judgments: tuple[PathJudgment, ...]) -> Completeness: + joined = Completeness(is_complete=True) + for judgment in judgments: + joined = join_completeness(joined, judgment.completeness) + return joined + + def _conjoined(pair: tuple[WitnessMatch, DominanceEvidence]) -> EvidenceRelation: match, dominance = pair if match.relation is EvidenceRelation.NO or dominance.relation is EvidenceRelation.NO: @@ -65,4 +103,4 @@ def _mixed_obligation( return PairJudgment.DISCHARGED, () -__all__ = ["judgment_for_path"] +__all__ = ["aggregate_judgments", "judgment_for_path"] diff --git a/tests/test_judgment_aggregation.py b/tests/test_judgment_aggregation.py new file mode 100644 index 0000000..071bf1c --- /dev/null +++ b/tests/test_judgment_aggregation.py @@ -0,0 +1,157 @@ +"""Task 10.5: aggregate multiple path judgments in the opt-in abstract mode. + +Req 3.10 chains stay independent; Reqs 4.1-4.5 findings only for unguarded; +Req 11.5: unguarded if any complete path is unguarded, discharged only for a +complete all-discharged enumeration, indeterminate otherwise. +""" + +from openultrasast.semantic.obligations.abstract_domain import ( + Completeness, + PairJudgment, + PathJudgment, + WitnessMatch, +) +from openultrasast.semantic.obligations.judgment import aggregate_judgments + + +def _match(evidence: str) -> WitnessMatch: + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation + + return WitnessMatch( + relation=EvidenceRelation.MUST, + resource_relation=EvidenceRelation.MUST, + authority_relation=EvidenceRelation.MUST, + evidence=(evidence,), + ) + + +def _judgment( + judgment: PairJudgment, + *, + missing: tuple[str, ...] = (), + is_complete: bool = True, + reasons: tuple[str, ...] = (), + evidence: tuple[str, ...] = (), +) -> PathJudgment: + completeness = Completeness(is_complete=is_complete, reasons=reasons) + return PathJudgment( + judgment=judgment, + missing=missing, + completeness=completeness, + matches=tuple(_match(item) for item in evidence), + ) + + +def test_any_complete_unguarded_path_makes_the_aggregate_unguarded() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.DISCHARGED), + _judgment(PairJudgment.UNGUARDED, missing=("path_guard",)), + ) + ) + assert aggregate.judgment is PairJudgment.UNGUARDED + assert aggregate.missing == ("path_guard",) + + +def test_unguarded_on_an_incomplete_path_does_not_decide() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.DISCHARGED), + _judgment( + PairJudgment.UNGUARDED, + missing=("path_guard",), + is_complete=False, + reasons=("resolution:no_candidate",), + ), + ) + ) + assert aggregate.judgment is PairJudgment.INDETERMINATE + + +def test_complete_all_discharged_enumeration_is_discharged() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.DISCHARGED), + _judgment(PairJudgment.DISCHARGED), + ) + ) + assert aggregate.judgment is PairJudgment.DISCHARGED + assert aggregate.missing == () + + +def test_discharged_with_one_incomplete_path_is_indeterminate() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.DISCHARGED), + _judgment( + PairJudgment.DISCHARGED, + is_complete=False, + reasons=("summaries:depth_cutoff",), + ), + ) + ) + assert aggregate.judgment is PairJudgment.INDETERMINATE + + +def test_discharged_and_indeterminate_mix_is_indeterminate() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.DISCHARGED), + _judgment(PairJudgment.INDETERMINATE), + ) + ) + assert aggregate.judgment is PairJudgment.INDETERMINATE + + +def test_empty_enumeration_is_indeterminate() -> None: + aggregate = aggregate_judgments(()) + assert aggregate.judgment is PairJudgment.INDETERMINATE + assert aggregate.missing == () + + +def test_missing_kinds_union_across_complete_unguarded_paths() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.UNGUARDED, missing=("path_guard",)), + _judgment( + PairJudgment.UNGUARDED, + missing=("ownership_check", "path_guard"), + ), + ) + ) + assert aggregate.judgment is PairJudgment.UNGUARDED + assert aggregate.missing == ("ownership_check", "path_guard") + + +def test_result_completeness_joins_input_reasons() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.DISCHARGED), + _judgment( + PairJudgment.INDETERMINATE, + is_complete=False, + reasons=("summaries:depth_cutoff",), + ), + ) + ) + assert aggregate.judgment is PairJudgment.INDETERMINATE + assert aggregate.completeness.is_complete is False + assert "summaries:depth_cutoff" in aggregate.completeness.reasons + + +def test_matches_from_every_path_are_carried_deduplicated() -> None: + aggregate = aggregate_judgments( + ( + _judgment(PairJudgment.UNGUARDED, missing=("path_guard",), evidence=("w:1",)), + _judgment(PairJudgment.DISCHARGED, evidence=("w:1", "w:2")), + ) + ) + assert tuple(match.evidence for match in aggregate.matches) == (("w:1",), ("w:2",)) + + +def test_aggregation_is_deterministic() -> None: + judgments = ( + _judgment(PairJudgment.UNGUARDED, missing=("path_guard",)), + _judgment(PairJudgment.DISCHARGED), + ) + assert aggregate_judgments(judgments) == aggregate_judgments(judgments)