diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index 6f78144..ce6c78d 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -300,7 +300,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Depends: 12.5_ - [ ] 13. Cross-cutting validation and measurements -- [ ] 13.1 Validate abstract-domain and metamorphic laws +- [x] 13.1 Validate abstract-domain and metamorphic laws - Cover the full join table, conjunction, witness aggregation, monotonicity and mixed-obligation rule. - Prove that type renaming preserves a judgment and adding ambiguity can only preserve it or make it indeterminate. - Done when property and fixture tests pass deterministically across repeated runs. diff --git a/tests/test_metamorphic_laws.py b/tests/test_metamorphic_laws.py new file mode 100644 index 0000000..dd3e536 --- /dev/null +++ b/tests/test_metamorphic_laws.py @@ -0,0 +1,202 @@ +"""Metamorphic-law validation for the abstract evidence domain (task 13.1). + +Covers the requirements the 7.1 algebra tests and the 10.4/10.5 fixture tests +leave as cross-domain laws only: the mixed-obligation rule swept over every +per-kind relation pair, judgment preservation under bijective type renaming, +and the Req 11.6 ambiguity-monotonicity law (adding ambiguity preserves a +judgment or makes it indeterminate -- it never flips unguarded/discharged). +Every law runs twice and asserts equal results (deterministic across repeated +runs). + +Reqs 11.2-11.7. The join-table, conjunction, witness-aggregation and +monotonicity laws of the domain itself are pinned in +tests/test_obligation_abstract_domain.py and are not duplicated here. +""" + +from __future__ import annotations + +import itertools + +import pytest + +from openultrasast.semantic.obligations.abstract_domain import ( + AuthorityImplication, + AuthorityRef, + Completeness, + EvidenceRelation, + ResourceRef, + WitnessMatch, +) +from openultrasast.semantic.obligations.cfg_dominance import DominanceEvidence +from openultrasast.semantic.obligations.judgment import judgment_for_path +from openultrasast.semantic.obligations.operations import Discharge, Operation +from openultrasast.semantic.obligations.witness import match_witness + +KINDS = ("path_guard", "ownership_check") +RELATIONS = ( + EvidenceRelation.MUST, + EvidenceRelation.MAY, + EvidenceRelation.NO, + EvidenceRelation.UNKNOWN, +) +_COMPLETE = Completeness(is_complete=True) + + +def _operation() -> Operation: + return Operation( + "src/C.java", + 4, + "handle", + "protected_read", + "f:op", + "book", + KINDS, + ) + + +def _pair(relation: EvidenceRelation) -> tuple[WitnessMatch, DominanceEvidence]: + match = WitnessMatch( + relation=relation, + resource_relation=EvidenceRelation.MUST, + authority_relation=EvidenceRelation.MUST, + evidence=("witness:f:guard",), + ) + return match, DominanceEvidence(relation=EvidenceRelation.MUST, guard_effect="throws") + + +def _matches_by_kind( + path_guard_relation: EvidenceRelation, ownership_relation: EvidenceRelation +) -> dict[str, tuple[tuple[WitnessMatch, DominanceEvidence], ...]]: + return { + "path_guard": (_pair(path_guard_relation),), + "ownership_check": (_pair(ownership_relation),), + } + + +def _expected_judgment(path_guard_relation: EvidenceRelation, ownership_relation: EvidenceRelation) -> str: + relations = (path_guard_relation, ownership_relation) + if any(relation not in (EvidenceRelation.MUST, EvidenceRelation.NO) for relation in relations): + return "indeterminate" + if EvidenceRelation.NO in relations: + missing = sorted(kind for kind, relation in zip(KINDS, relations, strict=True) if relation is EvidenceRelation.NO) + return "unguarded:" + "+".join(missing) + return "discharged" + + +def _judgment_name(judgment: object) -> str: + value = getattr(judgment, "value", None) + if isinstance(value, str): + return value + return getattr(judgment, "name", str(judgment)) + + +def test_mixed_obligation_rule_sweeps_every_relation_pair() -> None: + """Reqs 11.2-11.4: the mixed-obligation rule holds for every per-kind pair.""" + for path_guard_relation, ownership_relation in itertools.product(RELATIONS, RELATIONS): + judgment = judgment_for_path( + _operation(), + _matches_by_kind(path_guard_relation, ownership_relation), + _COMPLETE, + ) + expected = _expected_judgment(path_guard_relation, ownership_relation) + name = _judgment_name(judgment.judgment) + if expected.startswith("unguarded:"): + assert name == "unguarded", (path_guard_relation, ownership_relation, expected, name) + assert set(judgment.missing) == set(expected.split(":", 1)[1].split("+")) + else: + assert name == expected, (path_guard_relation, ownership_relation, expected, name) + + +def test_type_renaming_preserves_judgment_and_matching() -> None: + """Req 11.7: bijective renames of resources, authorities and fact ids change nothing observable.""" + witness = Discharge( + "src/C.java", + 3, + "handle", + "path_guard", + "java:guard", + "call", + "statement", + "", + resource=ResourceRef(kind="exact", values=("book",)), + authority=AuthorityRef(values=("admin",)), + ) + renamed_witness = Discharge( + "src/C.java", + 3, + "handle", + "path_guard", + "renamed:guard", + "call", + "statement", + "", + resource=ResourceRef(kind="exact", values=("tome",)), + authority=AuthorityRef(values=("root",)), + ) + operation = _operation() + renamed_operation = Operation( + "src/C.java", + 4, + "handle", + "protected_read", + "renamed:op", + "tome", + KINDS, + ) + implication = AuthorityImplication(id="impl:1", authority="admin", implies="supervisor") + renamed_implication = AuthorityImplication(id="impl:1", authority="root", implies="manager") + required = AuthorityRef(values=("supervisor",)) + renamed_required = AuthorityRef(values=("manager",)) + + base = match_witness(witness, operation, None, required_authority=required, implications=(implication,)) + renamed = match_witness( + renamed_witness, + renamed_operation, + None, + required_authority=renamed_required, + implications=(renamed_implication,), + ) + assert base.relation is renamed.relation is EvidenceRelation.MUST + assert base.resource_relation is renamed.resource_relation + assert base.authority_relation is renamed.authority_relation + + +def test_added_ambiguity_never_flips_discharged_to_unguarded() -> None: + """Req 11.6: degrading any dimension of a discharged pair keeps it discharged or makes it indeterminate.""" + degraded_relations = (EvidenceRelation.MAY, EvidenceRelation.UNKNOWN) + for degraded in degraded_relations: + for kind_index in range(len(KINDS)): + relations = [EvidenceRelation.MUST, EvidenceRelation.MUST] + relations[kind_index] = degraded + judgment = judgment_for_path( + _operation(), + _matches_by_kind(relations[0], relations[1]), + _COMPLETE, + ) + assert _judgment_name(judgment.judgment) in ("discharged", "indeterminate"), (degraded, kind_index) + + +def test_added_ambiguity_never_flips_unguarded_to_discharged() -> None: + """Req 11.6: degrading a governed kind of an unguarded pair keeps it unguarded or makes it indeterminate.""" + degraded_relations = (EvidenceRelation.MAY, EvidenceRelation.UNKNOWN) + for degraded in degraded_relations: + judgment = judgment_for_path( + _operation(), + _matches_by_kind(EvidenceRelation.NO, degraded), + _COMPLETE, + ) + assert _judgment_name(judgment.judgment) in ("unguarded", "indeterminate"), degraded + + +@pytest.mark.parametrize( + ("path_guard_relation", "ownership_relation"), + list(itertools.product(RELATIONS, RELATIONS)), +) +def test_laws_hold_deterministically_across_repeated_runs( + path_guard_relation: EvidenceRelation, ownership_relation: EvidenceRelation +) -> None: + """Req 11.7: two evaluations of the same law produce identical results.""" + matches = _matches_by_kind(path_guard_relation, ownership_relation) + first = judgment_for_path(_operation(), matches, _COMPLETE) + second = judgment_for_path(_operation(), matches, _COMPLETE) + assert first == second