feat(access-control-prover): 7.2 resource abstract values and operation-fact fields

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

@@ -87,7 +87,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with
   - Done when exhaustive table tests and algebraic law tests pass for every relation pair.
   - _Requirements: 11.1, 11.6, 11.7_
   - _Boundary: Abstract Evidence Domain_
-- [ ] 7.2 Add resource abstract values and operation-fact fields
+- [x] 7.2 Add resource abstract values and operation-fact fields
   - Represent exact resources, finite alias sets, request-global scope and unknown resources.
   - Extend operation facts to state when a request-global guard is sufficient.
   - Done when resource parsing and joins distinguish exact, alias, global and unknown fixtures.

src/openultrasast/semantic/obligations/abstract_domain.py

@@ -1,19 +1,25 @@
-"""Evidence relations and the completeness value (access-control-prover, Req 11.1, 11.6, 11.7).
+"""Evidence relations, the completeness value and resource abstract values (access-control-prover).
+
+Covers Req 2.1, 2.5, 2.6, 2.7, 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
 from being used for the wrong quantifier: ``join_alternatives`` merges evidence from alternative call
 targets or control paths, ``conjoin_dimensions`` combines one witness's kind, scope, resource, authority
 and dominance dimensions, and ``aggregate_witnesses`` asks whether any witness definitely governs one
-obligation. Every operation is deterministic, pure and independent of target names; join never converts
+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
+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.abc import Iterable, Mapping
+from collections.abc import Iterable, Mapping, Sequence
 from dataclasses import dataclass
 from enum import Enum
+from typing import Literal
 
 
 class EvidenceRelation(Enum):
@@ -38,6 +44,70 @@ class Completeness:
         object.__setattr__(self, "reasons", tuple(dict.fromkeys(self.reasons)))
 
 
+_RESOURCE_KINDS = ("exact", "aliases", "request_global", "unknown")
+
+
+@dataclass(frozen=True)
+class ResourceRef:
+    """The abstract value of one resource binding (design, "Abstract evidence domain"; Req 2.1, 2.5, 2.6, 2.7, 11.1).
+
+    ``exact`` binds one named resource, ``aliases`` binds a finite set of them, ``request_global`` binds the
+    whole request without resource equality, and ``unknown`` is an unresolvable or unbounded binding. Values
+    are deduplicated and sorted, so equal bindings are equal however they were constructed; a misshapen kind
+    or arity fails loud rather than degrading silently.
+    """
+
+    kind: Literal["exact", "aliases", "request_global", "unknown"]
+    values: tuple[str, ...] = ()
+
+    def __post_init__(self) -> None:
+        if self.kind not in _RESOURCE_KINDS:
+            raise ValueError(f"unknown resource kind: {self.kind!r}")
+        tokens = sorted(set(self.values))
+        if self.kind == "exact" and len(tokens) != 1:
+            raise ValueError(f"exact resource needs exactly one token: {self.values!r}")
+        if self.kind == "aliases" and not tokens:
+            raise ValueError("alias set needs at least one token")
+        if self.kind in ("request_global", "unknown") and tokens:
+            raise ValueError(f"{self.kind} resource binds no tokens: {self.values!r}")
+        object.__setattr__(self, "values", tuple(tokens))
+
+
+REQUEST_GLOBAL_RESOURCE = ResourceRef(kind="request_global")
+UNKNOWN_RESOURCE = ResourceRef(kind="unknown")
+
+
+def parse_resource(binding: str | Sequence[str] | None) -> ResourceRef:
+    """Parse one resource binding from fact or IR evidence into its abstract value.
+
+    A single identifier token is ``exact``, a finite token collection is a finite alias set, and ``None``
+    (no binding could be resolved) is ``unknown``; anything misshapen raises instead of quietly degrading.
+    """
+    if binding is None:
+        return UNKNOWN_RESOURCE
+    tokens = (binding,) if isinstance(binding, str) else tuple(binding)
+    if not tokens or not all(isinstance(token, str) and token for token in tokens):
+        raise ValueError(f"misshapen resource binding: {binding!r}")
+    kind: Literal["exact", "aliases"] = "exact" if isinstance(binding, str) else "aliases"
+    return ResourceRef(kind=kind, values=tokens)
+
+
+def join_resources(left: ResourceRef, right: ResourceRef) -> ResourceRef:
+    """Join resource bindings from alternative paths or call targets.
+
+    Alias sets join by finite union and identical exact tokens stay exact; request-global scope absorbs any
+    concrete binding because it already covers every resource in the request (Req 2.6), and an unbounded or
+    unresolvable value joins to ``unknown`` so losing precision cannot manufacture an exact match (Req 2.7, 11.1).
+    """
+    if left.kind == "unknown" or right.kind == "unknown":
+        return UNKNOWN_RESOURCE
+    if left.kind == "request_global" or right.kind == "request_global":
+        return REQUEST_GLOBAL_RESOURCE
+    if left.kind == right.kind == "exact" and left.values == right.values:
+        return left
+    return ResourceRef(kind="aliases", values=left.values + right.values)
+
+
 _ALTERNATIVE_JOIN: Mapping[tuple[EvidenceRelation, EvidenceRelation], EvidenceRelation] = {
     (EvidenceRelation.MUST, EvidenceRelation.MUST): EvidenceRelation.MUST,
     (EvidenceRelation.MUST, EvidenceRelation.NO): EvidenceRelation.MAY,

src/openultrasast/semantic/obligations/facts.py

@@ -22,7 +22,18 @@ SENSITIVITIES = ("low", "medium", "high")
 DEFAULT_OBLIGATION_FACTS_DIR = Path(__file__).resolve().parents[2] / "ruleset" / "obligations"
 
 _OPERATION_FIELDS = frozenset(
-    {"id", "kind", "calls", "resource_arg", "requires", "sensitivity", "query_document_arg", "handlers", "framework"}
+    {
+        "id",
+        "kind",
+        "calls",
+        "resource_arg",
+        "requires",
+        "sensitivity",
+        "query_document_arg",
+        "handlers",
+        "framework",
+        "request_global_kinds",
+    }
 )
 _DISCHARGER_FIELDS = frozenset(
     {"id", "kind", "calls", "decorators", "identity_sources", "constraint_params", "request_sources", "permissive_values"}
@@ -50,6 +61,9 @@ class OperationFact:
     query_document_arg: int | None = None
     handlers: tuple[str, ...] = ()
     framework: str | None = None
+    # Requirement 2.6 (access-control-prover): discharger kinds a request-global witness may discharge for
+    # this operation at request scope, without resource equality. Declared by the fact, never inferred.
+    request_global_kinds: tuple[str, ...] = ()
 
 
 @dataclass(frozen=True)
@@ -97,48 +111,7 @@ def _load_obligation_facts_uncached(directory: Path | None = None) -> Obligation
         language = str(payload.get("language") or path.stem)
         versions.append(str(payload.get("version", "1")))
         for row in _rows(payload.get("operation"), path):
-            _only_fields(row, _OPERATION_FIELDS, path)
-            kind = str(row.get("kind", ""))
-            if kind not in OPERATION_KINDS:
-                raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown kind {kind!r}")
-            requires = _strings(row.get("requires"), "requires", path)
-            for item in requires:
-                if item not in DISCHARGER_KINDS:
-                    raise ObligationFactsError(f"{path}: operation {row.get('id')!r} requires unknown discharger kind {item!r}")
-            sensitivity = str(row.get("sensitivity", "medium"))
-            if sensitivity not in SENSITIVITIES:
-                raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown sensitivity {sensitivity!r}")
-            resource_arg = row.get("resource_arg")
-            if resource_arg is not None and not isinstance(resource_arg, int):
-                raise ObligationFactsError(f"{path}: operation {row.get('id')!r} resource_arg must be an integer")
-            document_arg = row.get("query_document_arg")
-            if document_arg is not None and (not isinstance(document_arg, int) or document_arg < 1):
-                raise ObligationFactsError(f"{path}: operation {row.get('id')!r} query_document_arg must be a positive integer")
-            handlers = _strings(row.get("handlers"), "handlers", path)
-            framework = row.get("framework")
-            if framework is not None and (not isinstance(framework, str) or not framework):
-                raise ObligationFactsError("invalid operation framework")
-            if handlers and framework is None:
-                raise ObligationFactsError("handler operation needs a framework")
-            for pattern in handlers:
-                try:
-                    re.compile(pattern)
-                except re.error as exc:
-                    raise ObligationFactsError(type(exc).__name__) from exc
-            operations.append(
-                OperationFact(
-                    id=str(row["id"]),
-                    kind=kind,
-                    language=language,
-                    calls=_strings(row.get("calls"), "calls", path),
-                    resource_arg=resource_arg,
-                    requires=requires,
-                    sensitivity=sensitivity,
-                    query_document_arg=document_arg,
-                    handlers=handlers,
-                    framework=framework,
-                )
-            )
+            operations.append(_operation_fact(row, path, language))
         for row in _rows(payload.get("discharger"), path):
             _only_fields(row, _DISCHARGER_FIELDS, path)
             kind = str(row.get("kind", ""))
@@ -160,6 +133,64 @@ def _load_obligation_facts_uncached(directory: Path | None = None) -> Obligation
     return ObligationFacts(version=versions[0] if versions else "1", operations=tuple(operations), dischargers=tuple(dischargers))
 
 
+def _operation_fact(row: dict[str, object], path: Path, language: str) -> OperationFact:
+    """Validate one operation row against the closed sets and parse it; any unknown kind or field fails loud."""
+    _only_fields(row, _OPERATION_FIELDS, path)
+    kind = str(row.get("kind", ""))
+    if kind not in OPERATION_KINDS:
+        raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown kind {kind!r}")
+    requires = _strings(row.get("requires"), "requires", path)
+    for item in requires:
+        if item not in DISCHARGER_KINDS:
+            raise ObligationFactsError(f"{path}: operation {row.get('id')!r} requires unknown discharger kind {item!r}")
+    sensitivity = str(row.get("sensitivity", "medium"))
+    if sensitivity not in SENSITIVITIES:
+        raise ObligationFactsError(f"{path}: operation {row.get('id')!r} has unknown sensitivity {sensitivity!r}")
+    request_global_kinds = _strings(row.get("request_global_kinds"), "request_global_kinds", path)
+    for item in request_global_kinds:
+        if item not in DISCHARGER_KINDS:
+            raise ObligationFactsError(f"{path}: operation {row.get('id')!r} request_global_kinds names unknown discharger kind {item!r}")
+    handler_patterns, handler_framework = _handler_shape(row, path)
+    return OperationFact(
+        id=str(row["id"]),
+        kind=kind,
+        language=language,
+        calls=_strings(row.get("calls"), "calls", path),
+        resource_arg=_optional_int(row, "resource_arg", path, positive=False),
+        requires=requires,
+        sensitivity=sensitivity,
+        query_document_arg=_optional_int(row, "query_document_arg", path, positive=True),
+        handlers=handler_patterns,
+        framework=handler_framework,
+        request_global_kinds=request_global_kinds,
+    )
+
+
+def _optional_int(row: dict[str, object], field: str, path: Path, *, positive: bool) -> int | None:
+    value = row.get(field)
+    if value is None:
+        return None
+    if not isinstance(value, int) or (positive and value < 1):
+        requirement = "a positive integer" if positive else "an integer"
+        raise ObligationFactsError(f"{path}: operation {row.get('id')!r} {field} must be {requirement}")
+    return value
+
+
+def _handler_shape(row: dict[str, object], path: Path) -> tuple[tuple[str, ...], str | None]:
+    handler_patterns = _strings(row.get("handlers"), "handlers", path)
+    framework = row.get("framework")
+    if framework is not None and (not isinstance(framework, str) or not framework):
+        raise ObligationFactsError("invalid operation framework")
+    if handler_patterns and framework is None:
+        raise ObligationFactsError("handler operation needs a framework")
+    for pattern in handler_patterns:
+        try:
+            re.compile(pattern)
+        except re.error as exc:
+            raise ObligationFactsError(type(exc).__name__) from exc
+    return handler_patterns, framework
+
+
 def _rows(value: object, path: Path) -> list[dict[str, object]]:
     if value is None:
         return []

tests/test_obligation_resource_domain.py

@@ -0,0 +1,222 @@
+"""access-control-prover task 7.2: resource abstract values and operation-fact sufficiency fields (offline).
+
+Exact resources, finite alias sets, request-global scope and unknown resources per the design's "Abstract
+evidence domain" section (Req 2.1, 2.5, 2.6, 2.7, 11.1), plus the additive operation-fact field that declares
+a request-global witness kind sufficient at request scope (Req 2.6).
+"""
+
+from __future__ import annotations
+
+import itertools
+from pathlib import Path
+
+import pytest
+
+
+def _resource_fixtures():
+    from openultrasast.semantic.obligations.abstract_domain import (
+        REQUEST_GLOBAL_RESOURCE,
+        UNKNOWN_RESOURCE,
+        ResourceRef,
+    )
+
+    return (
+        ResourceRef(kind="exact", values=("book",)),
+        ResourceRef(kind="exact", values=("volume",)),
+        ResourceRef(kind="aliases", values=("book", "volume")),
+        ResourceRef(kind="aliases", values=("volume", "shelf")),
+        REQUEST_GLOBAL_RESOURCE,
+        UNKNOWN_RESOURCE,
+    )
+
+
+_OPERATION_TOML = """version = "1"
+language = "python"
+
+[[operation]]
+id = "orm-read"
+kind = "protected_read"
+calls = ["filter_by"]
+requires = ["identity_constraint"]
+sensitivity = "high"
+request_global_kinds = ["path_guard"]
+"""
+
+
+def test_parse_resource_single_token_is_exact() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef, parse_resource
+
+    binding = parse_resource("book")
+    assert binding == ResourceRef(kind="exact", values=("book",))
+    assert binding.kind == "exact"
+    assert binding.values == ("book",)
+
+
+def test_parse_resource_token_collection_is_a_finite_alias_set() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef, parse_resource
+
+    binding = parse_resource(["volume", "book", "volume"])
+    assert binding == ResourceRef(kind="aliases", values=("book", "volume"))
+
+
+def test_parse_resource_without_a_binding_is_unknown() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_RESOURCE, parse_resource
+
+    binding = parse_resource(None)
+    assert binding == UNKNOWN_RESOURCE
+    assert binding.kind == "unknown"
+    assert binding.values == ()
+
+
+def test_request_global_resource_binds_the_whole_request() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import REQUEST_GLOBAL_RESOURCE
+
+    assert REQUEST_GLOBAL_RESOURCE.kind == "request_global"
+    assert REQUEST_GLOBAL_RESOURCE.values == ()
+
+
+def test_resource_kinds_distinguish_exact_alias_global_and_unknown() -> None:
+    # Req 2.7, 11.1: the four grades stay distinct; an unknown binding never collapses onto a concrete one.
+    from openultrasast.semantic.obligations.abstract_domain import (
+        REQUEST_GLOBAL_RESOURCE,
+        UNKNOWN_RESOURCE,
+        parse_resource,
+    )
+
+    grades = {parse_resource("book"), parse_resource(["book"]), REQUEST_GLOBAL_RESOURCE, UNKNOWN_RESOURCE}
+    assert {resource.kind for resource in grades} == {"exact", "aliases", "request_global", "unknown"}
+
+
+def test_alias_values_are_normalized_deterministically() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef
+
+    forward = ResourceRef(kind="aliases", values=("volume", "book", "volume"))
+    backward = ResourceRef(kind="aliases", values=("book", "volume"))
+    assert forward == backward
+    assert hash(forward) == hash(backward)
+    assert len({forward, backward}) == 1
+
+
+def test_resource_ref_fails_loud_on_misshapen_kinds_and_arities() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef
+
+    with pytest.raises(ValueError, match="sometimes"):
+        ResourceRef(kind="sometimes", values=("book",))
+    with pytest.raises(ValueError, match="exact"):
+        ResourceRef(kind="exact")
+    with pytest.raises(ValueError, match="exact"):
+        ResourceRef(kind="exact", values=("book", "volume"))
+    with pytest.raises(ValueError, match="alias"):
+        ResourceRef(kind="aliases", values=())
+    with pytest.raises(ValueError, match="request_global"):
+        ResourceRef(kind="request_global", values=("book",))
+
+
+def test_parse_resource_rejects_misshapen_bindings() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import parse_resource
+
+    with pytest.raises(ValueError):
+        parse_resource("")
+    with pytest.raises(ValueError):
+        parse_resource(())
+    with pytest.raises(ValueError):
+        parse_resource(["book", ""])
+
+
+def test_join_resources_keeps_identical_exact_tokens_exact() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources
+
+    binding = ResourceRef(kind="exact", values=("book",))
+    assert join_resources(binding, ResourceRef(kind="exact", values=("book",))) == binding
+
+
+def test_join_resources_merges_different_exact_tokens_into_an_alias_set() -> None:
+    # Req 2.5: a different resource never collapses onto one exact binding; it widens to the finite alias set.
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources
+
+    joined = join_resources(
+        ResourceRef(kind="exact", values=("book",)),
+        ResourceRef(kind="exact", values=("volume",)),
+    )
+    assert joined == ResourceRef(kind="aliases", values=("book", "volume"))
+
+
+def test_join_resources_adds_exact_tokens_into_alias_sets() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources
+
+    joined = join_resources(
+        ResourceRef(kind="exact", values=("shelf",)),
+        ResourceRef(kind="aliases", values=("book", "volume")),
+    )
+    assert joined == ResourceRef(kind="aliases", values=("book", "shelf", "volume"))
+
+
+def test_join_resources_unions_alias_sets_to_their_superset() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import ResourceRef, join_resources
+
+    subset = ResourceRef(kind="aliases", values=("book",))
+    superset = ResourceRef(kind="aliases", values=("book", "volume"))
+    assert join_resources(subset, superset) == superset
+    assert join_resources(superset, subset) == superset
+    disjoint = join_resources(subset, ResourceRef(kind="aliases", values=("volume",)))
+    assert disjoint == ResourceRef(kind="aliases", values=("book", "volume"))
+
+
+def test_join_resources_request_global_absorbs_concrete_bindings() -> None:
+    # Req 2.6: request-global scope already covers every resource in the request.
+    from openultrasast.semantic.obligations.abstract_domain import (
+        REQUEST_GLOBAL_RESOURCE,
+        ResourceRef,
+        join_resources,
+    )
+
+    for concrete in (
+        ResourceRef(kind="exact", values=("book",)),
+        ResourceRef(kind="aliases", values=("book", "volume")),
+    ):
+        assert join_resources(concrete, REQUEST_GLOBAL_RESOURCE) == REQUEST_GLOBAL_RESOURCE
+        assert join_resources(REQUEST_GLOBAL_RESOURCE, concrete) == REQUEST_GLOBAL_RESOURCE
+    assert join_resources(REQUEST_GLOBAL_RESOURCE, REQUEST_GLOBAL_RESOURCE) == REQUEST_GLOBAL_RESOURCE
+
+
+def test_join_resources_unknown_absorbs_every_fixture() -> None:
+    # Req 2.7, 11.1: an unresolvable binding stays unresolvable; joining cannot manufacture precision.
+    from openultrasast.semantic.obligations.abstract_domain import UNKNOWN_RESOURCE, join_resources
+
+    for other in _resource_fixtures():
+        assert join_resources(other, UNKNOWN_RESOURCE) == UNKNOWN_RESOURCE, other
+        assert join_resources(UNKNOWN_RESOURCE, other) == UNKNOWN_RESOURCE, other
+
+
+def test_join_resources_is_commutative_and_idempotent_over_fixtures() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import join_resources
+
+    fixtures = _resource_fixtures()
+    for left, right in itertools.product(fixtures, repeat=2):
+        assert join_resources(left, right) == join_resources(right, left), (left, right)
+    for resource in fixtures:
+        assert join_resources(resource, resource) == resource, resource
+
+
+def test_operation_fact_declares_request_global_sufficient_kinds(tmp_path: Path) -> None:
+    from openultrasast.semantic.obligations.facts import load_obligation_facts
+
+    (tmp_path / "python.toml").write_text(_OPERATION_TOML)
+    (row,) = load_obligation_facts(tmp_path).operations
+    assert row.request_global_kinds == ("path_guard",)
+
+
+def test_operation_fact_without_sufficiency_declares_none(tmp_path: Path) -> None:
+    from openultrasast.semantic.obligations.facts import load_obligation_facts
+
+    (tmp_path / "python.toml").write_text(_OPERATION_TOML.replace('request_global_kinds = ["path_guard"]\n', ""))
+    (row,) = load_obligation_facts(tmp_path).operations
+    assert row.request_global_kinds == ()
+
+
+def test_operation_fact_rejects_unknown_request_global_kind(tmp_path: Path) -> None:
+    from openultrasast.semantic.obligations.facts import ObligationFactsError, load_obligation_facts
+
+    (tmp_path / "python.toml").write_text(_OPERATION_TOML.replace('["path_guard"]', '["vibes"]'))
+    with pytest.raises(ObligationFactsError, match="vibes"):
+        load_obligation_facts(tmp_path)