107 lines
3.2 KiB
Python
107 lines
3.2 KiB
Python
|
|
"""Oracles evaluate claims and invariants and produce verdicts.
|
||
|
|
|
||
|
|
An oracle reads only the independent observation snapshot. It has no access to
|
||
|
|
the actor, to the driver, or to what either of them believes happened.
|
||
|
|
|
||
|
|
`INCONCLUSIVE` is a first-class outcome, not a failure mode of the framework. An
|
||
|
|
oracle that cannot support a judgment from the retained evidence must say so
|
||
|
|
rather than defaulting either way — silently defaulting to PASS hides defects,
|
||
|
|
and silently defaulting to FAIL trains people to ignore results.
|
||
|
|
"""
|
||
|
|
|
||
|
|
from __future__ import annotations
|
||
|
|
|
||
|
|
from dataclasses import dataclass, field
|
||
|
|
from enum import Enum
|
||
|
|
from typing import Any, Mapping
|
||
|
|
|
||
|
|
from .intent import Claim, Invariant
|
||
|
|
|
||
|
|
|
||
|
|
class Verdict(str, Enum):
|
||
|
|
PASS = "PASS"
|
||
|
|
FAIL = "FAIL"
|
||
|
|
SUSPICIOUS = "SUSPICIOUS"
|
||
|
|
INCONCLUSIVE = "INCONCLUSIVE"
|
||
|
|
|
||
|
|
|
||
|
|
@dataclass(frozen=True, slots=True)
|
||
|
|
class Judgment:
|
||
|
|
assertion_id: str
|
||
|
|
text: str
|
||
|
|
verdict: Verdict
|
||
|
|
step_id: str | None
|
||
|
|
detail: dict[str, Any] = field(default_factory=dict)
|
||
|
|
|
||
|
|
def as_dict(self) -> dict[str, Any]:
|
||
|
|
return {
|
||
|
|
"assertion_id": self.assertion_id,
|
||
|
|
"text": self.text,
|
||
|
|
"verdict": self.verdict.value,
|
||
|
|
"step_id": self.step_id,
|
||
|
|
"detail": self.detail,
|
||
|
|
}
|
||
|
|
|
||
|
|
|
||
|
|
class Oracle:
|
||
|
|
"""Deterministic evaluation of one assertion against an observation snapshot."""
|
||
|
|
|
||
|
|
def judge(
|
||
|
|
self,
|
||
|
|
assertion: Claim | Invariant,
|
||
|
|
snapshot: Mapping[str, Any],
|
||
|
|
step_id: str | None,
|
||
|
|
) -> Judgment:
|
||
|
|
if not snapshot:
|
||
|
|
return Judgment(
|
||
|
|
assertion.id,
|
||
|
|
assertion.text,
|
||
|
|
Verdict.INCONCLUSIVE,
|
||
|
|
step_id,
|
||
|
|
{"reason": "no observations were collected"},
|
||
|
|
)
|
||
|
|
try:
|
||
|
|
satisfied = assertion.predicate(snapshot)
|
||
|
|
except KeyError as missing:
|
||
|
|
# The evidence needed to judge this assertion was not collected.
|
||
|
|
# That is an evidence failure, never a pass and never a fail.
|
||
|
|
return Judgment(
|
||
|
|
assertion.id,
|
||
|
|
assertion.text,
|
||
|
|
Verdict.INCONCLUSIVE,
|
||
|
|
step_id,
|
||
|
|
{"reason": f"required observation {missing} missing from snapshot"},
|
||
|
|
)
|
||
|
|
except Exception as exc:
|
||
|
|
return Judgment(
|
||
|
|
assertion.id,
|
||
|
|
assertion.text,
|
||
|
|
Verdict.INCONCLUSIVE,
|
||
|
|
step_id,
|
||
|
|
{"reason": f"predicate raised {type(exc).__name__}: {exc}"},
|
||
|
|
)
|
||
|
|
return Judgment(
|
||
|
|
assertion.id,
|
||
|
|
assertion.text,
|
||
|
|
Verdict.PASS if satisfied else Verdict.FAIL,
|
||
|
|
step_id,
|
||
|
|
)
|
||
|
|
|
||
|
|
|
||
|
|
def overall(judgments: list[Judgment]) -> Verdict:
|
||
|
|
"""Aggregate run verdict.
|
||
|
|
|
||
|
|
FAIL dominates; INCONCLUSIVE outranks PASS. A run containing an unjudgeable
|
||
|
|
assertion has not passed, whatever else it did.
|
||
|
|
"""
|
||
|
|
verdicts = {j.verdict for j in judgments}
|
||
|
|
if not judgments:
|
||
|
|
return Verdict.INCONCLUSIVE
|
||
|
|
if Verdict.FAIL in verdicts:
|
||
|
|
return Verdict.FAIL
|
||
|
|
if Verdict.INCONCLUSIVE in verdicts:
|
||
|
|
return Verdict.INCONCLUSIVE
|
||
|
|
if Verdict.SUSPICIOUS in verdicts:
|
||
|
|
return Verdict.SUSPICIOUS
|
||
|
|
return Verdict.PASS
|