feat(access-control-prover): task 7.4 - judgment, trace and coverage contracts with abstract state

src/openultrasast/hunt/prover.py

@@ -15,6 +15,7 @@ from ..semantic.cfg import ControlContext, FunctionCfg
 from ..semantic.cst import parse_function_nodes
 from ..semantic.facts import load_facts
 from ..semantic.ir import FileIR, FunctionIR, trailing_name
+from ..semantic.obligations.abstract_domain import PairJudgmentCounts
 from ..semantic.obligations.cfg_dominance import CfgDominance
 from ..semantic.obligations.check import _on_caller_hop, _relevant, _route_path, check_obligations
 from ..semantic.obligations.enforcement import witnesses
@@ -36,6 +37,10 @@ class Coverage:
     operations_checked: int
     operations_discharged: int
     unchecked_by_reason: dict[str, int]
+    # Requirement 7.1/7.6 (access-control-prover): three-way pair judgment totals, additive and zero
+    # until the prover opts into abstract judgment (task 10.6). Indeterminate pairs are counted
+    # neither clean nor discharged.
+    pair_judgments: PairJudgmentCounts = PairJudgmentCounts()
 
 
 @dataclass(frozen=True)

src/openultrasast/semantic/obligations/abstract_domain.py

@@ -1,6 +1,6 @@
 """Evidence relations, the completeness value, resource and authority abstract values (access-control-prover).
 
-Covers Req 2.1, 2.2, 2.5, 2.6, 2.7, 2.8, 11.1, 11.6, 11.7.
+Covers Req 2.1, 2.2, 2.5, 2.6, 2.7, 2.8, 7.1, 7.2, 7.5, 7.6, 9.1, 9.2, 9.6, 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
@@ -22,7 +22,7 @@ operation is deterministic, pure and independent of target names; join never con
 
 from __future__ import annotations
 
-from collections import deque
+from collections import Counter, deque
 from collections.abc import Iterable, Mapping, Sequence
 from dataclasses import dataclass
 from enum import Enum
@@ -37,6 +37,18 @@ class EvidenceRelation(Enum):
     UNKNOWN = "unknown"
 
 
+class PairJudgment(Enum):
+    """The three-way judgment of one examined pair (design, "Abstract evidence domain"; Req 4.1-4.3, 9.2).
+
+    Degraded evidence can reduce a pair to ``INDETERMINATE`` but can never manufacture
+    ``UNGUARDED`` or ``DISCHARGED``.
+    """
+
+    UNGUARDED = "unguarded"
+    DISCHARGED = "discharged"
+    INDETERMINATE = "indeterminate"
+
+
 @dataclass(frozen=True)
 class Completeness:
     """What the analysis could not decide; reasons are stage-prefixed strings, deduplicated in order.
@@ -352,3 +364,73 @@ def join_completeness(left: Completeness, right: Completeness) -> Completeness:
         is_complete=left.is_complete and right.is_complete,
         reasons=left.reasons + right.reasons,
     )
+
+
+@dataclass(frozen=True)
+class WitnessMatch:
+    """One witness's match relations for one obligation (design, "Witness matching and judgment"; Req 9.1).
+
+    ``relation`` is the conjoined kind/scope/dominance verdict, ``resource_relation`` and
+    ``authority_relation`` are the resource and authority compatibility relations, and ``evidence``
+    names the supporting fact identifiers (for example the authority implications used, Req 2.8).
+    """
+
+    relation: EvidenceRelation
+    resource_relation: EvidenceRelation
+    authority_relation: EvidenceRelation
+    evidence: tuple[str, ...]
+
+
+@dataclass(frozen=True)
+class PathJudgment:
+    """The abstract judgment of one examined path (design, "Witness matching and judgment"; Req 9.1, 11.4).
+
+    ``missing`` names every required obligation with no governing witness; ``completeness`` carries
+    each incompleteness reason of the path (Req 7.5) and ``matches`` holds one row per witness
+    examined. Computing these values is task 10.4; this is the contract they must fill.
+    """
+
+    judgment: PairJudgment
+    missing: tuple[str, ...]
+    completeness: Completeness
+    matches: tuple[WitnessMatch, ...]
+
+
+@dataclass(frozen=True)
+class PairJudgmentCounts:
+    """Pair judgment totals for failure-visible coverage (Req 7.1, 7.6).
+
+    ``indeterminate`` is a first-class count: an indeterminate pair is included in neither
+    ``unguarded`` nor ``discharged``, so a degraded instrument cannot read as a clean bill of health.
+    """
+
+    unguarded: int = 0
+    discharged: int = 0
+    indeterminate: int = 0
+
+    def examined(self) -> int:
+        """Examined pairs overall; the indeterminate rate is reported against this total (Req 7.6)."""
+        return self.unguarded + self.discharged + self.indeterminate
+
+
+def count_pair_judgments(judgments: Iterable[PairJudgment]) -> PairJudgmentCounts:
+    """Count the three pair judgments separately over one examined population (Req 7.1, 7.6)."""
+    counts = Counter(judgments)
+    return PairJudgmentCounts(
+        unguarded=counts[PairJudgment.UNGUARDED],
+        discharged=counts[PairJudgment.DISCHARGED],
+        indeterminate=counts[PairJudgment.INDETERMINATE],
+    )
+
+
+def reason_counts(completeness_values: Iterable[Completeness]) -> dict[str, int]:
+    """Aggregate every incompleteness reason across examined pairs (Req 7.2, 7.5).
+
+    Each pair contributes one count per distinct reason (``Completeness`` already deduplicates within
+    one value), so a reason two pairs share counts twice and no pair's reason is lost. Keys are
+    sorted, so the aggregate is deterministic however the pairs were ordered.
+    """
+    counts: Counter[str] = Counter()
+    for value in completeness_values:
+        counts.update(value.reasons)
+    return dict(sorted(counts.items()))

src/openultrasast/semantic/obligations/trace.py

@@ -7,10 +7,20 @@ import json
 import re
 from collections.abc import Mapping, Sequence
 from dataclasses import asdict, dataclass, replace
+from enum import Enum
 from typing import Any
 
 from ..cfg import ControlContext
 from ..ir import FileIR, FunctionIR, trailing_name
+from .abstract_domain import (
+    AuthorityRef,
+    Completeness,
+    EvidenceRelation,
+    PairJudgment,
+    PathJudgment,
+    ResourceRef,
+    WitnessMatch,
+)
 from .cfg_dominance import describe, operation_context
 from .dominance import Dominance
 from .facts import ObligationFacts
@@ -38,6 +48,73 @@ class Hop:
     forwarded: tuple[str, ...]
 
 
+@dataclass(frozen=True)
+class AbstractTraceState:
+    """The abstract evidence a prover-mode trace carries beyond the legacy verdict (Req 9.1, 9.2, 9.6).
+
+    ``path_judgment`` is the three-way judgment with its missing kinds, every incompleteness reason
+    and the per-witness match relations; ``resource`` and ``authority`` are the operation's abstract
+    values and ``resource_relation``/``authority_relation`` the pair-level compatibility relations.
+    The state is absent from legacy traces, which stay byte-stable (task 7.4).
+    """
+
+    path_judgment: PathJudgment
+    resource: ResourceRef
+    authority: AuthorityRef
+    resource_relation: EvidenceRelation
+    authority_relation: EvidenceRelation
+
+
+def _enum_json_value(value: Any) -> str:
+    """The canonical JSON encoding of a relation or judgment: its value string."""
+    if isinstance(value, Enum):
+        return str(value.value)
+    raise TypeError(f"not canonically serializable: {type(value).__name__}")
+
+
+def _parse_path_judgment(payload: Mapping[str, Any]) -> PathJudgment:
+    """Rebuild one ``PathJudgment`` from its canonical JSON (round-trip half of Req 9.5)."""
+    completeness_payload = payload["completeness"]
+    return PathJudgment(
+        judgment=PairJudgment(payload["judgment"]),
+        missing=tuple(payload["missing"]),
+        completeness=Completeness(
+            is_complete=bool(completeness_payload["is_complete"]),
+            reasons=tuple(completeness_payload["reasons"]),
+        ),
+        matches=tuple(
+            WitnessMatch(
+                relation=EvidenceRelation(match["relation"]),
+                resource_relation=EvidenceRelation(match["resource_relation"]),
+                authority_relation=EvidenceRelation(match["authority_relation"]),
+                evidence=tuple(match["evidence"]),
+            )
+            for match in payload["matches"]
+        ),
+    )
+
+
+def parse_abstract_state(payload: Mapping[str, Any]) -> AbstractTraceState:
+    """Rebuild the abstract trace state from its canonical JSON record.
+
+    The inverse of the canonical encoding: value strings name relations and judgments again, field
+    dicts become ``ResourceRef``/``AuthorityRef`` values and every incompleteness reason is kept.
+    Anything outside the closed vocabularies fails loud rather than degrading to a quieter value.
+    """
+    resource_payload = payload["resource"]
+    authority_payload = payload["authority"]
+    return AbstractTraceState(
+        path_judgment=_parse_path_judgment(payload["path_judgment"]),
+        resource=ResourceRef(kind=resource_payload["kind"], values=tuple(resource_payload["values"])),
+        authority=AuthorityRef(
+            values=tuple(authority_payload["values"]),
+            is_unknown=bool(authority_payload["is_unknown"]),
+        ),
+        resource_relation=EvidenceRelation(payload["resource_relation"]),
+        authority_relation=EvidenceRelation(payload["authority_relation"]),
+    )
+
+
 @dataclass(frozen=True)
 class Trace:
     entry_kind: str
@@ -54,14 +131,24 @@ class Trace:
     dominating: tuple[str, ...]
     missing: str | None
     operation_context: ControlContext = ControlContext()
+    # Opt-in abstract evidence (task 7.4): absent (None) in legacy mode, so legacy serialization is
+    # byte-stable; set only by the prover's abstract judgment path (task 10.6).
+    abstract_state: AbstractTraceState | None = None
 
     def record(self) -> dict[str, Any]:
-        """Return JSON values with keys sorted recursively, retaining sequence order."""
-        result: dict[str, Any] = json.loads(json.dumps(asdict(self), sort_keys=True))
-        return result
+        """Return JSON values with keys sorted recursively, retaining sequence order.
+
+        The abstract state is omitted entirely when unset, so a legacy trace's record keeps its exact
+        historical shape; when set, relations and judgments encode as their value strings.
+        """
+        payload = asdict(self)
+        if payload["abstract_state"] is None:
+            del payload["abstract_state"]
+        record: dict[str, Any] = json.loads(json.dumps(payload, sort_keys=True, default=_enum_json_value))
+        return record
 
     def text(self) -> str:
-        """Emit entry, hops, operation, later guards and verdict in that order."""
+        """Emit entry, hops, operation, later guards, verdict and, when present, the abstract state."""
         record = self.record()
         components = [("entry", {key: record[key] for key in ("entry_kind", "boundary", "access", "parameters")})]
         components.extend(("hop", hop) for hop in record["hops"])
@@ -69,6 +156,8 @@ class Trace:
         components.append(("operation", {key: record[key] for key in operation_keys}))
         components.extend(("guard_after", guard) for guard in record["guards_after"])
         components.append(("verdict", {key: record[key] for key in ("requires", "dominating", "missing")}))
+        if "abstract_state" in record:
+            components.append(("abstract", record["abstract_state"]))
         return "\n".join(f"{label} {json.dumps(value, sort_keys=True, separators=(',', ':'))}" for label, value in components)
 
 
@@ -168,6 +257,7 @@ def build_trace(
     dominating: tuple[str, ...],
     missing: str | None,
     access: str | None = None,
+    abstract_state: AbstractTraceState | None = None,
 ) -> Trace:
     """Build one trace without changing the checker's verdict or coverage."""
     texts = {file: text for file, (_, text) in irs.items()}
@@ -244,4 +334,5 @@ def build_trace(
         tuple(sorted(dominating)),
         missing,
         operation_context(dominance, operation),
+        abstract_state,
     )