From 2f97fb269302d40d72f420d147187c662df152b9 Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Thu, 29 Oct 2026 15:06:53 +0100 Subject: [PATCH] feat(access-control-prover): 7.3 authority abstract values and promoted implication facts --- .kiro/specs/access-control-prover/tasks.md | 2 +- .../semantic/obligations/abstract_domain.py | 171 ++++++- .../semantic/obligations/facts.py | 45 +- tests/test_obligation_authority_domain.py | 447 ++++++++++++++++++ 4 files changed, 660 insertions(+), 5 deletions(-) create mode 100644 tests/test_obligation_authority_domain.py diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index 9aa3491..4277649 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -94,7 +94,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with - _Requirements: 2.1, 2.5, 2.6, 2.7, 11.1_ - _Boundary: Resource Domain_ - _Depends: 7.1_ -- [ ] 7.3 Add authority abstract values and promoted implication facts +- [x] 7.3 Add authority abstract values and promoted implication facts - Represent exact, finite and unknown authorities separately from resources. - Load authority implications from promoted facts and retain the supporting fact identifier. - Done when sufficient, insufficient and unknown authority fixtures produce the specified relations. diff --git a/src/openultrasast/semantic/obligations/abstract_domain.py b/src/openultrasast/semantic/obligations/abstract_domain.py index 51fb895..b6e57ba 100644 --- a/src/openultrasast/semantic/obligations/abstract_domain.py +++ b/src/openultrasast/semantic/obligations/abstract_domain.py @@ -1,6 +1,6 @@ -"""Evidence relations, the completeness value and resource abstract values (access-control-prover). +"""Evidence relations, the completeness value, resource and authority abstract values (access-control-prover). -Covers Req 2.1, 2.5, 2.6, 2.7, 11.1, 11.6, 11.7. +Covers Req 2.1, 2.2, 2.5, 2.6, 2.7, 2.8, 11.1, 11.6, 11.7. ``EvidenceRelation`` is the abstract evidence domain: definite presence (``MUST``), definite absence (``NO``), possibility (``MAY``) and unknown (``UNKNOWN``). Three separate operations keep one table @@ -9,16 +9,24 @@ targets or control paths, ``conjoin_dimensions`` combines one witness's kind, sc and dominance dimensions, and ``aggregate_witnesses`` asks whether any witness definitely governs one obligation. ``ResourceRef`` abstracts one resource binding into an exact token, a finite alias set, request-global scope or an unknown value; ``join_resources`` unions alias sets finitely, lets -request-global scope absorb concrete bindings and never lets an unresolvable value resolve. Every +request-global scope absorb concrete bindings and never lets an unresolvable value resolve. +``AuthorityRef`` abstracts one authority holding into an exact name, a finite alternative set or an +unknown value; ``authority_satisfies`` asks whether a held authority satisfies a required one by +folding ``join_alternatives`` over every held-by-required name pair, where a pair is ``MUST`` when a +promoted ``AuthorityImplication`` chain connects them and ``NO`` otherwise, so sufficient authority is +``MUST``, insufficient is ``NO`` and undecidable is ``UNKNOWN`` (Req 2.5, 2.7, 2.8). ``supporting_implications`` +returns the implications used with their supporting fact ids, retained for the trace (Req 2.8). Every operation is deterministic, pure and independent of target names; join never converts ``MAY`` or ``UNKNOWN`` into ``MUST`` or ``NO``, so losing precision cannot manufacture a verdict. """ from __future__ import annotations +from collections import deque from collections.abc import Iterable, Mapping, Sequence from dataclasses import dataclass from enum import Enum +from functools import reduce from typing import Literal @@ -108,6 +116,163 @@ def join_resources(left: ResourceRef, right: ResourceRef) -> ResourceRef: return ResourceRef(kind="aliases", values=left.values + right.values) +@dataclass(frozen=True) +class AuthorityRef: + """The abstract value of one authority holding (design, "Abstract evidence domain"; Req 2.1, 2.2, 2.5, 2.7, 11.1). + + One value is an ``exact`` authority, several values are a ``finite`` alternative set (the authority is + one of them, not all of them) and ``is_unknown`` marks an unresolvable holding that can neither match + nor fail. Values are deduplicated and sorted, so equal holdings are equal however they were + constructed; a misshapen value fails loud rather than degrading silently. + """ + + values: tuple[str, ...] + is_unknown: bool = False + + def __post_init__(self) -> None: + if not all(isinstance(value, str) and value for value in self.values): + raise ValueError(f"misshapen authority values: {self.values!r}") + if self.is_unknown and self.values: + raise ValueError(f"unknown authority binds no values: {self.values!r}") + if not self.is_unknown and not self.values: + raise ValueError("authority needs at least one value") + object.__setattr__(self, "values", tuple(sorted(set(self.values)))) + + +UNKNOWN_AUTHORITY = AuthorityRef(values=(), is_unknown=True) + + +def parse_authority(binding: str | Sequence[str] | None) -> AuthorityRef: + """Parse one authority holding from fact or IR evidence into its abstract value. + + A single name is ``exact``, a finite name collection is a finite alternative set, and ``None`` + (no holding could be resolved) is ``unknown``; anything misshapen raises instead of quietly degrading. + """ + if binding is None: + return UNKNOWN_AUTHORITY + names = (binding,) if isinstance(binding, str) else tuple(binding) + if not names or not all(isinstance(name, str) and name for name in names): + raise ValueError(f"misshapen authority binding: {binding!r}") + return AuthorityRef(values=names) + + +def join_authorities(left: AuthorityRef, right: AuthorityRef) -> AuthorityRef: + """Join authority holdings from alternative paths or call targets. + + Identical exact holdings stay exact and finite sets join by finite union, mirroring ``join_resources``; + an unresolvable holding joins to ``unknown`` so losing precision cannot manufacture a match + (Req 2.7, 11.1). + """ + if left.is_unknown or right.is_unknown: + return UNKNOWN_AUTHORITY + if left.values == right.values: + return left + return AuthorityRef(values=left.values + right.values) + + +@dataclass(frozen=True) +class AuthorityImplication: + """One promoted implication fact: ``authority`` also covers ``implies`` (Req 2.8). + + ``id`` is the supporting promoted fact row's identifier, retained so the trace can name the + implication used. The engine bakes in no implication of its own; only these facts connect authorities. + """ + + id: str + authority: str + implies: str + + +def _implication_index( + implications: Iterable[AuthorityImplication], +) -> dict[str, tuple[AuthorityImplication, ...]]: + """Group implications by the authority they extend, preserving first-occurrence order.""" + grouped: dict[str, list[AuthorityImplication]] = {} + for implication in implications: + grouped.setdefault(implication.authority, []).append(implication) + return {authority: tuple(edges) for authority, edges in grouped.items()} + + +def _implication_path( + source: str, + target: str, + index: Mapping[str, tuple[AuthorityImplication, ...]], +) -> tuple[AuthorityImplication, ...] | None: + """The implications leading from ``source`` to ``target``, or ``None`` when no promoted chain reaches it. + + Breadth-first over the finite edges in fact order, so the returned chain is deterministic and shortest + by edge count; ``()`` means the names are identical and no implication is needed. + """ + if source == target: + return () + parents: dict[str, tuple[str, AuthorityImplication] | None] = {source: None} + frontier: deque[str] = deque([source]) + while frontier: + current = frontier.popleft() + for implication in index.get(current, ()): + reached = implication.implies + if reached in parents: + continue + parents[reached] = (current, implication) + if reached == target: + chain: list[AuthorityImplication] = [] + node: str = target + while True: + step = parents[node] + if step is None: + return tuple(reversed(chain)) + previous, edge = step + chain.append(edge) + node = previous + frontier.append(reached) + return None + + +def authority_satisfies( + held: AuthorityRef, + required: AuthorityRef, + implications: Iterable[AuthorityImplication] = (), +) -> EvidenceRelation: + """Ask whether one held authority value satisfies one required authority value (Req 2.5, 2.7, 2.8, 11.1). + + Each held-by-required name pair is definite: ``MUST`` when the names match or a promoted implication + chain connects them, ``NO`` otherwise. The aggregate folds ``join_alternatives`` over every pair, so a + finite holding with one satisfying alternative is ``MAY``; an unresolvable holding or requirement is + ``UNKNOWN`` and can never match broadly or fail definitely. + """ + if held.is_unknown or required.is_unknown: + return EvidenceRelation.UNKNOWN + index = _implication_index(implications) + pairs = [ + EvidenceRelation.MUST if _implication_path(held_name, required_name, index) is not None else EvidenceRelation.NO + for held_name in held.values + for required_name in required.values + ] + return reduce(join_alternatives, pairs) + + +def supporting_implications( + held: AuthorityRef, + required: AuthorityRef, + implications: Iterable[AuthorityImplication] = (), +) -> tuple[AuthorityImplication, ...]: + """The implications used on satisfying paths, with supporting fact ids retained for the trace (Req 2.8). + + First-occurrence order over the normalized names, deduplicated; empty when nothing matched or the + relation could not be decided. + """ + if held.is_unknown or required.is_unknown: + return () + index = _implication_index(implications) + used: list[AuthorityImplication] = [] + for held_name in held.values: + for required_name in required.values: + chain = _implication_path(held_name, required_name, index) + if chain is not None: + used.extend(chain) + return tuple(dict.fromkeys(used)) + + _ALTERNATIVE_JOIN: Mapping[tuple[EvidenceRelation, EvidenceRelation], EvidenceRelation] = { (EvidenceRelation.MUST, EvidenceRelation.MUST): EvidenceRelation.MUST, (EvidenceRelation.MUST, EvidenceRelation.NO): EvidenceRelation.MAY, diff --git a/src/openultrasast/semantic/obligations/facts.py b/src/openultrasast/semantic/obligations/facts.py index 48100e6..ff9d1fb 100644 --- a/src/openultrasast/semantic/obligations/facts.py +++ b/src/openultrasast/semantic/obligations/facts.py @@ -14,6 +14,7 @@ from pathlib import Path from ...source import canonical_language from ..facts import _ruleset_state +from .abstract_domain import AuthorityImplication OPERATION_KINDS = ("protected_read", "protected_write", "privileged_action", "security_setting") DISCHARGER_KINDS = ("path_guard", "identity_constraint", "ownership_check", "non_permissive_value", "validated_input") @@ -38,6 +39,7 @@ _OPERATION_FIELDS = frozenset( _DISCHARGER_FIELDS = frozenset( {"id", "kind", "calls", "decorators", "identity_sources", "constraint_params", "request_sources", "permissive_values"} ) +_IMPLICATION_FIELDS = frozenset({"id", "authority", "implies"}) class ObligationFactsError(ValueError): @@ -79,11 +81,25 @@ class DischargerFact: permissive_values: tuple[str, ...] = () # literal values that leave a security setting open (non_permissive_value facts) +@dataclass(frozen=True) +class ImplicationFact(AuthorityImplication): + """One promoted ``[[implication]]`` row: ``authority`` also covers ``implies`` (Req 2.8). + + Extends the abstract domain's ``AuthorityImplication`` with the loader's language scope, so loaded + facts feed ``authority_satisfies`` directly while filtering per language like every other fact row. + """ + + language: str = "" + + @dataclass(frozen=True) class ObligationFacts: version: str operations: tuple[OperationFact, ...] dischargers: tuple[DischargerFact, ...] + # Requirement 2.8 (access-control-prover): promoted authority implications, each retaining the + # supporting fact row id so the trace can name the implication used. Default-empty; older data loads unchanged. + implications: tuple[ImplicationFact, ...] = () def for_language(self, language: str) -> ObligationFacts: key = canonical_language(language) @@ -93,6 +109,7 @@ class ObligationFacts: version=self.version, operations=tuple(item for item in self.operations if item.language == key), dischargers=tuple(item for item in self.dischargers if item.language == key), + implications=tuple(item for item in self.implications if item.language == key), ) @@ -102,6 +119,7 @@ def _load_obligation_facts_uncached(directory: Path | None = None) -> Obligation raise ObligationFactsError(f"obligation facts directory missing: {root}") operations: list[OperationFact] = [] dischargers: list[DischargerFact] = [] + implications: list[ImplicationFact] = [] versions: list[str] = [] for path in sorted(root.glob("*.toml")): try: @@ -112,6 +130,8 @@ def _load_obligation_facts_uncached(directory: Path | None = None) -> Obligation versions.append(str(payload.get("version", "1"))) for row in _rows(payload.get("operation"), path): operations.append(_operation_fact(row, path, language)) + for row in _rows(payload.get("implication"), path): + implications.append(_implication_fact(row, path, language)) for row in _rows(payload.get("discharger"), path): _only_fields(row, _DISCHARGER_FIELDS, path) kind = str(row.get("kind", "")) @@ -130,7 +150,12 @@ def _load_obligation_facts_uncached(directory: Path | None = None) -> Obligation permissive_values=_strings(row.get("permissive_values"), "permissive_values", path), ) ) - return ObligationFacts(version=versions[0] if versions else "1", operations=tuple(operations), dischargers=tuple(dischargers)) + return ObligationFacts( + version=versions[0] if versions else "1", + operations=tuple(operations), + dischargers=tuple(dischargers), + implications=tuple(implications), + ) def _operation_fact(row: dict[str, object], path: Path, language: str) -> OperationFact: @@ -166,6 +191,24 @@ def _operation_fact(row: dict[str, object], path: Path, language: str) -> Operat ) +def _implication_fact(row: dict[str, object], path: Path, language: str) -> ImplicationFact: + """Validate one implication row against the closed fields; both names must be non-empty strings.""" + _only_fields(row, _IMPLICATION_FIELDS, path) + return ImplicationFact( + id=str(row["id"]), + authority=_implication_name(row, "authority", path), + implies=_implication_name(row, "implies", path), + language=language, + ) + + +def _implication_name(row: dict[str, object], field: str, path: Path) -> str: + value = row.get(field) + if not isinstance(value, str) or not value: + raise ObligationFactsError(f"{path}: implication {row.get('id')!r} needs a non-empty {field}") + return value + + def _optional_int(row: dict[str, object], field: str, path: Path, *, positive: bool) -> int | None: value = row.get(field) if value is None: diff --git a/tests/test_obligation_authority_domain.py b/tests/test_obligation_authority_domain.py new file mode 100644 index 0000000..2ead573 --- /dev/null +++ b/tests/test_obligation_authority_domain.py @@ -0,0 +1,447 @@ +"""access-control-prover task 7.3: authority abstract values and promoted implication facts (offline). + +Exact, finite and unknown authorities per the design's "Abstract evidence domain" section (Req 2.1, 2.2, +2.5, 2.7, 11.1), the promoted implication facts that carry one authority implying another with the +supporting fact id retained (Req 2.8), and the satisfy query stated in the EvidenceRelation algebra +from task 7.1: sufficient authority is MUST, insufficient is NO, undecidable is UNKNOWN, and a finite set +with one satisfying alternative is MAY. +""" + +from __future__ import annotations + +import itertools +from pathlib import Path +from typing import TYPE_CHECKING + +import pytest + +if TYPE_CHECKING: + from openultrasast.semantic.obligations.abstract_domain import AuthorityImplication, AuthorityRef + + +def _authority_fixtures() -> tuple[AuthorityRef, ...]: + from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_AUTHORITY, parse_authority + + return ( + parse_authority("admin"), + parse_authority("staff"), + parse_authority("guest"), + parse_authority(["admin", "guest"]), + parse_authority(["staff", "owner"]), + UNKNOWN_AUTHORITY, + ) + + +def _implication_fixtures() -> tuple[AuthorityImplication, ...]: + from openultrasast.semantic.obligations.abstract_domain import AuthorityImplication + + # owner -> staff -> authenticated, plus admin -> owner: a chain promotion must be able to walk. + return ( + AuthorityImplication(id="admin-covers-owner", authority="admin", implies="owner"), + AuthorityImplication(id="owner-covers-staff", authority="owner", implies="staff"), + AuthorityImplication(id="staff-covers-authenticated", authority="staff", implies="authenticated"), + ) + + +_IMPLICATION_TOML = """version = "1" +language = "python" + +[[operation]] +id = "orm-read" +kind = "protected_read" +calls = ["filter_by"] +requires = ["identity_constraint"] +sensitivity = "high" + +[[implication]] +id = "admin-covers-owner" +authority = "admin" +implies = "owner" + +[[implication]] +id = "owner-covers-staff" +authority = "owner" +implies = "staff" +""" + + +def test_parse_authority_single_name_is_exact() -> None: + from openultrasast.semantic.obligations.abstract_domain import AuthorityRef, parse_authority + + authority = parse_authority("admin") + assert authority == AuthorityRef(values=("admin",)) + assert authority.values == ("admin",) + assert authority.is_unknown is False + + +def test_parse_authority_name_collection_is_a_finite_set() -> None: + from openultrasast.semantic.obligations.abstract_domain import AuthorityRef, parse_authority + + authority = parse_authority(["owner", "admin", "owner"]) + assert authority == AuthorityRef(values=("admin", "owner")) + + +def test_parse_authority_without_a_binding_is_unknown() -> None: + from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_AUTHORITY, parse_authority + + authority = parse_authority(None) + assert authority == UNKNOWN_AUTHORITY + assert authority.is_unknown is True + assert authority.values == () + + +def test_authority_grades_distinguish_exact_finite_and_unknown() -> None: + # Req 11.1: authority compatibility distinguishes definite, possible, absent and unknown evidence. + from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_AUTHORITY, parse_authority + + exact = parse_authority("admin") + finite = parse_authority(["admin", "owner"]) + grades = {exact, finite, UNKNOWN_AUTHORITY} + assert len(grades) == 3 + assert (len(exact.values), exact.is_unknown) == (1, False) + assert (len(finite.values), finite.is_unknown) == (2, False) + assert UNKNOWN_AUTHORITY.values == () and UNKNOWN_AUTHORITY.is_unknown + + +def test_authority_values_are_normalized_deterministically() -> None: + from openultrasast.semantic.obligations.abstract_domain import AuthorityRef + + forward = AuthorityRef(values=("owner", "admin", "owner")) + backward = AuthorityRef(values=("admin", "owner")) + assert forward == backward + assert hash(forward) == hash(backward) + assert len({forward, backward}) == 1 + + +def test_authority_ref_fails_loud_on_misshapen_values() -> None: + from openultrasast.semantic.obligations.abstract_domain import AuthorityRef + + with pytest.raises(ValueError, match="at least one"): + AuthorityRef(values=()) + with pytest.raises(ValueError, match="unknown authority"): + AuthorityRef(values=("admin",), is_unknown=True) + with pytest.raises(ValueError, match="misshapen"): + AuthorityRef(values=("admin", "")) + with pytest.raises(ValueError, match="misshapen"): + AuthorityRef(values=("",)) + + +def test_parse_authority_rejects_misshapen_bindings() -> None: + from openultrasast.semantic.obligations.abstract_domain import parse_authority + + with pytest.raises(ValueError): + parse_authority("") + with pytest.raises(ValueError): + parse_authority(()) + with pytest.raises(ValueError): + parse_authority(["admin", ""]) + + +def test_join_authorities_keeps_identical_exact_authorities_exact() -> None: + from openultrasast.semantic.obligations.abstract_domain import join_authorities, parse_authority + + authority = parse_authority("admin") + assert join_authorities(authority, parse_authority("admin")) == authority + + +def test_join_authorities_merges_different_authorities_into_a_finite_set() -> None: + from openultrasast.semantic.obligations.abstract_domain import join_authorities, parse_authority + + joined = join_authorities(parse_authority("admin"), parse_authority("owner")) + assert joined == parse_authority(["admin", "owner"]) + + +def test_join_authorities_unions_finite_sets_to_their_superset() -> None: + from openultrasast.semantic.obligations.abstract_domain import join_authorities, parse_authority + + subset = parse_authority(["admin"]) + superset = parse_authority(["admin", "owner"]) + assert join_authorities(subset, superset) == superset + assert join_authorities(superset, subset) == superset + assert join_authorities(parse_authority(["admin"]), parse_authority(["staff"])) == parse_authority(["admin", "staff"]) + + +def test_join_authorities_unknown_absorbs_every_fixture() -> None: + # Req 11.1: an unresolvable authority stays unresolvable; joining cannot manufacture precision. + from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_AUTHORITY, join_authorities + + for other in _authority_fixtures(): + assert join_authorities(other, UNKNOWN_AUTHORITY) == UNKNOWN_AUTHORITY, other + assert join_authorities(UNKNOWN_AUTHORITY, other) == UNKNOWN_AUTHORITY, other + + +def test_join_authorities_is_commutative_and_idempotent_over_fixtures() -> None: + from openultrasast.semantic.obligations.abstract_domain import join_authorities + + fixtures = _authority_fixtures() + for left, right in itertools.product(fixtures, repeat=2): + assert join_authorities(left, right) == join_authorities(right, left), (left, right) + for authority in fixtures: + assert join_authorities(authority, authority) == authority, authority + + +def test_sufficient_exact_authority_satisfies_the_required_authority() -> None: + # Req 2.5, 11.1: a witness holding exactly the required authority is a definite match. + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + assert authority_satisfies(parse_authority("admin"), parse_authority("admin")) is EvidenceRelation.MUST + + +def test_sufficient_authority_via_promoted_implication_satisfies() -> None: + # Req 2.8: one authority implying another discharges the requirement, from promoted facts only. + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + implications = _implication_fixtures() + assert authority_satisfies(parse_authority("staff"), parse_authority("authenticated"), implications) is EvidenceRelation.MUST + assert authority_satisfies(parse_authority("admin"), parse_authority("staff"), implications) is EvidenceRelation.MUST + + +def test_transitive_implication_chain_satisfies_across_every_hop() -> None: + # Req 2.8: admin -> owner -> staff -> authenticated must hold end to end. + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + assert authority_satisfies(parse_authority("admin"), parse_authority("authenticated"), _implication_fixtures()) is EvidenceRelation.MUST + + +def test_cyclic_implications_terminate() -> None: + from openultrasast.semantic.obligations.abstract_domain import ( + AuthorityImplication, + EvidenceRelation, + authority_satisfies, + parse_authority, + ) + + ring = ( + AuthorityImplication(id="billing-covers-audit", authority="billing", implies="audit"), + AuthorityImplication(id="audit-covers-billing", authority="audit", implies="billing"), + ) + assert authority_satisfies(parse_authority("billing"), parse_authority("audit"), ring) is EvidenceRelation.MUST + assert authority_satisfies(parse_authority("billing"), parse_authority("admin"), ring) is EvidenceRelation.NO + + +def test_implication_applies_only_when_promoted() -> None: + # Req 2.8: the engine bakes in no implication vocabulary; without the promoted fact it is NO. + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + assert authority_satisfies(parse_authority("staff"), parse_authority("authenticated"), ()) is EvidenceRelation.NO + + +def test_insufficient_authority_is_definitely_insufficient() -> None: + # Req 2.5: an insufficient authority must not discharge the operation; the relation is NO. + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + assert authority_satisfies(parse_authority("guest"), parse_authority("admin"), _implication_fixtures()) is EvidenceRelation.NO + + +def test_unknown_held_authority_cannot_be_decided() -> None: + # Req 2.7, 11.1: undecidable authority compatibility is UNKNOWN, never a broad match or a rejection. + from openultrasast.semantic.obligations.abstract_domain import ( + UNKNOWN_AUTHORITY, + EvidenceRelation, + authority_satisfies, + parse_authority, + ) + + assert authority_satisfies(UNKNOWN_AUTHORITY, parse_authority("admin"), _implication_fixtures()) is EvidenceRelation.UNKNOWN + + +def test_unknown_required_authority_cannot_be_decided() -> None: + # Req 2.7: an unresolvable requirement is UNKNOWN, so the pair cannot become a final verdict. + from openultrasast.semantic.obligations.abstract_domain import ( + UNKNOWN_AUTHORITY, + EvidenceRelation, + authority_satisfies, + parse_authority, + ) + + assert authority_satisfies(parse_authority("admin"), UNKNOWN_AUTHORITY, _implication_fixtures()) is EvidenceRelation.UNKNOWN + + +def test_finite_authority_with_one_satisfying_alternative_is_possible() -> None: + # Req 11.1: one satisfying and one failing alternative join to MAY, never to MUST or NO. + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + relation = authority_satisfies(parse_authority(["admin", "guest"]), parse_authority("admin"), _implication_fixtures()) + assert relation is EvidenceRelation.MAY + + +def test_finite_authority_with_all_alternatives_satisfying_is_definite() -> None: + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + relation = authority_satisfies(parse_authority(["admin", "owner"]), parse_authority("staff"), _implication_fixtures()) + assert relation is EvidenceRelation.MUST + + +def test_widened_required_authority_stays_possible_not_definite() -> None: + # Req 2.7, 11.1: a requirement only imprecisely resolved to {authenticated, guest} is MAY, not MUST. + from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, authority_satisfies, parse_authority + + relation = authority_satisfies(parse_authority("admin"), parse_authority(["authenticated", "guest"]), _implication_fixtures()) + assert relation is EvidenceRelation.MAY + + +def test_authority_satisfies_folds_single_pairs_with_join_alternatives() -> None: + # The 7.1 law: the aggregate is exactly join_alternatives over every held x required singleton pair. + from openultrasast.semantic.obligations.abstract_domain import ( + EvidenceRelation, + authority_satisfies, + join_alternatives, + parse_authority, + ) + + implications = _implication_fixtures() + for held, required in itertools.product(_authority_fixtures(), repeat=2): + aggregated = authority_satisfies(held, required, implications) + if held.is_unknown or required.is_unknown: + assert aggregated is EvidenceRelation.UNKNOWN, (held, required) + continue + folded: EvidenceRelation | None = None + for held_name in held.values: + for required_name in required.values: + single = authority_satisfies(parse_authority(held_name), parse_authority(required_name), implications) + folded = single if folded is None else join_alternatives(folded, single) + assert folded == aggregated, (held, required) + + +def test_widening_either_authority_never_gains_definiteness() -> None: + # Req 11.1, 11.6: coarsening a value moves the relation up the precision order or leaves it. + from openultrasast.semantic.obligations.abstract_domain import at_least_as_precise, authority_satisfies, join_authorities + + implications = _implication_fixtures() + fixtures = _authority_fixtures() + for held, required, extra in itertools.product(fixtures, repeat=3): + base = authority_satisfies(held, required, implications) + wider_held = authority_satisfies(join_authorities(held, extra), required, implications) + assert at_least_as_precise(base, wider_held), (held, extra, required) + wider_required = authority_satisfies(held, join_authorities(required, extra), implications) + assert at_least_as_precise(base, wider_required), (held, required, extra) + + +def test_supporting_implications_retain_the_fact_ids_used() -> None: + # Req 2.8: the implications used on the satisfying path are retained with their supporting fact ids. + from openultrasast.semantic.obligations.abstract_domain import authority_satisfies, parse_authority, supporting_implications + + implications = _implication_fixtures() + used = supporting_implications(parse_authority("admin"), parse_authority("authenticated"), implications) + assert [implication.id for implication in used] == [ + "admin-covers-owner", + "owner-covers-staff", + "staff-covers-authenticated", + ] + assert authority_satisfies(parse_authority("admin"), parse_authority("authenticated"), implications).value == "must" + + +def test_supporting_implications_are_empty_for_identity_and_for_failure() -> None: + from openultrasast.semantic.obligations.abstract_domain import ( + UNKNOWN_AUTHORITY, + parse_authority, + supporting_implications, + ) + + implications = _implication_fixtures() + assert supporting_implications(parse_authority("admin"), parse_authority("admin"), implications) == () + assert supporting_implications(parse_authority("guest"), parse_authority("admin"), implications) == () + assert supporting_implications(UNKNOWN_AUTHORITY, parse_authority("admin"), implications) == () + + +def test_supporting_implications_deduplicate_stably() -> None: + from openultrasast.semantic.obligations.abstract_domain import parse_authority, supporting_implications + + implications = _implication_fixtures() + assert supporting_implications(parse_authority("owner"), parse_authority("staff"), implications + implications) == (implications[1],) + + +def test_implication_facts_load_and_retain_supporting_ids(tmp_path: Path) -> None: + # Req 2.8: implications come from promoted fact rows, keep the row id for the trace, and stay + # AuthorityImplication values so the checker can feed them straight into the satisfy algebra. + from openultrasast.semantic.obligations.abstract_domain import AuthorityImplication + from openultrasast.semantic.obligations.facts import ImplicationFact, load_obligation_facts + + (tmp_path / "python.toml").write_text(_IMPLICATION_TOML) + facts = load_obligation_facts(tmp_path) + assert facts.implications == ( + ImplicationFact(id="admin-covers-owner", authority="admin", implies="owner", language="python"), + ImplicationFact(id="owner-covers-staff", authority="owner", implies="staff", language="python"), + ) + assert all(isinstance(implication, AuthorityImplication) for implication in facts.implications) + + +def test_implication_facts_default_to_empty(tmp_path: Path) -> None: + from openultrasast.semantic.obligations.facts import load_obligation_facts + + (tmp_path / "python.toml").write_text( + 'version = "1"\nlanguage = "python"\n\n[[operation]]\nid = "orm-read"\nkind = "protected_read"\n' + 'calls = ["filter_by"]\nrequires = ["identity_constraint"]\nsensitivity = "high"\n' + ) + assert load_obligation_facts(tmp_path).implications == () + + +def test_implication_facts_filter_by_language(tmp_path: Path) -> None: + from openultrasast.semantic.obligations.facts import load_obligation_facts + + (tmp_path / "python.toml").write_text(_IMPLICATION_TOML) + (tmp_path / "ruby.toml").write_text( + 'version = "1"\nlanguage = "ruby"\n\n[[implication]]\nid = "ruby-maintainer-covers-reporter"\n' + 'authority = "maintainer"\nimplies = "reporter"\n' + ) + all_languages = load_obligation_facts(tmp_path) + assert {implication.id for implication in all_languages.implications} == { + "admin-covers-owner", + "owner-covers-staff", + "ruby-maintainer-covers-reporter", + } + python = all_languages.for_language("python") + assert [implication.id for implication in python.implications] == ["admin-covers-owner", "owner-covers-staff"] + assert all_languages.for_language("ruby").implications != python.implications + + +def test_implication_fact_rejects_unknown_fields(tmp_path: Path) -> None: + from openultrasast.semantic.obligations.facts import ObligationFactsError, load_obligation_facts + + (tmp_path / "python.toml").write_text(_IMPLICATION_TOML + "weight = 3\n") + with pytest.raises(ObligationFactsError, match="weight"): + load_obligation_facts(tmp_path) + + +def test_implication_fact_rejects_missing_or_misshapen_names(tmp_path: Path) -> None: + from openultrasast.semantic.obligations.facts import ObligationFactsError, load_obligation_facts + + (tmp_path / "python.toml").write_text('version = "1"\nlanguage = "python"\n\n[[implication]]\nid = "broken"\nimplies = "owner"\n') + with pytest.raises(ObligationFactsError, match="authority"): + load_obligation_facts(tmp_path) + (tmp_path / "python.toml").write_text('version = "1"\nlanguage = "python"\n\n[[implication]]\nid = "broken"\nauthority = "admin"\n') + with pytest.raises(ObligationFactsError, match="implies"): + load_obligation_facts(tmp_path) + (tmp_path / "python.toml").write_text( + 'version = "1"\nlanguage = "python"\n\n[[implication]]\nid = "broken"\nauthority = "admin"\nimplies = ""\n' + ) + with pytest.raises(ObligationFactsError, match="implies"): + load_obligation_facts(tmp_path) + + +def test_sufficient_insufficient_and_unknown_fixtures_produce_the_specified_relations() -> None: + # The task's three fixture grades: sufficient -> MUST, insufficient -> NO, unknown -> UNKNOWN. + from openultrasast.semantic.obligations.abstract_domain import ( + UNKNOWN_AUTHORITY, + EvidenceRelation, + authority_satisfies, + parse_authority, + ) + + implications = _implication_fixtures() + sufficient = ( + (parse_authority("admin"), parse_authority("admin")), + (parse_authority("staff"), parse_authority("authenticated")), + (parse_authority(["admin", "owner"]), parse_authority("staff")), + ) + for held, required in sufficient: + assert authority_satisfies(held, required, implications) is EvidenceRelation.MUST, (held, required) + insufficient = ( + (parse_authority("guest"), parse_authority("admin")), + (parse_authority("staff"), parse_authority("authenticated"), ()), + ) + for fixture in insufficient: + held, required, *rest = fixture + assert authority_satisfies(held, required, *rest) is EvidenceRelation.NO, fixture + assert authority_satisfies(UNKNOWN_AUTHORITY, parse_authority("admin"), implications) is EvidenceRelation.UNKNOWN + assert authority_satisfies(parse_authority("admin"), UNKNOWN_AUTHORITY, implications) is EvidenceRelation.UNKNOWN