Reasoning (guardrail_solver.reasoning)

The explanation DAG, the SMT helpers, the forward derivation rules, puzzle solving, and Mermaid rendering. See How reasoning works for the narrative.

reasoning

The reasoning engine, re-exported as a stable public surface.

The engine lives in :mod:._python, with rendering split out into :mod:.renderers (.renderers.mermaid, .renderers.d3, .renderers.markdown); this package keeps the public import path (guardrail_solver.reasoning.X) stable so a sibling backend can be slotted in behind it later without touching callers.

ENTAILS_NOTARY module-attribute

ENTAILS_NOTARY = EntailsNotary()

DEFAULT_SOLVER_TIMEOUT_MS module-attribute

DEFAULT_SOLVER_TIMEOUT_MS = 30000

Z3_ALGEBRA module-attribute

Z3_ALGEBRA = Z3ExpressionAlgebra()

Z3_SEMANTICS module-attribute

Z3_SEMANTICS = Z3SemanticBackend(
    timeout_ms=DEFAULT_SOLVER_TIMEOUT_MS
)

DEFAULT_REASONING_BACKEND module-attribute

DEFAULT_REASONING_BACKEND = default_reasoning_backend()

ingest_puzzle module-attribute

ingest_puzzle = ingest

solve_puzzle module-attribute

solve_puzzle = PuzzleSolver()

RecordProposal

RecordProposal = VarEqConst | VarEqVar

Derivation dataclass

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class Derivation:
    premise_ids: tuple[FactId, ...]
    rule: str

premise_ids instance-attribute

premise_ids

rule instance-attribute

rule

ProvenanceDag dataclass

Bases: Generic[ExprT]

Typed boundary around the heterogeneous provenance rustworkx DAG.

rustworkx has no freeze() equivalent, so immutability is by convention, not by runtime guard: every mutating method below builds a fresh .copy() (via to_rustworkx) and never touches self._graph or self._index_by_id in place.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class ProvenanceDag(Generic[ExprT]):
    """Typed boundary around the heterogeneous provenance rustworkx DAG.

    rustworkx has no ``freeze()`` equivalent, so immutability is by convention,
    not by runtime guard: every mutating method below builds a fresh
    ``.copy()`` (via ``to_rustworkx``) and never touches ``self._graph`` or
    ``self._index_by_id`` in place.
    """

    _graph: ProvenanceGraph[ExprT] = field(
        default_factory=empty_rustworkx_digraph, repr=False
    )
    _index_by_id: Mapping[GraphNodeId, int] = field(default_factory=dict, repr=False)

    @classmethod
    def from_rustworkx(
        cls, graph: rx.PyDiGraph[ProvenanceNode[ExprT], None]
    ) -> ProvenanceDag[ExprT]:
        """Copy, validate, and adopt a raw interoperability graph."""
        copied = graph.copy()
        index_by_id: dict[GraphNodeId, int] = {}
        for idx in copied.node_indices():
            # `rustworkx` payloads are untyped only because nothing declares
            # what this graph carries. This one carries exactly the three
            # node kinds `add_node` is ever given, all of which declare
            # `id`, so the boundary can name them and reject anything else
            # instead of probing every payload for an attribute.
            # `ExplanationNode` belongs here with the other two: leaving it
            # out left a saturated graph's explanations unindexed, so a
            # round-tripped graph raised `KeyError` from `explanation_lines`.
            data = copied.get_node_data(idx)
            if isinstance(data, FactNode | DerivationNode | ExplanationNode) and (
                data.id not in index_by_id
            ):
                index_by_id[data.id] = idx
        result = cls(_graph=copied, _index_by_id=index_by_id)
        result.validate()
        return result

    def to_rustworkx(self) -> ProvenanceGraph[ExprT]:
        """Return a mutable copy for explicit interoperability boundaries."""
        return self._graph.copy()

    def _replace_graph(
        self, graph: ProvenanceGraph[ExprT], index_by_id: Mapping[GraphNodeId, int]
    ) -> ProvenanceDag[ExprT]:
        return replace(self, _graph=graph, _index_by_id=index_by_id)

    def validate(self) -> None:
        """Establish the complete typed provenance topology at one boundary."""
        if not _rustworkx().is_directed_acyclic_graph(self._graph):
            raise ValueError("Provenance graph must be acyclic.")

        for idx in self._graph.node_indices():
            payload = self._graph.get_node_data(idx)
            if not isinstance(payload, (FactNode, DerivationNode, ExplanationNode)):
                raise TypeError(f"Unknown node payload: index {idx}")

        seen_ids: set[GraphNodeId] = set()
        for idx in self._graph.node_indices():
            node_id = self._graph.get_node_data(idx).id
            if node_id in seen_ids:
                raise ValueError(f"Duplicate node id: {node_id}")
            seen_ids.add(node_id)

        for source_idx, target_idx in self._graph.edge_list():
            source = self._graph.get_node_data(source_idx)
            target = self._graph.get_node_data(target_idx)
            source_is_fact = isinstance(source, FactNode)
            target_is_fact = isinstance(target, FactNode)
            if source_is_fact == target_is_fact:
                raise ValueError(f"Invalid provenance edge: {source.id} -> {target.id}")
            if isinstance(source, FactNode) and source.kind is FactKind.CHECK:
                raise ValueError(f"Checks cannot be premises: {source.id}")

        for idx in self._graph.node_indices():
            payload = self._graph.get_node_data(idx)
            if isinstance(payload, FactNode):
                continue

            successor_indices = self._graph.successor_indices(idx)
            if len(successor_indices) > 1:
                raise ValueError(
                    f"Provenance steps conclude at most one fact: {payload.id}"
                )
            # Bound once and tested on that binding. Fetching twice and checking
            # the other call left both unnarrowed, which is why reading
            # `conclusion.kind` below needed the payload type to be `Any`.
            conclusion = (
                self._graph.get_node_data(successor_indices[0])
                if len(successor_indices) == 1
                else None
            )
            if conclusion is None:
                # A step may conclude nothing -- a conflict cites the givens
                # that cannot all hold and establishes no fact -- but only a
                # derivation, and only one that cites something. An
                # explanation is by definition about a check, and a box with
                # nothing on either side of it says nothing at all.
                if isinstance(payload, ExplanationNode):
                    raise ValueError(f"Explanations must conclude checks: {payload.id}")
                if not self._graph.predecessor_indices(idx):
                    raise ValueError(
                        "A step that concludes nothing must cite something: "
                        f"{payload.id}"
                    )
                continue
            # A successor of a step is a fact: the edge check above already
            # refused step-to-step, so there is no arm here for anything else.
            assert isinstance(conclusion, FactNode)
            if isinstance(payload, DerivationNode):
                if conclusion.kind is FactKind.CHECK:
                    raise ValueError(
                        f"Derivations cannot conclude checks: {payload.id}"
                    )
            elif conclusion.kind is not FactKind.CHECK:
                raise ValueError(f"Explanations must conclude checks: {payload.id}")

    def __contains__(self, node_id: GraphNodeId) -> bool:
        return node_id in self._index_by_id

    def _required_payload[PayloadT](
        self,
        node_id: GraphNodeId,
        payload_type: type[PayloadT],
        label: str,
    ) -> PayloadT:
        payload = self._graph.get_node_data(self._index_by_id[node_id])
        if not isinstance(payload, payload_type):
            raise TypeError(f"Not a {label} node: {node_id}")
        return payload

    def fact(self, fact_id: FactId) -> FactNode[ExprT]:
        return self._required_payload(fact_id, FactNode, "fact")

    def derivation(self, derivation_id: DerivationId) -> DerivationNode:
        return self._required_payload(derivation_id, DerivationNode, "derivation")

    def explanation(self, step_id: DerivationId) -> ExplanationNode:
        return self._required_payload(step_id, ExplanationNode, "explanation")

    def facts(self) -> Mapping[FactId, FactNode[ExprT]]:
        return {node.id: node for node in self.nodes() if isinstance(node, FactNode)}

    def derivation_nodes(self) -> Mapping[DerivationId, DerivationNode]:
        return {
            node.id: node for node in self.nodes() if isinstance(node, DerivationNode)
        }

    def nodes(self) -> Iterator[ProvenanceNode[ExprT]]:
        for idx in self._graph.node_indices():
            yield self._graph.get_node_data(idx)

    def edges(self) -> Iterator[tuple[GraphNodeId, GraphNodeId]]:
        """Yield edges grouped by source in node-creation order.

        ``rx.PyDiGraph.edge_list()`` orders by raw edge-insertion time, which
        depends on incidental construction order rather than graph content —
        two structurally equivalent graphs built in a different sequence (or
        via a different backend) could yield edges differently, changing
        renderer output for no semantic reason. Iterating nodes in creation
        order, then each node's own successors, is canonical: it depends only
        on stable node identity (assigned once, at creation), not on when an
        edge happened to be added.
        """
        graph = self._graph
        for source_idx in graph.node_indices():
            source_id = graph.get_node_data(source_idx).id
            # rustworkx yields successors in reverse edge-insertion order;
            # reverse back for a stable, content-derived order.
            for target_idx in reversed(graph.successor_indices(source_idx)):
                yield source_id, graph.get_node_data(target_idx).id

    def in_degree(self, fact_id: FactId) -> int:
        return int(self._graph.in_degree(self._index_by_id[fact_id]))

    def has_edge(self, source: GraphNodeId, target: GraphNodeId) -> bool:
        source_idx = self._index_by_id.get(source)
        target_idx = self._index_by_id.get(target)
        if source_idx is None or target_idx is None:
            return False
        return self._graph.has_edge(source_idx, target_idx)

    def premises_of(self, step_id: GraphNodeId) -> Iterator[FactId]:
        """The facts a step rests on, in the order they were added."""
        return self._fact_predecessors(step_id)

    def successors(self, node_id: GraphNodeId) -> Iterator[GraphNodeId]:
        """The nodes this one points at, in edge-insertion order."""
        indices = reversed(self._graph.successor_indices(self._index_by_id[node_id]))
        return (self._graph.get_node_data(idx).id for idx in indices)

    def _fact_predecessors(self, node_id: GraphNodeId) -> Iterator[FactId]:
        graph = self._graph
        # rustworkx yields predecessors in reverse edge-insertion order;
        # reverse back so premise order matches the order they were added in.
        indices = reversed(graph.predecessor_indices(self._index_by_id[node_id]))
        # One lookup per node, and the `isinstance` tests the same binding it
        # then reads `.id` from -- so the element type is `FactId` rather than
        # the full payload union with a cast over it.
        payloads = (graph.get_node_data(idx) for idx in indices)
        return (payload.id for payload in payloads if isinstance(payload, FactNode))

    def explanation_node_ids(
        self,
        target_id: FactId,
    ) -> frozenset[GraphNodeId]:
        """Return the target and every provenance node contributing to it."""
        if target_id not in self._index_by_id:
            raise KeyError(f"Unknown fact id: {target_id}")

        ancestor_indices = _rustworkx().ancestors(
            self._graph, self._index_by_id[target_id]
        )
        ancestor_ids = {self._graph.get_node_data(i).id for i in ancestor_indices}
        return frozenset(ancestor_ids | {target_id})

    def derivations(self) -> Mapping[FactId, tuple[Derivation, ...]]:
        result: dict[FactId, list[Derivation]] = {}
        for derivation_id, derivation in self.derivation_nodes().items():
            premise_ids = tuple(self._fact_predecessors(derivation_id))
            successor_indices = self._graph.successor_indices(
                self._index_by_id[derivation_id]
            )
            conclusion = self._graph.get_node_data(next(iter(successor_indices)))
            # `validate()` refuses any derivation whose single successor is not a
            # fact, at construction, so this cannot fire. Asserted rather than
            # cast: it names the invariant being relied on, and fails loudly if
            # that guarantee ever moves.
            assert isinstance(conclusion, FactNode), (
                f"derivation {derivation_id} concludes a non-fact"
            )
            result.setdefault(conclusion.id, []).append(
                Derivation(premise_ids=premise_ids, rule=derivation.rule)
            )
        return {fact_id: tuple(items) for fact_id, items in result.items()}

    def reaches_any(self, source: FactId, targets: Iterable[FactId]) -> bool:
        """True when ``source`` is, or has a directed path to, any ``target``."""
        descendant_indices = _rustworkx().descendants(
            self._graph, self._index_by_id[source]
        )
        descendant_ids = {
            self._graph.get_node_data(idx).id for idx in descendant_indices
        }
        return any(target == source or target in descendant_ids for target in targets)

    def has_derivation(
        self,
        *,
        conclusion_id: FactId,
        premise_ids: tuple[FactId, ...],
        rule: str,
    ) -> bool:
        expected_premises = set(premise_ids)
        for predecessor_idx in self._graph.predecessor_indices(
            self._index_by_id[conclusion_id]
        ):
            predecessor = self._graph.get_node_data(predecessor_idx)
            if not isinstance(predecessor, DerivationNode):
                continue
            if predecessor.rule != rule:
                continue
            actual_premises = set(self._fact_predecessors(predecessor.id))
            if actual_premises == expected_premises:
                return True
        return False

    def with_fact(
        self,
        node: FactNode[ExprT],
        *,
        derivation: DerivationNode | None = None,
        premises: tuple[FactId, ...] = (),
    ) -> ProvenanceDag[ExprT]:
        graph = self.to_rustworkx()
        index_by_id = dict(self._index_by_id)
        index_by_id[node.id] = graph.add_node(node)
        if derivation is not None:
            return self._with_step(
                derivation,
                premises=premises,
                conclusion=node.id,
                graph=graph,
                index_by_id=index_by_id,
            )
        return self._replace_graph(graph, index_by_id)

    def _with_step(
        self,
        step: DerivationNode | ExplanationNode,
        *,
        premises: tuple[FactId, ...],
        conclusion: FactId | None,
        graph: ProvenanceGraph[ExprT] | None = None,
        index_by_id: Mapping[GraphNodeId, int] | None = None,
    ) -> ProvenanceDag[ExprT]:
        graph = self.to_rustworkx() if graph is None else graph
        index_by_id = dict(self._index_by_id if index_by_id is None else index_by_id)
        step_idx = graph.add_node(step)
        index_by_id[step.id] = step_idx
        for premise in premises:
            graph.add_edge(index_by_id[premise], step_idx, None)
        if conclusion is not None:
            graph.add_edge(step_idx, index_by_id[conclusion], None)
        return self._replace_graph(graph, index_by_id)

    def with_derivation(
        self,
        derivation: DerivationNode,
        *,
        premises: tuple[FactId, ...],
        conclusion: FactId | None,
    ) -> ProvenanceDag[ExprT]:
        """Add a forward step, or one that concludes nothing.

        ``conclusion=None`` is a step with premises and no result: an
        inconsistent base's conflict, which cites the givens that cannot all
        hold and establishes nothing, because an edge into the check would
        draw it as decided in a world that does not exist. The step is what
        it always was on the wire; until 2026-09-19 this type could not hold
        it, so an `INCONSISTENT_BASE` response could not be rebuilt at all.
        """
        return self._with_step(
            derivation,
            premises=premises,
            conclusion=conclusion,
        )

    def with_explanation(
        self,
        explanation: ExplanationNode,
        *,
        premises: tuple[FactId, ...],
        check: FactId,
    ) -> ProvenanceDag[ExprT]:
        return self._with_step(
            explanation,
            premises=premises,
            conclusion=check,
        )

    def explanation_nodes(self, target_id: FactId) -> Iterator[ProvenanceNode[ExprT]]:
        relevant_ids = self.explanation_node_ids(target_id)
        relevant_indices = [self._index_by_id[node_id] for node_id in relevant_ids]
        sub = self._graph.subgraph(relevant_indices)
        for idx in _rustworkx().topological_sort(sub):
            payload = sub.get_node_data(idx)
            if isinstance(payload, FactNode):
                yield self.fact(payload.id)
            elif isinstance(payload, DerivationNode):
                yield self.derivation(payload.id)
            else:
                yield self.explanation(payload.id)

    def slice_for(self, target_id: FactId) -> ProvenanceDag[ExprT]:
        relevant_ids = self.explanation_node_ids(target_id)
        return self._sub_dag(relevant_ids)

    def _step_predecessors(
        self, fact_id: FactId
    ) -> Iterator[DerivationNode | ExplanationNode]:
        """The steps that establish ``fact_id``, in edge-insertion order."""
        indices = reversed(self._graph.predecessor_indices(self._index_by_id[fact_id]))
        payloads = (self._graph.get_node_data(idx) for idx in indices)
        return (
            payload
            for payload in payloads
            if isinstance(payload, (DerivationNode, ExplanationNode))
        )

    def _sub_dag(self, node_ids: Collection[GraphNodeId]) -> ProvenanceDag[ExprT]:
        sub = self._graph.subgraph([self._index_by_id[one] for one in node_ids])
        index_by_id = {sub.get_node_data(idx).id: idx for idx in sub.node_indices()}
        return self._replace_graph(sub, index_by_id)

    def proof_for(self, target_id: FactId) -> ProvenanceDag[ExprT]:
        """One route to ``target_id``: the slice, with one step per fact.

        Saturation reaches a fact by every route the rules allow, and the
        provenance records them all -- `relay-chain`'s second departure is
        derived both from the givens directly and from the first departure
        once that was derived. Both are true, and a reader shown both is
        shown the same conclusion twice with no way to tell which reading is
        the one to follow.

        So a *proof* keeps one: walking back from the target, each fact keeps
        the step with the fewest ancestors -- the shortest route to it -- and
        only that step's premises are then needed. Ties go to the step whose
        id sorts first, so the same graph always yields the same proof and a
        renderer's output does not move under it.

        `slice_for` stays the faithful answer, and is what a question about
        provenance gets; this is what a question about the explanation gets.
        """
        ancestors = _rustworkx().ancestors
        within = self.explanation_node_ids(target_id)

        def reach(step: DerivationNode | ExplanationNode) -> int:
            indices = ancestors(self._graph, self._index_by_id[step.id])
            return len({self._graph.get_node_data(one).id for one in indices} & within)

        kept: set[GraphNodeId] = set()
        pending: list[FactId] = [target_id]
        while pending:
            fact = pending.pop()
            if fact in kept:
                continue
            kept.add(fact)
            steps = [one for one in self._step_predecessors(fact) if one.id in within]
            if not steps:
                continue
            chosen = min(steps, key=lambda step: (reach(step), str(step.id)))
            kept.add(chosen.id)
            pending.extend(self._fact_predecessors(chosen.id))
        return self._sub_dag(kept)

from_rustworkx classmethod

from_rustworkx(graph)

Copy, validate, and adopt a raw interoperability graph.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@classmethod
def from_rustworkx(
    cls, graph: rx.PyDiGraph[ProvenanceNode[ExprT], None]
) -> ProvenanceDag[ExprT]:
    """Copy, validate, and adopt a raw interoperability graph."""
    copied = graph.copy()
    index_by_id: dict[GraphNodeId, int] = {}
    for idx in copied.node_indices():
        # `rustworkx` payloads are untyped only because nothing declares
        # what this graph carries. This one carries exactly the three
        # node kinds `add_node` is ever given, all of which declare
        # `id`, so the boundary can name them and reject anything else
        # instead of probing every payload for an attribute.
        # `ExplanationNode` belongs here with the other two: leaving it
        # out left a saturated graph's explanations unindexed, so a
        # round-tripped graph raised `KeyError` from `explanation_lines`.
        data = copied.get_node_data(idx)
        if isinstance(data, FactNode | DerivationNode | ExplanationNode) and (
            data.id not in index_by_id
        ):
            index_by_id[data.id] = idx
    result = cls(_graph=copied, _index_by_id=index_by_id)
    result.validate()
    return result

to_rustworkx

to_rustworkx()

Return a mutable copy for explicit interoperability boundaries.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def to_rustworkx(self) -> ProvenanceGraph[ExprT]:
    """Return a mutable copy for explicit interoperability boundaries."""
    return self._graph.copy()

validate

validate()

Establish the complete typed provenance topology at one boundary.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def validate(self) -> None:
    """Establish the complete typed provenance topology at one boundary."""
    if not _rustworkx().is_directed_acyclic_graph(self._graph):
        raise ValueError("Provenance graph must be acyclic.")

    for idx in self._graph.node_indices():
        payload = self._graph.get_node_data(idx)
        if not isinstance(payload, (FactNode, DerivationNode, ExplanationNode)):
            raise TypeError(f"Unknown node payload: index {idx}")

    seen_ids: set[GraphNodeId] = set()
    for idx in self._graph.node_indices():
        node_id = self._graph.get_node_data(idx).id
        if node_id in seen_ids:
            raise ValueError(f"Duplicate node id: {node_id}")
        seen_ids.add(node_id)

    for source_idx, target_idx in self._graph.edge_list():
        source = self._graph.get_node_data(source_idx)
        target = self._graph.get_node_data(target_idx)
        source_is_fact = isinstance(source, FactNode)
        target_is_fact = isinstance(target, FactNode)
        if source_is_fact == target_is_fact:
            raise ValueError(f"Invalid provenance edge: {source.id} -> {target.id}")
        if isinstance(source, FactNode) and source.kind is FactKind.CHECK:
            raise ValueError(f"Checks cannot be premises: {source.id}")

    for idx in self._graph.node_indices():
        payload = self._graph.get_node_data(idx)
        if isinstance(payload, FactNode):
            continue

        successor_indices = self._graph.successor_indices(idx)
        if len(successor_indices) > 1:
            raise ValueError(
                f"Provenance steps conclude at most one fact: {payload.id}"
            )
        # Bound once and tested on that binding. Fetching twice and checking
        # the other call left both unnarrowed, which is why reading
        # `conclusion.kind` below needed the payload type to be `Any`.
        conclusion = (
            self._graph.get_node_data(successor_indices[0])
            if len(successor_indices) == 1
            else None
        )
        if conclusion is None:
            # A step may conclude nothing -- a conflict cites the givens
            # that cannot all hold and establishes no fact -- but only a
            # derivation, and only one that cites something. An
            # explanation is by definition about a check, and a box with
            # nothing on either side of it says nothing at all.
            if isinstance(payload, ExplanationNode):
                raise ValueError(f"Explanations must conclude checks: {payload.id}")
            if not self._graph.predecessor_indices(idx):
                raise ValueError(
                    "A step that concludes nothing must cite something: "
                    f"{payload.id}"
                )
            continue
        # A successor of a step is a fact: the edge check above already
        # refused step-to-step, so there is no arm here for anything else.
        assert isinstance(conclusion, FactNode)
        if isinstance(payload, DerivationNode):
            if conclusion.kind is FactKind.CHECK:
                raise ValueError(
                    f"Derivations cannot conclude checks: {payload.id}"
                )
        elif conclusion.kind is not FactKind.CHECK:
            raise ValueError(f"Explanations must conclude checks: {payload.id}")

fact

fact(fact_id)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def fact(self, fact_id: FactId) -> FactNode[ExprT]:
    return self._required_payload(fact_id, FactNode, "fact")

derivation

derivation(derivation_id)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def derivation(self, derivation_id: DerivationId) -> DerivationNode:
    return self._required_payload(derivation_id, DerivationNode, "derivation")

explanation

explanation(step_id)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def explanation(self, step_id: DerivationId) -> ExplanationNode:
    return self._required_payload(step_id, ExplanationNode, "explanation")

facts

facts()

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def facts(self) -> Mapping[FactId, FactNode[ExprT]]:
    return {node.id: node for node in self.nodes() if isinstance(node, FactNode)}

derivation_nodes

derivation_nodes()

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def derivation_nodes(self) -> Mapping[DerivationId, DerivationNode]:
    return {
        node.id: node for node in self.nodes() if isinstance(node, DerivationNode)
    }

nodes

nodes()

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def nodes(self) -> Iterator[ProvenanceNode[ExprT]]:
    for idx in self._graph.node_indices():
        yield self._graph.get_node_data(idx)

edges

edges()

Yield edges grouped by source in node-creation order.

rx.PyDiGraph.edge_list() orders by raw edge-insertion time, which depends on incidental construction order rather than graph content — two structurally equivalent graphs built in a different sequence (or via a different backend) could yield edges differently, changing renderer output for no semantic reason. Iterating nodes in creation order, then each node's own successors, is canonical: it depends only on stable node identity (assigned once, at creation), not on when an edge happened to be added.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def edges(self) -> Iterator[tuple[GraphNodeId, GraphNodeId]]:
    """Yield edges grouped by source in node-creation order.

    ``rx.PyDiGraph.edge_list()`` orders by raw edge-insertion time, which
    depends on incidental construction order rather than graph content —
    two structurally equivalent graphs built in a different sequence (or
    via a different backend) could yield edges differently, changing
    renderer output for no semantic reason. Iterating nodes in creation
    order, then each node's own successors, is canonical: it depends only
    on stable node identity (assigned once, at creation), not on when an
    edge happened to be added.
    """
    graph = self._graph
    for source_idx in graph.node_indices():
        source_id = graph.get_node_data(source_idx).id
        # rustworkx yields successors in reverse edge-insertion order;
        # reverse back for a stable, content-derived order.
        for target_idx in reversed(graph.successor_indices(source_idx)):
            yield source_id, graph.get_node_data(target_idx).id

in_degree

in_degree(fact_id)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def in_degree(self, fact_id: FactId) -> int:
    return int(self._graph.in_degree(self._index_by_id[fact_id]))

has_edge

has_edge(source, target)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def has_edge(self, source: GraphNodeId, target: GraphNodeId) -> bool:
    source_idx = self._index_by_id.get(source)
    target_idx = self._index_by_id.get(target)
    if source_idx is None or target_idx is None:
        return False
    return self._graph.has_edge(source_idx, target_idx)

premises_of

premises_of(step_id)

The facts a step rests on, in the order they were added.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def premises_of(self, step_id: GraphNodeId) -> Iterator[FactId]:
    """The facts a step rests on, in the order they were added."""
    return self._fact_predecessors(step_id)

successors

successors(node_id)

The nodes this one points at, in edge-insertion order.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def successors(self, node_id: GraphNodeId) -> Iterator[GraphNodeId]:
    """The nodes this one points at, in edge-insertion order."""
    indices = reversed(self._graph.successor_indices(self._index_by_id[node_id]))
    return (self._graph.get_node_data(idx).id for idx in indices)

explanation_node_ids

explanation_node_ids(target_id)

Return the target and every provenance node contributing to it.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def explanation_node_ids(
    self,
    target_id: FactId,
) -> frozenset[GraphNodeId]:
    """Return the target and every provenance node contributing to it."""
    if target_id not in self._index_by_id:
        raise KeyError(f"Unknown fact id: {target_id}")

    ancestor_indices = _rustworkx().ancestors(
        self._graph, self._index_by_id[target_id]
    )
    ancestor_ids = {self._graph.get_node_data(i).id for i in ancestor_indices}
    return frozenset(ancestor_ids | {target_id})

derivations

derivations()

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def derivations(self) -> Mapping[FactId, tuple[Derivation, ...]]:
    result: dict[FactId, list[Derivation]] = {}
    for derivation_id, derivation in self.derivation_nodes().items():
        premise_ids = tuple(self._fact_predecessors(derivation_id))
        successor_indices = self._graph.successor_indices(
            self._index_by_id[derivation_id]
        )
        conclusion = self._graph.get_node_data(next(iter(successor_indices)))
        # `validate()` refuses any derivation whose single successor is not a
        # fact, at construction, so this cannot fire. Asserted rather than
        # cast: it names the invariant being relied on, and fails loudly if
        # that guarantee ever moves.
        assert isinstance(conclusion, FactNode), (
            f"derivation {derivation_id} concludes a non-fact"
        )
        result.setdefault(conclusion.id, []).append(
            Derivation(premise_ids=premise_ids, rule=derivation.rule)
        )
    return {fact_id: tuple(items) for fact_id, items in result.items()}

reaches_any

reaches_any(source, targets)

True when source is, or has a directed path to, any target.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def reaches_any(self, source: FactId, targets: Iterable[FactId]) -> bool:
    """True when ``source`` is, or has a directed path to, any ``target``."""
    descendant_indices = _rustworkx().descendants(
        self._graph, self._index_by_id[source]
    )
    descendant_ids = {
        self._graph.get_node_data(idx).id for idx in descendant_indices
    }
    return any(target == source or target in descendant_ids for target in targets)

has_derivation

has_derivation(*, conclusion_id, premise_ids, rule)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def has_derivation(
    self,
    *,
    conclusion_id: FactId,
    premise_ids: tuple[FactId, ...],
    rule: str,
) -> bool:
    expected_premises = set(premise_ids)
    for predecessor_idx in self._graph.predecessor_indices(
        self._index_by_id[conclusion_id]
    ):
        predecessor = self._graph.get_node_data(predecessor_idx)
        if not isinstance(predecessor, DerivationNode):
            continue
        if predecessor.rule != rule:
            continue
        actual_premises = set(self._fact_predecessors(predecessor.id))
        if actual_premises == expected_premises:
            return True
    return False

with_fact

with_fact(node, *, derivation=None, premises=())

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def with_fact(
    self,
    node: FactNode[ExprT],
    *,
    derivation: DerivationNode | None = None,
    premises: tuple[FactId, ...] = (),
) -> ProvenanceDag[ExprT]:
    graph = self.to_rustworkx()
    index_by_id = dict(self._index_by_id)
    index_by_id[node.id] = graph.add_node(node)
    if derivation is not None:
        return self._with_step(
            derivation,
            premises=premises,
            conclusion=node.id,
            graph=graph,
            index_by_id=index_by_id,
        )
    return self._replace_graph(graph, index_by_id)

with_derivation

with_derivation(derivation, *, premises, conclusion)

Add a forward step, or one that concludes nothing.

conclusion=None is a step with premises and no result: an inconsistent base's conflict, which cites the givens that cannot all hold and establishes nothing, because an edge into the check would draw it as decided in a world that does not exist. The step is what it always was on the wire; until 2026-09-19 this type could not hold it, so an INCONSISTENT_BASE response could not be rebuilt at all.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def with_derivation(
    self,
    derivation: DerivationNode,
    *,
    premises: tuple[FactId, ...],
    conclusion: FactId | None,
) -> ProvenanceDag[ExprT]:
    """Add a forward step, or one that concludes nothing.

    ``conclusion=None`` is a step with premises and no result: an
    inconsistent base's conflict, which cites the givens that cannot all
    hold and establishes nothing, because an edge into the check would
    draw it as decided in a world that does not exist. The step is what
    it always was on the wire; until 2026-09-19 this type could not hold
    it, so an `INCONSISTENT_BASE` response could not be rebuilt at all.
    """
    return self._with_step(
        derivation,
        premises=premises,
        conclusion=conclusion,
    )

with_explanation

with_explanation(explanation, *, premises, check)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def with_explanation(
    self,
    explanation: ExplanationNode,
    *,
    premises: tuple[FactId, ...],
    check: FactId,
) -> ProvenanceDag[ExprT]:
    return self._with_step(
        explanation,
        premises=premises,
        conclusion=check,
    )

explanation_nodes

explanation_nodes(target_id)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def explanation_nodes(self, target_id: FactId) -> Iterator[ProvenanceNode[ExprT]]:
    relevant_ids = self.explanation_node_ids(target_id)
    relevant_indices = [self._index_by_id[node_id] for node_id in relevant_ids]
    sub = self._graph.subgraph(relevant_indices)
    for idx in _rustworkx().topological_sort(sub):
        payload = sub.get_node_data(idx)
        if isinstance(payload, FactNode):
            yield self.fact(payload.id)
        elif isinstance(payload, DerivationNode):
            yield self.derivation(payload.id)
        else:
            yield self.explanation(payload.id)

slice_for

slice_for(target_id)

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def slice_for(self, target_id: FactId) -> ProvenanceDag[ExprT]:
    relevant_ids = self.explanation_node_ids(target_id)
    return self._sub_dag(relevant_ids)

proof_for

proof_for(target_id)

One route to target_id: the slice, with one step per fact.

Saturation reaches a fact by every route the rules allow, and the provenance records them all -- relay-chain's second departure is derived both from the givens directly and from the first departure once that was derived. Both are true, and a reader shown both is shown the same conclusion twice with no way to tell which reading is the one to follow.

So a proof keeps one: walking back from the target, each fact keeps the step with the fewest ancestors -- the shortest route to it -- and only that step's premises are then needed. Ties go to the step whose id sorts first, so the same graph always yields the same proof and a renderer's output does not move under it.

slice_for stays the faithful answer, and is what a question about provenance gets; this is what a question about the explanation gets.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def proof_for(self, target_id: FactId) -> ProvenanceDag[ExprT]:
    """One route to ``target_id``: the slice, with one step per fact.

    Saturation reaches a fact by every route the rules allow, and the
    provenance records them all -- `relay-chain`'s second departure is
    derived both from the givens directly and from the first departure
    once that was derived. Both are true, and a reader shown both is
    shown the same conclusion twice with no way to tell which reading is
    the one to follow.

    So a *proof* keeps one: walking back from the target, each fact keeps
    the step with the fewest ancestors -- the shortest route to it -- and
    only that step's premises are then needed. Ties go to the step whose
    id sorts first, so the same graph always yields the same proof and a
    renderer's output does not move under it.

    `slice_for` stays the faithful answer, and is what a question about
    provenance gets; this is what a question about the explanation gets.
    """
    ancestors = _rustworkx().ancestors
    within = self.explanation_node_ids(target_id)

    def reach(step: DerivationNode | ExplanationNode) -> int:
        indices = ancestors(self._graph, self._index_by_id[step.id])
        return len({self._graph.get_node_data(one).id for one in indices} & within)

    kept: set[GraphNodeId] = set()
    pending: list[FactId] = [target_id]
    while pending:
        fact = pending.pop()
        if fact in kept:
            continue
        kept.add(fact)
        steps = [one for one in self._step_predecessors(fact) if one.id in within]
        if not steps:
            continue
        chosen = min(steps, key=lambda step: (reach(step), str(step.id)))
        kept.add(chosen.id)
        pending.extend(self._fact_predecessors(chosen.id))
    return self._sub_dag(kept)

DerivationId dataclass

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class DerivationId:
    value: str

    def __str__(self) -> str:
        return self.value

value instance-attribute

value

DerivationInput dataclass

Bases: Generic[ExprT]

Backend-free view constructible only from a consistent unsaturated graph.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class DerivationInput(Generic[ExprT]):
    """Backend-free view constructible only from a consistent unsaturated graph."""

    established: tuple[FactNode[ExprT], ...]
    #: Slot name -> dimension record (see ``FactGraph.slot_dimensions``), so
    #: derivation rules render their conclusions against declared display
    #: formats rather than assuming any particular dimension.
    slot_dimensions: Mapping[str, Dimension[Any]] = field(default_factory=dict)

established instance-attribute

established

slot_dimensions class-attribute instance-attribute

slot_dimensions = field(default_factory=dict)

DerivationNode dataclass

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class DerivationNode:
    id: DerivationId
    rule: str

id instance-attribute

id

rule instance-attribute

rule

DerivationProposal dataclass

Bases: Generic[ExprT]

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class DerivationProposal(Generic[ExprT]):
    conclusion: Prop[ExprT]
    premises: tuple[FactId, ...]
    rule: str
    source: SourceSpan | None = None
    #: The conclusion as a wire operand, where the rule read its premises
    #: from theirs: what the derived fact is identified by.
    identity: Stated | None = None

conclusion instance-attribute

conclusion

premises instance-attribute

premises

rule instance-attribute

rule

source class-attribute instance-attribute

source = None

identity class-attribute instance-attribute

identity = None

ExplanationInput dataclass

Bases: Generic[ExprT]

Backend-free view constructible only from a consistent saturated graph.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class ExplanationInput(Generic[ExprT]):
    """Backend-free view constructible only from a consistent saturated graph."""

    established: tuple[FactNode[ExprT], ...]
    checks: tuple[FactNode[ExprT], ...]
    #: Dimension name -> its declaration: its invariant over every slot of it
    #: the graph maps, conjoined in slot order. Separate from ``established``
    #: because these are not facts anyone authored and have no `FactId`;
    #: present at all because a check can be entailed by one, and a backend
    #: that never saw them could not tell that from a check entailed by
    #: nothing. Keyed by dimension because that is how a proposal cites one.
    declarations: Mapping[str, ExprT] = field(default_factory=dict)

established instance-attribute

established

checks instance-attribute

checks

declarations class-attribute instance-attribute

declarations = field(default_factory=dict)

ExplanationNode dataclass

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class ExplanationNode:
    id: DerivationId
    rule: str

id instance-attribute

id

rule instance-attribute

rule

ExplanationProposal dataclass

One proposed explanation: which premises justify a check, and by what rule.

premises names facts already in the graph. declarations names dimensions whose declaration the check also needed -- one fact for the puzzle, its invariant over every slot of it, not one per slot, so the houses are said once to be numbered 1 to 3 -- a declaration has no FactId until something cites it, so the graph materialises one as a FactKind.DECLARED fact when it attaches the proposal.

Names rather than expressions, and that is the load-bearing choice. The term is z3's and cannot cross the FFI; the dimension's name can, so each engine looks the declaration up and realises it for itself. Handing an engine the other's term would make it a courier rather than an implementation, which is the same argument fill-dimensional-gaps 1f settled for the invariants in the analysis base.

Materialised on demand rather than up front, which is the whole of joint-premise-explanations.md step 5: a declaration appears in an explanation exactly when it altered the result, so a graph carries no node nobody needed and an explanation omits nothing that mattered.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class ExplanationProposal:
    """One proposed explanation: which premises justify a check, and by what rule.

    ``premises`` names facts already in the graph. ``declarations`` names
    *dimensions* whose declaration the check also needed -- one fact for the
    puzzle, its invariant over every slot of it, not one per slot, so the
    houses are said once to be numbered 1 to 3 -- a
    declaration has no `FactId` until something cites it, so the graph
    materialises one as a `FactKind.DECLARED` fact when it attaches the
    proposal.

    Names rather than expressions, and that is the load-bearing choice. The
    term is z3's and cannot cross the FFI; the dimension's name can, so each engine
    looks the declaration up and realises it for itself. Handing an engine the
    other's term would make it a courier rather than an implementation, which
    is the same argument `fill-dimensional-gaps` 1f settled for the invariants
    in the analysis base.

    Materialised on demand rather than up front, which is the whole of
    joint-premise-explanations.md step 5: a declaration appears in an
    explanation exactly when it altered the result, so a graph carries no node
    nobody needed and an explanation omits nothing that mattered.
    """

    check_id: FactId
    premises: tuple[FactId, ...]
    rule: str
    declarations: tuple[str, ...] = ()

check_id instance-attribute

check_id

premises instance-attribute

premises

rule instance-attribute

rule

declarations class-attribute instance-attribute

declarations = ()

FactId dataclass

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class FactId:
    value: str

    def __str__(self) -> str:
        return self.value

value instance-attribute

value

FactKind

Bases: str, Enum

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

class FactKind(str, Enum):
    GIVEN = "GIVEN"
    DERIVED = "DERIVED"
    CHECK = "CHECK"
    #: A dimension's declared invariant, materialised so an explanation can
    #: cite it. Its own kind rather than a `GIVEN`, because a given is
    #: something a person asserted and this is something the *type* guarantees;
    #: a reader owes the distinction and so does anything counting authored
    #: premises. Never `established`: it is citable, not a fact the graph
    #: reasons forward from -- `base_exprs` already conjoins the same terms,
    #: and a second copy would be a second answer.
    DECLARED = "DECLARED"

GIVEN class-attribute instance-attribute

GIVEN = 'GIVEN'

DERIVED class-attribute instance-attribute

DERIVED = 'DERIVED'

CHECK class-attribute instance-attribute

CHECK = 'CHECK'

DECLARED class-attribute instance-attribute

DECLARED = 'DECLARED'

FactNode dataclass

Bases: Generic[ExprT]

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class FactNode(Generic[ExprT]):
    id: FactId
    kind: FactKind
    expr: ExprT
    text: str
    subject: str | None = None
    check_label: str | None = None
    source: SourceSpan | None = None
    #: The expression as it was stated, where it differs from ``expr``: a
    #: given authored as "17:30 minus 8 hours" is stored, keyed and derived
    #: from as ``== 570``, and this keeps the sum. Presentation only -- a
    #: realiser may say it; identity, keys, rules and verdicts read ``expr``.
    stated: ExprT | None = None
    #: What the fact is, as no engine spells it (:data:`Identity`).
    identity: Identity | None = None
    #: The author's own words for it, where they gave some
    #: (``.annotate(...)``): ``text`` is then this, and the presentation
    #: sidecar says so (``TextOrigin.AUTHORED``). ``None`` where ``text`` is
    #: a rendering.
    caption: str | None = None

id instance-attribute

id

kind instance-attribute

kind

expr instance-attribute

expr

text instance-attribute

text

subject class-attribute instance-attribute

subject = None

check_label class-attribute instance-attribute

check_label = None

source class-attribute instance-attribute

source = None

stated class-attribute instance-attribute

stated = None

identity class-attribute instance-attribute

identity = None

caption class-attribute instance-attribute

caption = None

FactToken dataclass

Bases: Generic[ExprT]

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True)
class FactToken(Generic[ExprT]):
    id: FactId

id instance-attribute

id

SourceSpan dataclass

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

@dataclass(frozen=True, order=True)
class SourceSpan:
    uri: str
    start_line: int
    start_col: int
    end_line: int
    end_col: int

uri instance-attribute

uri

start_line instance-attribute

start_line

start_col instance-attribute

start_col

end_line instance-attribute

end_line

end_col instance-attribute

end_col

CheckResult dataclass

A classification verdict plus the witnessing models and unsat cores.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class CheckResult:
    """A classification verdict plus the witnessing models and unsat cores."""

    status: Status
    true_model: ModelRef | None
    false_model: ModelRef | None
    true_core: tuple[BoolRef, ...]
    false_core: tuple[BoolRef, ...]

status instance-attribute

status

true_model instance-attribute

true_model

false_model instance-attribute

false_model

true_core instance-attribute

true_core

false_core instance-attribute

false_core

EntailsNotary dataclass

The z3 judgement: premises support a conclusion iff they entail it.

The one notary that existed implicitly before the seam — every add_derived was an inlined entails call. Spelled as an object so a conclusion type with a different standard of proof (the dialects' complete-unless-rogue, whose judge is enumeration, not entailment) can stand in the same slot without the graph changing.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class EntailsNotary:
    """The z3 judgement: premises support a conclusion iff they entail it.

    The one notary that existed implicitly before the seam — every
    ``add_derived`` was an inlined ``entails`` call. Spelled as an object so
    a conclusion type with a different standard of proof (the dialects'
    ``complete-unless-rogue``, whose judge is enumeration, not entailment)
    can stand in the same slot without the graph changing.
    """

    def notarise(
        self,
        premises: Sequence[BoolRef],
        conclusion: BoolRef,
        semantics: SemanticBackend,
    ) -> Entailment:
        return entails(premises, conclusion, backend=semantics)

notarise

notarise(premises, conclusion, semantics)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def notarise(
    self,
    premises: Sequence[BoolRef],
    conclusion: BoolRef,
    semantics: SemanticBackend,
) -> Entailment:
    return entails(premises, conclusion, backend=semantics)

FactGraph dataclass

Bases: Generic[StateT]

Facts, derivation steps, and checks in one typed provenance DAG.

Derivations are represented as:

premise fact -> derivation step -> conclusion fact

This preserves multi-premise rules and allows a single semantic fact to have several independent derivations without overloading edge labels or a single rule attribute on the conclusion fact.

Checks remain candidate propositions, not established facts. They cannot be premises; they are sinks. A known fact can point directly into a check when explain_check establishes an explicit explanation step.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class FactGraph(Generic[StateT]):
    """Facts, derivation steps, and checks in one typed provenance DAG.

    Derivations are represented as:

        premise fact -> derivation step -> conclusion fact

    This preserves multi-premise rules and allows a single semantic fact to have
    several independent derivations without overloading edge labels or a single
    ``rule`` attribute on the conclusion fact.

    Checks remain candidate propositions, not established facts. They cannot be
    premises; they are sinks. A known fact can point directly into a check when
    ``explain_check`` establishes an explicit explanation step.
    """

    dag: ProvenanceDag[BoolRef] = field(default_factory=ProvenanceDag[BoolRef])
    by_expr: Mapping[str, FactId] = field(default_factory=dict)
    #: Slot name -> dimension record, harvested from ingested propositions'
    #: pre-lowering expression trees (the one place dimension identity still
    #: exists before ``as_z3_bool`` erases it to named z3 terms). Rendering
    #: reads a slot's *declared* DisplayFormat/unit from here — the reasoning
    #: layer names no dimension of its own.
    slot_dimensions: Mapping[str, Dimension[Any]] = field(default_factory=dict)
    next_index: int = 1
    next_derivation_index: int = 1
    reasoning_backend: ReasoningBackend = field(
        default_factory=default_reasoning_backend,
        compare=False,
        repr=False,
    )

    @classmethod
    def empty(cls) -> FactGraph[Evidence[Unchecked, Unsaturated]]:
        return FactGraph()

    def with_reasoning_backend(
        self,
        backend: ReasoningBackend,
    ) -> FactGraph[StateT]:
        """Return an equal immutable graph using ``backend`` operationally."""
        return replace(self, reasoning_backend=backend)

    @property
    def _algebra(self) -> ExpressionAlgebra[Boolish_Bound, BoolRef]:
        """The backend's expression operations — the graph's only route to them.

        Every identity, ingress, normalisation and rendering decision goes
        through here, never through the module-level z3 helpers directly:
        that is the keying seam that lets a different expression type slot in
        behind the same graph.
        """
        return self.reasoning_backend.algebra

    def _fresh_id(self) -> FactId:
        return FactId(f"f{self.next_index}")

    def _fresh_derivation_id(self) -> DerivationId:
        return DerivationId(f"d{self.next_derivation_index}")

    def fact(self, fact_id: FactId) -> FactNode[BoolRef]:
        return self.dag.fact(fact_id)

    def derivation_step(self, derivation_id: DerivationId) -> DerivationNode:
        return self.dag.derivation(derivation_id)

    @property
    def nodes(self) -> Mapping[FactId, FactNode[BoolRef]]:
        return self.dag.facts()

    @property
    def derivation_nodes(self) -> Mapping[DerivationId, DerivationNode]:
        return self.dag.derivation_nodes()

    @property
    def derivations(self) -> Mapping[FactId, tuple[Derivation, ...]]:
        return self.dag.derivations()

    def _index_key(self, expr: BoolRef, identity: Identity | None) -> str:
        """What the graph coalesces a fact on: what it is -- its operand's
        canonical key, or its slot (`identity_key`) -- the key both engines
        share (reasoning-wire-ir.md phase 3). Only a fact asserted as a raw
        solver term, with no identity, falls back to z3's spelling of it."""
        if identity is None:
            return f"z3\x1f{self._algebra.key(expr)}"
        return identity_key(identity, "")

    def _insert_fact(
        self,
        node: FactNode[BoolRef],
        *,
        index_expression: bool,
    ) -> tuple[FactId, FactGraph[StateT]]:
        by_expr = (
            {**self.by_expr, self._index_key(node.expr, node.identity): node.id}
            if index_expression
            else self.by_expr
        )
        return node.id, replace(
            self,
            dag=self.dag.with_fact(node),
            by_expr=by_expr,
            next_index=self.next_index + 1,
        )

    def _noting_slots(self, expr: object) -> FactGraph[StateT]:
        """Record any dimension-carrying slot references found in ``expr``.

        Called with the authored (pre-lowering) proposition, whose reference
        leaves still carry their ``Dimension`` records and paths; the same
        slot always resolves the same dimension, so merging is idempotent.
        """
        found = slot_dimensions_in(expr)
        if not found:
            return self
        return replace(self, slot_dimensions={**self.slot_dimensions, **found})

    def _with_given(
        self,
        *,
        expr: BoolRef,
        text: str | None,
        caption: str | None = None,
        subject_name: str | None = None,
        source: SourceSpan | None,
        identity: Identity | None = None,
    ) -> tuple[FactId, FactGraph[StateT], bool]:
        stated = expr
        expr = self._algebra.normalise(expr)
        key = self._index_key(expr, identity)
        if key in self.by_expr:
            return self.by_expr[key], self, False
        fact_id, graph = self._insert_fact(
            FactNode(
                id=self._fresh_id(),
                kind=FactKind.GIVEN,
                expr=expr,
                text=text or self._algebra.render(expr, self.slot_dimensions),
                caption=caption,
                subject=subject_name,
                source=source,
                # The sum an author wrote, kept beside the term it folds to.
                # Structural, not by key: the key is of the folded term.
                stated=None if stated.eq(expr) else stated,
                identity=identity,
            ),
            index_expression=True,
        )
        return fact_id, graph, True

    def _with_declaration(self, dimension: str) -> tuple[FactId, FactGraph[StateT]]:
        """Materialise one dimension's declaration as a citable fact, once.

        Keyed through ``by_expr`` like any other fact, so the same
        declaration cited by two explanations is one node rather than two --
        which is the "state a dimensional fact once" half of step 5, and free,
        because the index already answers it. One node for the puzzle, not
        one per slot: "the houses are numbered 1 to 3".

        No subject and no source: nobody authored this. The text is the
        algebra's rendering of the term, which is what a reader is owed when
        the thing being cited is a type's guarantee rather than a sentence
        somebody wrote.

        The term is realised here rather than carried in the proposal, because
        a proposal cites a *dimension*: this graph knows its slots and builds
        the same declaration the base already conjoins.
        """
        declared = self._algebra.declarations(self.slot_dimensions)
        if dimension not in declared:
            raise ValueError(
                f"No declaration for dimension {dimension!r}: an explanation can "
                "only cite a declaration the registry actually carries"
            )
        expr = self._algebra.normalise(declared[dimension])
        identity = Invariant(dimension=dimension)
        stated = self.by_expr.get(self._index_key(expr, identity))
        # The declaration already stated -- as the base's -- is this fact,
        # where it is the same term. A slot read as two sorts has two terms
        # for one declaration, and the one cited here is its own fact,
        # unindexed: the index keeps the first.
        if stated is not None and self.dag.fact(stated).expr.eq(expr):
            return stated, self
        return self._insert_fact(
            FactNode(
                id=self._fresh_id(),
                kind=FactKind.DECLARED,
                expr=expr,
                text=self._algebra.render(expr, self.slot_dimensions),
                identity=identity,
            ),
            index_expression=stated is None,
        )

    def _with_check(
        self,
        *,
        expr: BoolRef,
        text: str | None,
        caption: str | None = None,
        subject_name: str | None = None,
        check_label: str,
        source: SourceSpan | None,
        identity: Identity | None = None,
    ) -> tuple[FactId, FactGraph[StateT]]:
        expr = self._algebra.normalise(expr)
        return self._insert_fact(
            FactNode(
                id=self._fresh_id(),
                kind=FactKind.CHECK,
                expr=expr,
                text=text or self._algebra.render(expr, self.slot_dimensions),
                caption=caption,
                subject=subject_name,
                check_label=check_label,
                source=source,
                identity=identity,
            ),
            index_expression=False,
        )

    # The token returned by each add_* method carries the asserted Prop's
    # expression type as phantom evidence of what the caller put in. Note
    # that dedupe can hand back a token for a structurally equal fact that
    # was asserted under a different expression type, so this evidence is
    # about the claim, not the stored node — a typed recall() accessor must
    # wait for Phase 4's typed check surface.

    def add_given[E: Boolish_Bound](
        self: FactGraph[Evidence[Unchecked, Unsaturated]],
        prop_: Prop[E],
        *,
        subject_name: str | None = None,
        source: SourceSpan | None = None,
        identity: Identity | None = None,
    ) -> tuple[FactToken[E], FactGraph[Evidence[Unchecked, Unsaturated]]]:
        fact_id, graph, _added = self._noting_slots(prop_.expr)._with_given(
            expr=self._algebra.ingress(prop_.expr),
            text=prop_.display_text,
            caption=prop_.text,
            subject_name=subject_name,
            source=source,
            identity=identity or _authored(prop_.expr),
        )
        return FactToken[E](fact_id), graph

    def add_check[E: Boolish_Bound](
        self,
        prop_: Prop[E],
        *,
        subject_name: str | None = None,
        check_label: str,
        source: SourceSpan | None = None,
        identity: Identity | None = None,
    ) -> tuple[FactToken[E], FactGraph[StateT]]:
        fact_id, graph = self._noting_slots(prop_.expr)._with_check(
            expr=self._algebra.ingress(prop_.expr),
            text=prop_.display_text,
            caption=prop_.text,
            subject_name=subject_name,
            check_label=check_label,
            source=source,
            identity=identity or _authored(prop_.expr),
        )
        return FactToken[E](fact_id), graph

    def add_derived[E: Boolish_Bound](
        self: FactGraph[Evidence[Consistent, Unsaturated]],
        prop_: Prop[E],
        *,
        premises: Iterable[FactToken[Any]],
        rule: str,
        source: SourceSpan | None = None,
    ) -> tuple[
        FactToken[E],
        bool,
        FactGraph[Evidence[Consistent, Unsaturated]],
    ]:
        proposal = DerivationProposal(
            conclusion=Prop(expr=self._algebra.ingress(prop_.expr), text=prop_.text),
            premises=tuple(token.id for token in premises),
            rule=rule,
            source=source,
        )
        token, added, graph = self.apply_derivation(proposal)
        return FactToken[E](token.id), added, graph

    def apply_derivation(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
        proposal: DerivationProposal[BoolRef],
    ) -> tuple[
        FactToken[BoolRef],
        bool,
        FactGraph[Evidence[Consistent, Unsaturated]],
    ]:
        if (
            self.reasoning_backend.notary.notarise(
                [node.expr for node in self._premise_nodes(proposal.premises)],
                self._algebra.ingress(proposal.conclusion.expr),
                self.reasoning_backend.semantics,
            )
            is not Entailment.PROVED
        ):
            raise ValueError(
                "Invalid derivation: premises do not entail conclusion.\n"
                f"Rule: {proposal.rule}\n"
                f"Conclusion: {self._algebra.ingress(proposal.conclusion.expr)}"
            )
        return self._with_derivation(proposal)

    def _premise_nodes(
        self, premise_ids: Iterable[FactId]
    ) -> tuple[FactNode[BoolRef], ...]:
        nodes: list[FactNode[BoolRef]] = []
        for premise_id in premise_ids:
            if premise_id not in self.dag:
                raise KeyError(
                    f"Premise token does not belong to this graph: {premise_id}"
                )
            node = self.fact(premise_id)
            if node.kind is FactKind.CHECK:
                raise ValueError(f"Checks cannot be premises: {node.id}")
            nodes.append(node)
        return tuple(nodes)

    def apply_derivations(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
        proposals: Iterable[DerivationProposal[BoolRef]],
    ) -> tuple[bool, FactGraph[Evidence[Consistent, Unsaturated]]]:
        changed = False
        working = self
        for proposal in proposals:
            _token, added, working = working.apply_derivation(proposal)
            changed |= added
        return changed, working

    def _with_derivation(
        self,
        proposal: DerivationProposal[BoolRef],
    ) -> tuple[FactToken[BoolRef], bool, FactGraph[StateT]]:
        premise_ids = proposal.premises
        expr = self._algebra.normalise(self._algebra.ingress(proposal.conclusion.expr))
        key = self._index_key(expr, proposal.identity)
        existing_fact_id = self.by_expr.get(key)
        if existing_fact_id is not None:
            # A conclusion that is — or transitively feeds — one of its own
            # premises is declined outright: the "derivation" would be
            # circular, and its edge the one step shape that can close a
            # provenance cycle (``validate()`` rejects the result, but only
            # at boundaries the saturation loop never crosses).
            if self.dag.reaches_any(
                existing_fact_id, premise_ids
            ) or self.dag.has_derivation(
                conclusion_id=existing_fact_id,
                premise_ids=premise_ids,
                rule=proposal.rule,
            ):
                return FactToken[BoolRef](existing_fact_id), False, self
            derivation = DerivationNode(
                id=self._fresh_derivation_id(), rule=proposal.rule
            )
            return (
                FactToken[BoolRef](existing_fact_id),
                False,
                replace(
                    self,
                    dag=self.dag.with_derivation(
                        derivation,
                        premises=premise_ids,
                        conclusion=existing_fact_id,
                    ),
                    next_derivation_index=self.next_derivation_index + 1,
                ),
            )

        fact_id = self._fresh_id()
        derivation = DerivationNode(id=self._fresh_derivation_id(), rule=proposal.rule)
        node = FactNode(
            id=fact_id,
            kind=FactKind.DERIVED,
            expr=expr,
            text=proposal.conclusion.display_text
            or self._algebra.render(expr, self.slot_dimensions),
            caption=proposal.conclusion.text,
            source=proposal.source,
            identity=proposal.identity,
        )
        return (
            FactToken[BoolRef](fact_id),
            True,
            replace(
                self,
                dag=self.dag.with_fact(
                    node,
                    derivation=derivation,
                    premises=premise_ids,
                ),
                by_expr={**self.by_expr, key: fact_id},
                next_index=self.next_index + 1,
                next_derivation_index=self.next_derivation_index + 1,
            ),
        )

    #: Node kinds that are not established facts: a check is what the graph is
    #: asked about, and a declaration is a citable statement of what a type
    #: guarantees rather than something the graph reasons forward from.
    _NOT_ESTABLISHED = frozenset({FactKind.CHECK, FactKind.DECLARED})

    def established_facts(self) -> tuple[FactNode[BoolRef], ...]:
        return tuple(
            node
            for node in self.nodes.values()
            if node.kind not in self._NOT_ESTABLISHED
        )

    def base_exprs(self) -> list[BoolRef]:
        """The established facts, plus every mapped slot's declared invariant.

        The invariants are not facts anyone authored, so they stay out of
        ``established_facts`` (and therefore out of the explanation DAG); they
        are the same standing assumptions the wire path conjoins into every
        analysis base, so a witness can never assign a slot a value its
        dimension forbids, and a check the declaration alone entails comes back
        VERIFIED rather than UNKNOWN.
        """
        return [
            *(node.expr for node in self.established_facts()),
            *self._algebra.invariants(self.slot_dimensions),
        ]

    def derivation_input(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
    ) -> DerivationInput[BoolRef]:
        return DerivationInput(
            established=self.established_facts(),
            slot_dimensions=self.slot_dimensions,
        )

    def explanation_input(
        self: FactGraph[Evidence[Consistent, Saturated]],
        checks: Iterable[FactToken[Any]],
    ) -> ExplanationInput[BoolRef]:
        check_nodes = tuple(self.fact(token.id) for token in checks)
        for node in check_nodes:
            if node.kind is not FactKind.CHECK:
                raise ValueError(f"Not a check token: {node.id}")
        return ExplanationInput(
            established=self.established_facts(),
            checks=check_nodes,
            declarations=self._algebra.declarations(self.slot_dimensions),
        )

    def check_consistent[SaturationT](
        self: FactGraph[Evidence[Unchecked, SaturationT]],
    ) -> FactGraph[Evidence[Consistent, SaturationT]]:
        result = self.reasoning_backend.semantics.solve(self.base_exprs())
        if result.status is SolveStatus.UNSAT:
            lines = "\n".join(f"  {expr}" for expr in result.core)
            raise ValueError(f"Inconsistent givens:\n{lines}")
        if result.status in NO_VERDICT:
            raise ValueError("Solver could not determine consistency.")
        return cast(FactGraph[Evidence[Consistent, SaturationT]], self)

    def saturate(
        self: FactGraph[Evidence[Consistent, Unsaturated]],
    ) -> FactGraph[Evidence[Consistent, Saturated]]:
        working = self
        for _round in range(self.reasoning_backend.max_rounds):
            changed, working = working.apply_derivations(
                self.reasoning_backend.derivation.derive(working.derivation_input())
            )
            if not changed:
                return cast(FactGraph[Evidence[Consistent, Saturated]], working)
        raise RuntimeError("Derivation did not reach a fixed point.")

    def classify[SaturationT](
        self: FactGraph[Evidence[Consistent, SaturationT]],
        check: FactToken[Any],
    ) -> CheckVerdict:
        """Classify one check fact against this graph's base.

        The base is :meth:`base_exprs` — every established fact *and* every
        mapped slot's declared invariant — not the facts alone, so a check the
        declaration by itself entails comes back `VERIFIED` rather than
        `UNKNOWN`.

        The explanation stage solves over the same set, and has since a
        declaration became citable (joint-premise-explanations.md step 5).
        Before that it deliberately solved over the facts alone, because an
        invariant had no node a proposal could name; now one is materialised
        when the core says it mattered, so a verdict and its explanation rest
        on the same premises rather than on two sets that had to be reconciled.
        Whether the two should therefore share *one solve* was measured and
        declined — see that document's step 4.

        Callable in any saturation state, because classification reads the base
        rather than the derivations; consistency is required because an
        unsatisfiable base entails everything and the answer would be
        meaningless.
        """
        node = self.fact(check.id)
        if node.kind is not FactKind.CHECK:
            raise ValueError(f"Not a check token: {node.id}")
        base = self.base_exprs()
        result = classify(base, node.expr, backend=self.reasoning_backend.semantics)
        return verdict_of(result, [node.expr, *base], self.nodes.values())

    def verify_derivations(self) -> list[str]:
        """Re-check every stored derivation against the solver.

        Derivations are already entails-verified at insertion time in
        ``add_derived``; this is an opt-in audit for callers who want to
        re-establish that guarantee (e.g. over a deserialized graph), not
        something the solving pipeline runs per round.
        """
        errors: list[str] = []

        for conclusion_id, derivations in self.derivations.items():
            for derivation in derivations:
                premises = [
                    self.fact(premise_id).expr for premise_id in derivation.premise_ids
                ]
                conclusion = self.fact(conclusion_id).expr

                if (
                    self.reasoning_backend.notary.notarise(
                        premises,
                        conclusion,
                        self.reasoning_backend.semantics,
                    )
                    is not Entailment.PROVED
                ):
                    errors.append(
                        f"Invalid derivation {conclusion_id}: {derivation.rule}"
                    )

        return errors

    def explanation_for(self, target: FactToken[Any]) -> list[str]:
        return explanation_lines(self.dag, target.id)

    def explanation_subgraph_for(
        self,
        target: FactToken[Any],
    ) -> FactGraph[StateT]:
        """Return the minimal ancestor subgraph explaining ``target``.

        This is the graph-shaped counterpart to ``explanation_for``. It keeps
        the same immutable graph wrapper, but restricts the DAG to the target
        fact plus all graph nodes that feed into it, including derivation steps.
        """
        target_id = target.id

        if target_id not in self.dag:
            raise KeyError(f"Unknown fact id: {target_id}")

        sliced_dag = self.dag.slice_for(target_id)

        by_expr = {
            key: fact_id
            for key, fact_id in self.by_expr.items()
            if fact_id in sliced_dag
        }

        return replace(
            self,
            dag=sliced_dag,
            by_expr=by_expr,
        )

    def explain_check(
        self: FactGraph[Evidence[Consistent, Saturated]],
        check: FactToken[Any],
    ) -> tuple[bool, FactGraph[Evidence[Consistent, Saturated]]]:
        check_id = check.id
        if check_id not in self.dag:
            raise KeyError(f"Check token does not belong to this graph: {check_id}")
        check_node = self.fact(check_id)
        if check_node.kind is not FactKind.CHECK:
            raise ValueError(f"Not a check token: {check_id}")
        if self.dag.in_degree(check_id) > 0:
            return True, self

        return next(
            iter(
                (True, self.apply_explanation(x))
                for x in self.reasoning_backend.explanation.explain(
                    self.explanation_input((check,)),
                    self.reasoning_backend.semantics,
                )
            ),
            (False, self),
        )

    def apply_explanation(
        self,
        proposal: ExplanationProposal,
    ) -> FactGraph[StateT]:
        """Attach one proposed explanation to a check, after verifying it.

        The verification is the whole point of the method, and it is *not*
        equivalence. What is required is one-way entailment — the proposal's
        premises must prove the check, checked by the reasoning backend's
        notary — so a set of facts that jointly imply a check is a valid
        explanation of it even when no member restates it and the implication
        does not run the other way. `amount = 10000` explains
        `amount >= 10000`; the reverse does not hold and does not need to.

        Premises are plural for the same reason. Nothing here privileges a
        single fact, and a proposer that only ever offers one is leaving valid
        explanations on the table rather than obeying a rule.

        A proposal whose premises do not entail the check raises rather than
        being dropped. An explanation stage is free to find nothing; it is not
        free to attach something wrong, and silently discarding a bad proposal
        would turn a proposer's bug into a quietly emptier DAG.

        Returns:
            A new graph with one `ExplanationNode` joining the premises to the
            check. The graph is immutable, so the receiver is unchanged.

        Raises:
            KeyError: if the check id is not in this graph.
            ValueError: if the id names something other than a check, or if
                the premises do not entail it.
        """
        if proposal.check_id not in self.dag:
            raise KeyError(
                f"Check token does not belong to this graph: {proposal.check_id}"
            )
        check_node = self.fact(proposal.check_id)
        if check_node.kind is not FactKind.CHECK:
            raise ValueError(f"Not a check token: {proposal.check_id}")
        # Declarations arrive as expressions rather than ids, because a
        # dimension's invariant has no node until something cites it. They are
        # materialised here, before the notary runs, so the entailment is
        # checked against exactly the premises the DAG will record -- attaching
        # a proposal whose declared half was never notarised would be the one
        # way this method could pass something wrong.
        graph: FactGraph[StateT] = self
        declared_ids: list[FactId] = []
        for dimension in proposal.declarations:
            declared_id, graph = graph._with_declaration(dimension)
            declared_ids.append(declared_id)
        premise_ids = (*proposal.premises, *declared_ids)
        premises = graph._premise_nodes(premise_ids)
        if (
            graph.reasoning_backend.notary.notarise(
                [premise.expr for premise in premises],
                check_node.expr,
                graph.reasoning_backend.semantics,
            )
            is not Entailment.PROVED
        ):
            raise ValueError("Explanation premises do not entail the check.")
        step = ExplanationNode(
            id=graph._fresh_derivation_id(),
            rule=proposal.rule,
        )
        return replace(
            graph,
            dag=graph.dag.with_explanation(
                step,
                premises=premise_ids,
                check=proposal.check_id,
            ),
            next_derivation_index=graph.next_derivation_index + 1,
        )

dag class-attribute instance-attribute

dag = field(default_factory=ProvenanceDag[BoolRef])

by_expr class-attribute instance-attribute

by_expr = field(default_factory=dict)

slot_dimensions class-attribute instance-attribute

slot_dimensions = field(default_factory=dict)

next_index class-attribute instance-attribute

next_index = 1

next_derivation_index class-attribute instance-attribute

next_derivation_index = 1

reasoning_backend class-attribute instance-attribute

reasoning_backend = field(
    default_factory=default_reasoning_backend,
    compare=False,
    repr=False,
)

nodes property

nodes

derivation_nodes property

derivation_nodes

derivations property

derivations

empty classmethod

empty()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@classmethod
def empty(cls) -> FactGraph[Evidence[Unchecked, Unsaturated]]:
    return FactGraph()

with_reasoning_backend

with_reasoning_backend(backend)

Return an equal immutable graph using backend operationally.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def with_reasoning_backend(
    self,
    backend: ReasoningBackend,
) -> FactGraph[StateT]:
    """Return an equal immutable graph using ``backend`` operationally."""
    return replace(self, reasoning_backend=backend)

fact

fact(fact_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def fact(self, fact_id: FactId) -> FactNode[BoolRef]:
    return self.dag.fact(fact_id)

derivation_step

derivation_step(derivation_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derivation_step(self, derivation_id: DerivationId) -> DerivationNode:
    return self.dag.derivation(derivation_id)

add_given

add_given(
    prop_, *, subject_name=None, source=None, identity=None
)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def add_given[E: Boolish_Bound](
    self: FactGraph[Evidence[Unchecked, Unsaturated]],
    prop_: Prop[E],
    *,
    subject_name: str | None = None,
    source: SourceSpan | None = None,
    identity: Identity | None = None,
) -> tuple[FactToken[E], FactGraph[Evidence[Unchecked, Unsaturated]]]:
    fact_id, graph, _added = self._noting_slots(prop_.expr)._with_given(
        expr=self._algebra.ingress(prop_.expr),
        text=prop_.display_text,
        caption=prop_.text,
        subject_name=subject_name,
        source=source,
        identity=identity or _authored(prop_.expr),
    )
    return FactToken[E](fact_id), graph

add_check

add_check(
    prop_,
    *,
    subject_name=None,
    check_label,
    source=None,
    identity=None
)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def add_check[E: Boolish_Bound](
    self,
    prop_: Prop[E],
    *,
    subject_name: str | None = None,
    check_label: str,
    source: SourceSpan | None = None,
    identity: Identity | None = None,
) -> tuple[FactToken[E], FactGraph[StateT]]:
    fact_id, graph = self._noting_slots(prop_.expr)._with_check(
        expr=self._algebra.ingress(prop_.expr),
        text=prop_.display_text,
        caption=prop_.text,
        subject_name=subject_name,
        check_label=check_label,
        source=source,
        identity=identity or _authored(prop_.expr),
    )
    return FactToken[E](fact_id), graph

add_derived

add_derived(prop_, *, premises, rule, source=None)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def add_derived[E: Boolish_Bound](
    self: FactGraph[Evidence[Consistent, Unsaturated]],
    prop_: Prop[E],
    *,
    premises: Iterable[FactToken[Any]],
    rule: str,
    source: SourceSpan | None = None,
) -> tuple[
    FactToken[E],
    bool,
    FactGraph[Evidence[Consistent, Unsaturated]],
]:
    proposal = DerivationProposal(
        conclusion=Prop(expr=self._algebra.ingress(prop_.expr), text=prop_.text),
        premises=tuple(token.id for token in premises),
        rule=rule,
        source=source,
    )
    token, added, graph = self.apply_derivation(proposal)
    return FactToken[E](token.id), added, graph

apply_derivation

apply_derivation(proposal)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def apply_derivation(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
    proposal: DerivationProposal[BoolRef],
) -> tuple[
    FactToken[BoolRef],
    bool,
    FactGraph[Evidence[Consistent, Unsaturated]],
]:
    if (
        self.reasoning_backend.notary.notarise(
            [node.expr for node in self._premise_nodes(proposal.premises)],
            self._algebra.ingress(proposal.conclusion.expr),
            self.reasoning_backend.semantics,
        )
        is not Entailment.PROVED
    ):
        raise ValueError(
            "Invalid derivation: premises do not entail conclusion.\n"
            f"Rule: {proposal.rule}\n"
            f"Conclusion: {self._algebra.ingress(proposal.conclusion.expr)}"
        )
    return self._with_derivation(proposal)

apply_derivations

apply_derivations(proposals)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def apply_derivations(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
    proposals: Iterable[DerivationProposal[BoolRef]],
) -> tuple[bool, FactGraph[Evidence[Consistent, Unsaturated]]]:
    changed = False
    working = self
    for proposal in proposals:
        _token, added, working = working.apply_derivation(proposal)
        changed |= added
    return changed, working

established_facts

established_facts()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def established_facts(self) -> tuple[FactNode[BoolRef], ...]:
    return tuple(
        node
        for node in self.nodes.values()
        if node.kind not in self._NOT_ESTABLISHED
    )

base_exprs

base_exprs()

The established facts, plus every mapped slot's declared invariant.

The invariants are not facts anyone authored, so they stay out of established_facts (and therefore out of the explanation DAG); they are the same standing assumptions the wire path conjoins into every analysis base, so a witness can never assign a slot a value its dimension forbids, and a check the declaration alone entails comes back VERIFIED rather than UNKNOWN.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def base_exprs(self) -> list[BoolRef]:
    """The established facts, plus every mapped slot's declared invariant.

    The invariants are not facts anyone authored, so they stay out of
    ``established_facts`` (and therefore out of the explanation DAG); they
    are the same standing assumptions the wire path conjoins into every
    analysis base, so a witness can never assign a slot a value its
    dimension forbids, and a check the declaration alone entails comes back
    VERIFIED rather than UNKNOWN.
    """
    return [
        *(node.expr for node in self.established_facts()),
        *self._algebra.invariants(self.slot_dimensions),
    ]

derivation_input

derivation_input()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derivation_input(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
) -> DerivationInput[BoolRef]:
    return DerivationInput(
        established=self.established_facts(),
        slot_dimensions=self.slot_dimensions,
    )

explanation_input

explanation_input(checks)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_input(
    self: FactGraph[Evidence[Consistent, Saturated]],
    checks: Iterable[FactToken[Any]],
) -> ExplanationInput[BoolRef]:
    check_nodes = tuple(self.fact(token.id) for token in checks)
    for node in check_nodes:
        if node.kind is not FactKind.CHECK:
            raise ValueError(f"Not a check token: {node.id}")
    return ExplanationInput(
        established=self.established_facts(),
        checks=check_nodes,
        declarations=self._algebra.declarations(self.slot_dimensions),
    )

check_consistent

check_consistent()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def check_consistent[SaturationT](
    self: FactGraph[Evidence[Unchecked, SaturationT]],
) -> FactGraph[Evidence[Consistent, SaturationT]]:
    result = self.reasoning_backend.semantics.solve(self.base_exprs())
    if result.status is SolveStatus.UNSAT:
        lines = "\n".join(f"  {expr}" for expr in result.core)
        raise ValueError(f"Inconsistent givens:\n{lines}")
    if result.status in NO_VERDICT:
        raise ValueError("Solver could not determine consistency.")
    return cast(FactGraph[Evidence[Consistent, SaturationT]], self)

saturate

saturate()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def saturate(
    self: FactGraph[Evidence[Consistent, Unsaturated]],
) -> FactGraph[Evidence[Consistent, Saturated]]:
    working = self
    for _round in range(self.reasoning_backend.max_rounds):
        changed, working = working.apply_derivations(
            self.reasoning_backend.derivation.derive(working.derivation_input())
        )
        if not changed:
            return cast(FactGraph[Evidence[Consistent, Saturated]], working)
    raise RuntimeError("Derivation did not reach a fixed point.")

classify

classify(check)

Classify one check fact against this graph's base.

The base is :meth:base_exprs — every established fact and every mapped slot's declared invariant — not the facts alone, so a check the declaration by itself entails comes back VERIFIED rather than UNKNOWN.

The explanation stage solves over the same set, and has since a declaration became citable (joint-premise-explanations.md step 5). Before that it deliberately solved over the facts alone, because an invariant had no node a proposal could name; now one is materialised when the core says it mattered, so a verdict and its explanation rest on the same premises rather than on two sets that had to be reconciled. Whether the two should therefore share one solve was measured and declined — see that document's step 4.

Callable in any saturation state, because classification reads the base rather than the derivations; consistency is required because an unsatisfiable base entails everything and the answer would be meaningless.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def classify[SaturationT](
    self: FactGraph[Evidence[Consistent, SaturationT]],
    check: FactToken[Any],
) -> CheckVerdict:
    """Classify one check fact against this graph's base.

    The base is :meth:`base_exprs` — every established fact *and* every
    mapped slot's declared invariant — not the facts alone, so a check the
    declaration by itself entails comes back `VERIFIED` rather than
    `UNKNOWN`.

    The explanation stage solves over the same set, and has since a
    declaration became citable (joint-premise-explanations.md step 5).
    Before that it deliberately solved over the facts alone, because an
    invariant had no node a proposal could name; now one is materialised
    when the core says it mattered, so a verdict and its explanation rest
    on the same premises rather than on two sets that had to be reconciled.
    Whether the two should therefore share *one solve* was measured and
    declined — see that document's step 4.

    Callable in any saturation state, because classification reads the base
    rather than the derivations; consistency is required because an
    unsatisfiable base entails everything and the answer would be
    meaningless.
    """
    node = self.fact(check.id)
    if node.kind is not FactKind.CHECK:
        raise ValueError(f"Not a check token: {node.id}")
    base = self.base_exprs()
    result = classify(base, node.expr, backend=self.reasoning_backend.semantics)
    return verdict_of(result, [node.expr, *base], self.nodes.values())

verify_derivations

verify_derivations()

Re-check every stored derivation against the solver.

Derivations are already entails-verified at insertion time in add_derived; this is an opt-in audit for callers who want to re-establish that guarantee (e.g. over a deserialized graph), not something the solving pipeline runs per round.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def verify_derivations(self) -> list[str]:
    """Re-check every stored derivation against the solver.

    Derivations are already entails-verified at insertion time in
    ``add_derived``; this is an opt-in audit for callers who want to
    re-establish that guarantee (e.g. over a deserialized graph), not
    something the solving pipeline runs per round.
    """
    errors: list[str] = []

    for conclusion_id, derivations in self.derivations.items():
        for derivation in derivations:
            premises = [
                self.fact(premise_id).expr for premise_id in derivation.premise_ids
            ]
            conclusion = self.fact(conclusion_id).expr

            if (
                self.reasoning_backend.notary.notarise(
                    premises,
                    conclusion,
                    self.reasoning_backend.semantics,
                )
                is not Entailment.PROVED
            ):
                errors.append(
                    f"Invalid derivation {conclusion_id}: {derivation.rule}"
                )

    return errors

explanation_for

explanation_for(target)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_for(self, target: FactToken[Any]) -> list[str]:
    return explanation_lines(self.dag, target.id)

explanation_subgraph_for

explanation_subgraph_for(target)

Return the minimal ancestor subgraph explaining target.

This is the graph-shaped counterpart to explanation_for. It keeps the same immutable graph wrapper, but restricts the DAG to the target fact plus all graph nodes that feed into it, including derivation steps.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explanation_subgraph_for(
    self,
    target: FactToken[Any],
) -> FactGraph[StateT]:
    """Return the minimal ancestor subgraph explaining ``target``.

    This is the graph-shaped counterpart to ``explanation_for``. It keeps
    the same immutable graph wrapper, but restricts the DAG to the target
    fact plus all graph nodes that feed into it, including derivation steps.
    """
    target_id = target.id

    if target_id not in self.dag:
        raise KeyError(f"Unknown fact id: {target_id}")

    sliced_dag = self.dag.slice_for(target_id)

    by_expr = {
        key: fact_id
        for key, fact_id in self.by_expr.items()
        if fact_id in sliced_dag
    }

    return replace(
        self,
        dag=sliced_dag,
        by_expr=by_expr,
    )

explain_check

explain_check(check)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explain_check(
    self: FactGraph[Evidence[Consistent, Saturated]],
    check: FactToken[Any],
) -> tuple[bool, FactGraph[Evidence[Consistent, Saturated]]]:
    check_id = check.id
    if check_id not in self.dag:
        raise KeyError(f"Check token does not belong to this graph: {check_id}")
    check_node = self.fact(check_id)
    if check_node.kind is not FactKind.CHECK:
        raise ValueError(f"Not a check token: {check_id}")
    if self.dag.in_degree(check_id) > 0:
        return True, self

    return next(
        iter(
            (True, self.apply_explanation(x))
            for x in self.reasoning_backend.explanation.explain(
                self.explanation_input((check,)),
                self.reasoning_backend.semantics,
            )
        ),
        (False, self),
    )

apply_explanation

apply_explanation(proposal)

Attach one proposed explanation to a check, after verifying it.

The verification is the whole point of the method, and it is not equivalence. What is required is one-way entailment — the proposal's premises must prove the check, checked by the reasoning backend's notary — so a set of facts that jointly imply a check is a valid explanation of it even when no member restates it and the implication does not run the other way. amount = 10000 explains amount >= 10000; the reverse does not hold and does not need to.

Premises are plural for the same reason. Nothing here privileges a single fact, and a proposer that only ever offers one is leaving valid explanations on the table rather than obeying a rule.

A proposal whose premises do not entail the check raises rather than being dropped. An explanation stage is free to find nothing; it is not free to attach something wrong, and silently discarding a bad proposal would turn a proposer's bug into a quietly emptier DAG.

Returns:

Type	Description
FactGraph[StateT]	A new graph with one ExplanationNode joining the premises to the
FactGraph[StateT]	check. The graph is immutable, so the receiver is unchanged.

Raises:

Type	Description
KeyError	if the check id is not in this graph.
ValueError	if the id names something other than a check, or if the premises do not entail it.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def apply_explanation(
    self,
    proposal: ExplanationProposal,
) -> FactGraph[StateT]:
    """Attach one proposed explanation to a check, after verifying it.

    The verification is the whole point of the method, and it is *not*
    equivalence. What is required is one-way entailment — the proposal's
    premises must prove the check, checked by the reasoning backend's
    notary — so a set of facts that jointly imply a check is a valid
    explanation of it even when no member restates it and the implication
    does not run the other way. `amount = 10000` explains
    `amount >= 10000`; the reverse does not hold and does not need to.

    Premises are plural for the same reason. Nothing here privileges a
    single fact, and a proposer that only ever offers one is leaving valid
    explanations on the table rather than obeying a rule.

    A proposal whose premises do not entail the check raises rather than
    being dropped. An explanation stage is free to find nothing; it is not
    free to attach something wrong, and silently discarding a bad proposal
    would turn a proposer's bug into a quietly emptier DAG.

    Returns:
        A new graph with one `ExplanationNode` joining the premises to the
        check. The graph is immutable, so the receiver is unchanged.

    Raises:
        KeyError: if the check id is not in this graph.
        ValueError: if the id names something other than a check, or if
            the premises do not entail it.
    """
    if proposal.check_id not in self.dag:
        raise KeyError(
            f"Check token does not belong to this graph: {proposal.check_id}"
        )
    check_node = self.fact(proposal.check_id)
    if check_node.kind is not FactKind.CHECK:
        raise ValueError(f"Not a check token: {proposal.check_id}")
    # Declarations arrive as expressions rather than ids, because a
    # dimension's invariant has no node until something cites it. They are
    # materialised here, before the notary runs, so the entailment is
    # checked against exactly the premises the DAG will record -- attaching
    # a proposal whose declared half was never notarised would be the one
    # way this method could pass something wrong.
    graph: FactGraph[StateT] = self
    declared_ids: list[FactId] = []
    for dimension in proposal.declarations:
        declared_id, graph = graph._with_declaration(dimension)
        declared_ids.append(declared_id)
    premise_ids = (*proposal.premises, *declared_ids)
    premises = graph._premise_nodes(premise_ids)
    if (
        graph.reasoning_backend.notary.notarise(
            [premise.expr for premise in premises],
            check_node.expr,
            graph.reasoning_backend.semantics,
        )
        is not Entailment.PROVED
    ):
        raise ValueError("Explanation premises do not entail the check.")
    step = ExplanationNode(
        id=graph._fresh_derivation_id(),
        rule=proposal.rule,
    )
    return replace(
        graph,
        dag=graph.dag.with_explanation(
            step,
            premises=premise_ids,
            check=proposal.check_id,
        ),
        next_derivation_index=graph.next_derivation_index + 1,
    )

FactGraphExplanationBackend dataclass

Propose check explanations from the established facts, two ways.

The first is a scan for a single established fact equivalent to the check. It is cheap, it produces a one-premise explanation a reader can take in at a glance, and it is what every explained check in this engine used to come from.

It is also strictly weaker than the rule the graph enforces. What :meth:FactGraph.apply_explanation requires of a proposal is one-way entailment — the premises must prove the check — and equivalence is that twice over. So a check the facts genuinely entail could be refused an explanation for the sole reason that no one fact restates it. Two shapes hit this constantly: an ordering claim entailed by two separate equalities (carol = 675 and alice = 540 give carol > alice), and a comparison against the constant a fact pins (amount = 10000 entails amount >= 10000 and is not equivalent to it, with no second premise involved at all). Both are recorded as measured gaps in joint-premise-explanations.md.

The second route closes them by asking the solver the question the gate actually asks. If premises ∧ ¬check is unsatisfiable then the premises entail the check, and z3's unsat core names a subset of them that suffices. That subset is then shrunk by deletion until it is minimal: every premise cited is one whose removal breaks the entailment.

Three things make the core safe to hand to the gate rather than merely plausible:

• the graph reaching this point is consistent, so the premises alone are satisfiable and ¬check must be in any unsat core — which means the rest of the core entails the check, rather than being jointly contradictory for reasons of its own;
• the solve asserts the established facts and every mapped slot's declared invariant, which is the same base classify reasons from. A declaration is not a fact anyone authored, so it is cited only when the core names it and is then materialised as a DECLARED node — in exactly when load-bearing, and absent otherwise (joint-premise-explanations.md step 5);
• terms in the core that are neither — ¬check itself, and the True the backend tracks alongside — are dropped rather than cited, which is the same filter stated from the other side.

The equivalence scan stays first, and not only for speed: where one fact does restate the check, "this check is that fact" is a better explanation than a set the solver happened to find sufficient.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class FactGraphExplanationBackend:
    """Propose check explanations from the established facts, two ways.

    The first is a scan for a single established fact *equivalent* to the
    check. It is cheap, it produces a one-premise explanation a reader can take
    in at a glance, and it is what every explained check in this engine used to
    come from.

    It is also strictly weaker than the rule the graph enforces. What
    :meth:`FactGraph.apply_explanation` requires of a proposal is one-way
    entailment — the premises must prove the check — and equivalence is that
    twice over. So a check the facts genuinely entail could be refused an
    explanation for the sole reason that no *one* fact restates it. Two shapes
    hit this constantly: an ordering claim entailed by two separate equalities
    (``carol = 675`` and ``alice = 540`` give ``carol > alice``), and a
    comparison against the constant a fact pins (``amount = 10000`` entails
    ``amount >= 10000`` and is not equivalent to it, with no second premise
    involved at all). Both are recorded as measured gaps in
    joint-premise-explanations.md.

    The second route closes them by asking the solver the question the gate
    actually asks. If ``premises ∧ ¬check`` is unsatisfiable then the premises
    entail the check, and z3's unsat core names a subset of them that suffices.
    That subset is then shrunk by deletion until it is *minimal*: every premise
    cited is one whose removal breaks the entailment.

    Three things make the core safe to hand to the gate rather than merely
    plausible:

    * the graph reaching this point is *consistent*, so the premises alone are
      satisfiable and ``¬check`` must be in any unsat core — which means the
      rest of the core entails the check, rather than being jointly
      contradictory for reasons of its own;
    * the solve asserts the established facts **and** every mapped slot's
      declared invariant, which is the same base ``classify`` reasons from. A
      declaration is not a fact anyone authored, so it is cited only when the
      core names it and is then materialised as a ``DECLARED`` node — in
      exactly when load-bearing, and absent otherwise
      (joint-premise-explanations.md step 5);
    * terms in the core that are neither — ``¬check`` itself, and the ``True``
      the backend tracks alongside — are dropped rather than cited, which is
      the same filter stated from the other side.

    The equivalence scan stays first, and not only for speed: where one fact
    does restate the check, "this check is that fact" is a better explanation
    than a set the solver happened to find sufficient.
    """

    def explain(
        self,
        input_: ExplanationInput[BoolRef],
        semantics: SemanticBackend,
    ) -> Iterable[ExplanationProposal]:
        for check_node in input_.checks:
            proposal = self._equivalent_fact(
                check_node, input_.established, semantics
            ) or self._entailing_core(
                check_node, input_.established, input_.declarations, semantics
            )
            if proposal is not None:
                yield proposal

    def _equivalent_fact(
        self,
        check: FactNode[BoolRef],
        established: tuple[FactNode[BoolRef], ...],
        semantics: SemanticBackend,
    ) -> ExplanationProposal | None:
        """The first established fact that restates the check, if any."""
        for node in established:
            if (
                equivalent(node.expr, check.expr, backend=semantics)
                is Entailment.PROVED
            ):
                return ExplanationProposal(
                    check_id=check.id,
                    premises=(node.id,),
                    rule=ExplanationRule.RESTATEMENT,
                )
        return None

    def _entailing_core(
        self,
        check: FactNode[BoolRef],
        established: tuple[FactNode[BoolRef], ...],
        declarations: Mapping[str, BoolRef],
        semantics: SemanticBackend,
    ) -> ExplanationProposal | None:
        """The premises the solver needed to refute the check's negation.

        ``None`` when the premises do not entail the check at all (the check is
        `FALSIFIED` or `UNKNOWN`), and when the core names none of them. That
        last case covers two different things on purpose: a check entailed by
        nothing is a tautology and citing the empty set explains it to nobody,
        and a backend that reports `UNSAT` without a core has not said which
        premises mattered. Naming all of them instead would be an explanation
        in name only.
        """
        # `as_bool_ref` because z3's `Not` is typed as returning `BoolRef |
        # Probe`, and a list mixing the two is not the `Sequence[BoolRef]` the
        # backend takes. The narrowing is real rather than a cast: `Not` of a
        # `BoolRef` is a `BoolRef`, and anything else raises here rather than
        # reaching the solver.
        negation = as_bool_ref(Not(check.expr))
        # One order for both premise families, and the same one the Rust route
        # labels them in: facts as the reader met them, then declarations by
        # slot. Z3 promises a *sufficient* core and nothing about its order,
        # and two solver invocations over the same premises do return it
        # differently -- measured between this backend and
        # `RustExplanationBackend`, which asks the same question of the same Z3
        # and got `(f2, f1)` for this backend's `(f1, f2)`. Deletion below
        # consumes this order too, so it is not only how the premises are
        # presented but which minimal subset is reached.
        candidates: tuple[_Premise, ...] = (
            *(_FactPremise(node.expr, node.id) for node in established),
            *(
                _DeclaredPremise(declarations[dimension], dimension)
                for dimension in sorted(declarations)
            ),
        )
        result = semantics.solve([*(premise.expr for premise in candidates), negation])
        if result.status is not SolveStatus.UNSAT:
            return None
        # Minimised from *every* candidate, not from the core Z3 returned.
        #
        # The core is where this started and it is not a function of the
        # record: measured 2026-09-19 over 40 solves of one parsed
        # `departure-chain` request, `carol_after_alice` came back with three
        # different sufficient cores -- 37 runs naming bob's departure and the
        # offset that fixes it, 2 naming alice's departure, 1 naming the two
        # offsets and neither departure. Every one of them entails the check;
        # Z3 promises a sufficient subset and nothing about *which*, and the
        # subset it finds moves with its own search.
        #
        # Deletion is order-deterministic and was already relied on for that,
        # but only downstream of the core, so a varying start reached a
        # varying minimal set -- and a check whose core happened to name no
        # derived fact lost its whole chain on the page, 3 facts and no step
        # where the same request usually draws 6 and 2. Starting from the
        # candidates makes the answer a function of the record: the order is
        # fixed above, deletion is deterministic in it, and Z3's choice is
        # used for the entailment verdict rather than for the content.
        #
        # It costs one solve per candidate instead of one per core premise.
        # Both are the same small queries, and an explanation that changes
        # between two builds of one commit is not a cheaper explanation.
        kept = _minimised(list(candidates), negation, semantics)
        # A kept restatement is cited as what it restates (`first_statements`),
        # in the order the reader met them, and once.
        first = first_statements(established)
        cited_facts = {
            first[premise.id] for premise in kept if isinstance(premise, _FactPremise)
        }
        premises = tuple(node.id for node in established if node.id in cited_facts)
        cited = tuple(
            premise.id for premise in kept if isinstance(premise, _DeclaredPremise)
        )
        if not premises and not cited:
            return None
        return ExplanationProposal(
            check_id=check.id,
            premises=premises,
            rule=ExplanationRule.SUFFICIENCY,
            declarations=cited,
        )

explain

explain(input_, semantics)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def explain(
    self,
    input_: ExplanationInput[BoolRef],
    semantics: SemanticBackend,
) -> Iterable[ExplanationProposal]:
    for check_node in input_.checks:
        proposal = self._equivalent_fact(
            check_node, input_.established, semantics
        ) or self._entailing_core(
            check_node, input_.established, input_.declarations, semantics
        )
        if proposal is not None:
            yield proposal

ForwardDerivationBackend dataclass

The Python structural rules behind the derivation interface.

The same pipeline RustDerivationBackend runs -- flatten the facts into records, run the structural step, reconstruct -- with the Python rules in the middle instead of the Rust core. So the two engines differ in exactly one function, and that function has the same signature on both sides.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ForwardDerivationBackend:
    """The Python structural rules behind the derivation interface.

    The same pipeline ``RustDerivationBackend`` runs -- flatten the facts into
    records, run the structural step, reconstruct -- with the Python rules in
    the middle instead of the Rust core. So the two engines differ in exactly
    one function, and that function has the same signature on both sides.
    """

    def derive(
        self,
        input_: DerivationInput[BoolRef],
    ) -> Iterable[DerivationProposal[BoolRef]]:
        records, lookup = linear_records(input_.established)
        yield from proposals_from_records(derive(records), lookup)

derive

derive(input_)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def derive(
    self,
    input_: DerivationInput[BoolRef],
) -> Iterable[DerivationProposal[BoolRef]]:
    records, lookup = linear_records(input_.established)
    yield from proposals_from_records(derive(records), lookup)

IngestedPuzzle dataclass

Bases: Generic[PuzzleT]

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class IngestedPuzzle(Generic[PuzzleT]):
    puzzle: PuzzleT
    graph: ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]]
    check_tokens: dict[str, FactToken[Any]]

puzzle instance-attribute

puzzle

graph instance-attribute

graph

check_tokens instance-attribute

check_tokens

PuzzleSolver dataclass

Configured callable that solves puzzles with one reasoning backend.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class PuzzleSolver:
    """Configured callable that solves puzzles with one reasoning backend."""

    backend: ReasoningBackend = field(default_factory=default_reasoning_backend)
    #: Builds the empty graph to ingest into; defaults to the Python
    #: ``FactGraph``. A different factory (e.g. a future Rust-native engine)
    #: swaps the graph implementation here without touching call sites --
    #: see ``ReasoningGraphBackend`` (reasoning/types.py) for the contract
    #: a substitute must satisfy.
    graph_factory: (
        Callable[[], ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]]] | None
    ) = None

    def ingest[PuzzleT](self, puzzle: PuzzleT) -> IngestedPuzzle[PuzzleT]:
        """Parse a puzzle without attaching this solver's backend.

        A `PuzzleProblem` (a `@puzzle` entry point) is solved as its
        instance is, and stays what ``.puzzle`` reports back.
        """
        instance = puzzle.instance if isinstance(puzzle, PuzzleProblem) else puzzle
        if not is_dataclass(instance):
            raise TypeError(f"Expected dataclass puzzle schema, got {puzzle!r}")
        # The authoring rules the wire path holds a puzzle to hold here too:
        # an event's time is its occurrence's, never a field (E1c).
        request = puzzle_to_solve_request(instance)
        if request.profile is not None:
            # An event program -- a state question's definition, or only an
            # absence or a precondition constraining what was declared -- is
            # wire, from the rules lowering; this graph is built from the
            # puzzle's own expressions and would drop it. Refused rather than
            # answered wrongly.
            raise NotImplementedError(
                "a puzzle with an event program (holds_at, an absence, an "
                "effect) is solved through its request: "
                "puzzle_to_solve_request(puzzle), then a Solver"
            )

        graph: ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]] = (
            FactGraph.empty() if self.graph_factory is None else self.graph_factory()
        )
        check_tokens: dict[str, FactToken[Any]] = {}

        for field_info in fields(instance):
            subject_name = field_info.name
            block = getattr(instance, subject_name)

            # `puzzle_to_solve_request` above refused any other field.
            assert isinstance(block, SubjectFacts)

            if block.given is not None:
                bound_given = block.given.bind(subject_name)
                _given_token, graph = graph.add_given(
                    bound_given,
                    subject_name=subject_name,
                )

            for check_label, check_prop in block.checks.items():
                bound_check = check_prop.bind(subject_name)
                check_token, graph = graph.add_check(
                    bound_check,
                    subject_name=subject_name,
                    check_label=check_label,
                )
                check_tokens[check_label] = check_token

        return IngestedPuzzle(
            puzzle=puzzle,
            graph=graph,
            check_tokens=check_tokens,
        )

    def __call__[PuzzleT](self, puzzle: PuzzleT) -> SolvedPuzzle[PuzzleT]:
        """Ingest, check consistency, saturate, and attach checks."""
        ingested = self.ingest(puzzle)
        graph = ingested.graph.with_reasoning_backend(self.backend)
        saturated = graph.check_consistent().saturate()
        final_graph = saturated
        proposals = self.backend.explanation.explain(
            saturated.explanation_input(ingested.check_tokens.values()),
            self.backend.semantics,
        )
        for proposal in proposals:
            final_graph = final_graph.apply_explanation(proposal)

        return SolvedPuzzle(
            puzzle=ingested.puzzle,
            graph=final_graph,
            check_tokens=ingested.check_tokens,
        )

backend class-attribute instance-attribute

backend = field(default_factory=default_reasoning_backend)

graph_factory class-attribute instance-attribute

graph_factory = None

ingest

ingest(puzzle)

Parse a puzzle without attaching this solver's backend.

A PuzzleProblem (a @puzzle entry point) is solved as its instance is, and stays what .puzzle reports back.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def ingest[PuzzleT](self, puzzle: PuzzleT) -> IngestedPuzzle[PuzzleT]:
    """Parse a puzzle without attaching this solver's backend.

    A `PuzzleProblem` (a `@puzzle` entry point) is solved as its
    instance is, and stays what ``.puzzle`` reports back.
    """
    instance = puzzle.instance if isinstance(puzzle, PuzzleProblem) else puzzle
    if not is_dataclass(instance):
        raise TypeError(f"Expected dataclass puzzle schema, got {puzzle!r}")
    # The authoring rules the wire path holds a puzzle to hold here too:
    # an event's time is its occurrence's, never a field (E1c).
    request = puzzle_to_solve_request(instance)
    if request.profile is not None:
        # An event program -- a state question's definition, or only an
        # absence or a precondition constraining what was declared -- is
        # wire, from the rules lowering; this graph is built from the
        # puzzle's own expressions and would drop it. Refused rather than
        # answered wrongly.
        raise NotImplementedError(
            "a puzzle with an event program (holds_at, an absence, an "
            "effect) is solved through its request: "
            "puzzle_to_solve_request(puzzle), then a Solver"
        )

    graph: ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]] = (
        FactGraph.empty() if self.graph_factory is None else self.graph_factory()
    )
    check_tokens: dict[str, FactToken[Any]] = {}

    for field_info in fields(instance):
        subject_name = field_info.name
        block = getattr(instance, subject_name)

        # `puzzle_to_solve_request` above refused any other field.
        assert isinstance(block, SubjectFacts)

        if block.given is not None:
            bound_given = block.given.bind(subject_name)
            _given_token, graph = graph.add_given(
                bound_given,
                subject_name=subject_name,
            )

        for check_label, check_prop in block.checks.items():
            bound_check = check_prop.bind(subject_name)
            check_token, graph = graph.add_check(
                bound_check,
                subject_name=subject_name,
                check_label=check_label,
            )
            check_tokens[check_label] = check_token

    return IngestedPuzzle(
        puzzle=puzzle,
        graph=graph,
        check_tokens=check_tokens,
    )

ReasoningBackend dataclass

Composite, graph-independent reasoning capabilities.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class ReasoningBackend:
    """Composite, graph-independent reasoning capabilities."""

    semantics: SemanticBackend = Z3_SEMANTICS
    algebra: ExpressionAlgebra[Boolish_Bound, BoolRef] = Z3_ALGEBRA
    notary: DerivationNotary[BoolRef, SemanticBackend] = ENTAILS_NOTARY
    derivation: DerivationBackend = ForwardDerivationBackend()
    explanation: ExplanationBackend = FactGraphExplanationBackend()
    max_rounds: int = 20

    def __enter__(self) -> ReasoningBackend:
        return self

    def __exit__(
        self,
        exc_type: type[BaseException] | None,
        exc_value: BaseException | None,
        traceback: object | None,
    ) -> None:
        return None

semantics class-attribute instance-attribute

semantics = Z3_SEMANTICS

algebra class-attribute instance-attribute

algebra = Z3_ALGEBRA

notary class-attribute instance-attribute

notary = ENTAILS_NOTARY

derivation class-attribute instance-attribute

derivation = ForwardDerivationBackend()

explanation class-attribute instance-attribute

explanation = FactGraphExplanationBackend()

max_rounds class-attribute instance-attribute

max_rounds = 20

SolveResult dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class SolveResult:
    status: SolveStatus
    model: ModelRef | None = None
    core: tuple[BoolRef, ...] = ()
    #: z3 rlimit units this solve consumed. Reported rather than inferred: an
    #: operation-wide step budget cannot be decremented by a cost nobody
    #: measured, and z3 only knows the count after the check has run.
    steps_used: int = 0

status instance-attribute

status

model class-attribute instance-attribute

model = None

core class-attribute instance-attribute

core = ()

steps_used class-attribute instance-attribute

steps_used = 0

SolveStatus

Bases: str, Enum

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

class SolveStatus(str, Enum):
    SAT = "SAT"
    UNSAT = "UNSAT"
    UNKNOWN = "UNKNOWN"
    #: The solver hit its resource budget (timeout/rlimit). Kept distinct from
    #: UNKNOWN so a resource exhaustion is never mistaken for a theory verdict.
    TIMEOUT = "TIMEOUT"
    #: Someone asked the solver to stop, and it did. Distinct from TIMEOUT for
    #: the same reason TIMEOUT is distinct from UNKNOWN: a solve abandoned on
    #: purpose is not a budget overrun, and reading it as one would make a
    #: disconnecting client look like a service too slow to answer.
    #:
    #: It is also the confirmation a permit release can key on. The plan in
    #: solver-interruption.md requires the permit be held until the worker has
    #: *stopped*, never released on the request-side cancellation --- and this
    #: status is the worker saying so, rather than the caller inferring it from
    #: elapsed time.
    INTERRUPTED = "INTERRUPTED"

SAT class-attribute instance-attribute

SAT = 'SAT'

UNSAT class-attribute instance-attribute

UNSAT = 'UNSAT'

UNKNOWN class-attribute instance-attribute

UNKNOWN = 'UNKNOWN'

TIMEOUT class-attribute instance-attribute

TIMEOUT = 'TIMEOUT'

INTERRUPTED class-attribute instance-attribute

INTERRUPTED = 'INTERRUPTED'

SolvedPuzzle dataclass

Bases: Generic[PuzzleT]

A puzzle after ingestion, consistency check, saturation, and attach.

graph is the final explanation DAG; check_tokens maps each check label to the fact recording that candidate proposition.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class SolvedPuzzle(Generic[PuzzleT]):
    """A puzzle after ingestion, consistency check, saturation, and attach.

    ``graph`` is the final explanation DAG; ``check_tokens`` maps each check
    label to the fact recording that candidate proposition.
    """

    puzzle: PuzzleT
    graph: ReasoningGraphBackend[Evidence[Consistent, Saturated]]
    check_tokens: dict[str, FactToken[Any]]

puzzle instance-attribute

puzzle

graph instance-attribute

graph

check_tokens instance-attribute

check_tokens

Z3ExpressionAlgebra dataclass

The z3 spelling of :class:ExpressionAlgebra.

Thin on purpose: each method is one of the module-level helpers the graph used to call directly, so behaviour is identical and the functions stay independently usable. ingress is as_z3_bool — the one place the authored frontend's booleans become stored BoolRef values.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class Z3ExpressionAlgebra:
    """The z3 spelling of :class:`ExpressionAlgebra`.

    Thin on purpose: each method is one of the module-level helpers the graph
    used to call directly, so behaviour is identical and the functions stay
    independently usable. ``ingress`` is ``as_z3_bool`` — the one place the
    authored frontend's booleans become stored ``BoolRef`` values.
    """

    def ingress(self, expr: Boolish_Bound) -> BoolRef:
        return as_z3_bool(expr)

    def normalise(self, expr: BoolRef) -> BoolRef:
        return as_bool_ref(stable_simplify(expr))

    def key(self, expr: BoolRef) -> str:
        return expr_key(expr)

    def render(self, expr: BoolRef, slots: Mapping[str, Dimension[Any]]) -> str:
        return render_fact(expr, slots=slots)

    def invariants(self, slots: Mapping[str, Dimension[Any]]) -> list[BoolRef]:
        return list(slot_invariant_terms(slots))

    def declarations(self, slots: Mapping[str, Dimension[Any]]) -> dict[str, BoolRef]:
        return declarations(slots)

ingress

ingress(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def ingress(self, expr: Boolish_Bound) -> BoolRef:
    return as_z3_bool(expr)

normalise

normalise(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def normalise(self, expr: BoolRef) -> BoolRef:
    return as_bool_ref(stable_simplify(expr))

key

key(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def key(self, expr: BoolRef) -> str:
    return expr_key(expr)

render

render(expr, slots)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def render(self, expr: BoolRef, slots: Mapping[str, Dimension[Any]]) -> str:
    return render_fact(expr, slots=slots)

invariants

invariants(slots)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def invariants(self, slots: Mapping[str, Dimension[Any]]) -> list[BoolRef]:
    return list(slot_invariant_terms(slots))

declarations

declarations(slots)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def declarations(self, slots: Mapping[str, Dimension[Any]]) -> dict[str, BoolRef]:
    return declarations(slots)

Z3SemanticBackend dataclass

Default semantic backend using Z3's solver and unsat cores.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@dataclass(frozen=True)
class Z3SemanticBackend:
    """Default semantic backend using Z3's solver and unsat cores."""

    solver_factory: Callable[[], Any] = field(default=thread_solver, repr=False)
    timeout_ms: int | None = None
    rlimit: int | None = None

    def solve(self, assertions: Sequence[BoolRef]) -> SolveResult:
        return check_with_core(
            assertions,
            BoolVal(True, ctx=z3_context()),
            solver_factory=self.solver_factory,
            timeout_ms=self.timeout_ms,
            rlimit=self.rlimit,
        )

    def asking(self, terms: Sequence[BoolRef], against: Sequence[BoolRef]) -> Asking:
        return _Assumed(self, tuple(terms), tuple(against))

solver_factory class-attribute instance-attribute

solver_factory = field(default=thread_solver, repr=False)

timeout_ms class-attribute instance-attribute

timeout_ms = None

rlimit class-attribute instance-attribute

rlimit = None

solve

solve(assertions)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def solve(self, assertions: Sequence[BoolRef]) -> SolveResult:
    return check_with_core(
        assertions,
        BoolVal(True, ctx=z3_context()),
        solver_factory=self.solver_factory,
        timeout_ms=self.timeout_ms,
        rlimit=self.rlimit,
    )

asking

asking(terms, against)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def asking(self, terms: Sequence[BoolRef], against: Sequence[BoolRef]) -> Asking:
    return _Assumed(self, tuple(terms), tuple(against))

Consistent

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class Consistent:
    pass

Entailment

Bases: Enum

A three-valued entailment verdict.

Deliberately a plain Enum, not IntEnum: a verdict must not be collapsible to bool — being three-valued is the whole point. Always compare with is (result is Entailment.PROVED); never use it in a boolean context, where "the solver gave up" would silently read as success.

The values form a conjunction lattice in which REFUTED is absorbing (one countermodel refutes the whole) and PROVED is the identity (an all-proved conjunction is proved), with UNDECIDED between. The ordering is expressed directly in :meth:conjunction, not smuggled into integer values.

• PROVED — the premises entail the conclusion (¬conclusion unsat).
• REFUTED — a countermodel exists (premises ∧ ¬conclusion sat); the entailment is definitely false, not merely unproven. The witnessing model lives on the SolveResult / classify path, not here.
• UNDECIDED — the solver could not decide (an encoding/theory limit).

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class Entailment(Enum):
    """A three-valued entailment verdict.

    Deliberately a plain ``Enum``, not ``IntEnum``: a verdict must not be
    collapsible to ``bool`` — being three-valued is the whole point. Always
    compare with ``is`` (``result is Entailment.PROVED``); never use it in a
    boolean context, where "the solver gave up" would silently read as success.

    The values form a *conjunction lattice* in which ``REFUTED`` is **absorbing**
    (one countermodel refutes the whole) and ``PROVED`` is the **identity**
    (an all-proved conjunction is proved), with ``UNDECIDED`` between. The
    ordering is expressed directly in :meth:`conjunction`, not smuggled into
    integer values.

    - ``PROVED``    — the premises entail the conclusion (``¬conclusion`` unsat).
    - ``REFUTED``   — a countermodel exists (``premises ∧ ¬conclusion`` sat); the
                      entailment is *definitely false*, not merely unproven. The
                      witnessing model lives on the ``SolveResult`` / ``classify``
                      path, not here.
    - ``UNDECIDED`` — the solver could not decide (an encoding/theory limit).
    """

    REFUTED = "REFUTED"
    UNDECIDED = "UNDECIDED"
    PROVED = "PROVED"

    def meet(self, other: Entailment) -> Entailment:
        """Binary Kleene conjunction (∧) — the monoid op behind `conjunction`.

        ``REFUTED`` is absorbing, ``PROVED`` is the identity, ``UNDECIDED`` sits
        between. Raises on a non-``Entailment`` rather than returning
        ``NotImplemented`` (this is a plain method, not an operator dunder, so
        ``NotImplemented`` would silently leak as a value).
        """
        if not isinstance(other, Entailment):
            raise TypeError(f"meet expects an Entailment, got {other!r}")
        return next(x for x in Entailment if x in (self, other))

    @classmethod
    def conjunction(cls, results: Iterable[Entailment]) -> Entailment:
        """Fold ``meet`` over obligations that must *all* hold.

        ``REFUTED`` is the absorbing element, so this short-circuits: given a
        generator of solver calls, it stops at the first countermodel instead of
        running the rest. The empty conjunction is ``PROVED`` (vacuous truth).
        """
        # `Entailment.meet`, not `cls.meet`: an Enum with members cannot be
        # subclassed, so the `Self` a classmethod's `cls` carries is empty
        # generality -- and it pins `reduce`'s accumulator to `Self@Entailment`,
        # which then refuses both the plain `Entailment` returns and the
        # `PROVED` identity element.
        return functools.reduce(
            Entailment.meet,
            takewhile_inclusive(lambda r: r is not Entailment.REFUTED, results),
            Entailment.PROVED,
        )

REFUTED class-attribute instance-attribute

REFUTED = 'REFUTED'

UNDECIDED class-attribute instance-attribute

UNDECIDED = 'UNDECIDED'

PROVED class-attribute instance-attribute

PROVED = 'PROVED'

meet

meet(other)

Binary Kleene conjunction (∧) — the monoid op behind conjunction.

REFUTED is absorbing, PROVED is the identity, UNDECIDED sits between. Raises on a non-Entailment rather than returning NotImplemented (this is a plain method, not an operator dunder, so NotImplemented would silently leak as a value).

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def meet(self, other: Entailment) -> Entailment:
    """Binary Kleene conjunction (∧) — the monoid op behind `conjunction`.

    ``REFUTED`` is absorbing, ``PROVED`` is the identity, ``UNDECIDED`` sits
    between. Raises on a non-``Entailment`` rather than returning
    ``NotImplemented`` (this is a plain method, not an operator dunder, so
    ``NotImplemented`` would silently leak as a value).
    """
    if not isinstance(other, Entailment):
        raise TypeError(f"meet expects an Entailment, got {other!r}")
    return next(x for x in Entailment if x in (self, other))

conjunction classmethod

conjunction(results)

Fold meet over obligations that must all hold.

REFUTED is the absorbing element, so this short-circuits: given a generator of solver calls, it stops at the first countermodel instead of running the rest. The empty conjunction is PROVED (vacuous truth).

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

@classmethod
def conjunction(cls, results: Iterable[Entailment]) -> Entailment:
    """Fold ``meet`` over obligations that must *all* hold.

    ``REFUTED`` is the absorbing element, so this short-circuits: given a
    generator of solver calls, it stops at the first countermodel instead of
    running the rest. The empty conjunction is ``PROVED`` (vacuous truth).
    """
    # `Entailment.meet`, not `cls.meet`: an Enum with members cannot be
    # subclassed, so the `Self` a classmethod's `cls` carries is empty
    # generality -- and it pins `reduce`'s accumulator to `Self@Entailment`,
    # which then refuses both the plain `Entailment` returns and the
    # `PROVED` identity element.
    return functools.reduce(
        Entailment.meet,
        takewhile_inclusive(lambda r: r is not Entailment.REFUTED, results),
        Entailment.PROVED,
    )

DerivationBackend

Bases: Protocol

Propose one round of derived facts from an immutable graph snapshot.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class DerivationBackend(Protocol):
    """Propose one round of derived facts from an immutable graph snapshot."""

    def derive(
        self,
        input_: DerivationInput,
    ) -> Iterable[DerivationProposal]: ...

derive

derive(input_)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def derive(
    self,
    input_: DerivationInput,
) -> Iterable[DerivationProposal]: ...

DerivationNotary

Bases: Protocol[ExprT_contra, SemanticsT_contra]

Judge whether premises genuinely support a proposed conclusion.

Phase 7b's insertion-gate seam. A graph refuses any step its notary does not prove, and its re-audit re-asks the same judge — the gate is the graph's, the judgement the backend's. For z3 expressions the judge is entails (guardrail_solver.reasoning.EntailsNotary); a different conclusion type brings its own — the dialects' complete-unless-rogue needs enumeration of the graph for rogue facts, which no entails call can decide. Answers the three-valued :class:Entailment, never a bool: "the solver gave up" must not read as either verdict.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class DerivationNotary(Protocol[ExprT_contra, SemanticsT_contra]):
    """Judge whether premises genuinely support a proposed conclusion.

    Phase 7b's insertion-gate seam. A graph refuses any step its notary
    does not prove, and its re-audit re-asks the same judge — the gate is
    the graph's, the judgement the backend's. For z3 expressions the judge
    is ``entails`` (``guardrail_solver.reasoning.EntailsNotary``); a
    different conclusion type brings its own — the dialects'
    ``complete-unless-rogue`` needs enumeration of the graph for rogue
    facts, which no ``entails`` call can decide. Answers the three-valued
    :class:`Entailment`, never a bool: "the solver gave up" must not read
    as either verdict.
    """

    # The semantic capability each judgement family consults is its own —
    # the entails notary takes the solver's `SemanticBackend`, the dialect
    # enumeration notary the graph's established facts — so it is a type
    # *parameter*, named per family, rather than one shape for all of them.
    def notarise(
        self,
        premises: Sequence[ExprT_contra],
        conclusion: ExprT_contra,
        semantics: SemanticsT_contra,
    ) -> Entailment: ...

notarise

notarise(premises, conclusion, semantics)

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def notarise(
    self,
    premises: Sequence[ExprT_contra],
    conclusion: ExprT_contra,
    semantics: SemanticsT_contra,
) -> Entailment: ...

Evidence

Phantom evidence carried by a graph's static type.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class Evidence[ConsistencyT, SaturationT]:
    """Phantom evidence carried by a graph's static type."""

ExplanationBackend

Bases: Protocol

Propose explanation edges without mutating the fact graph.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class ExplanationBackend(Protocol):
    """Propose explanation edges without mutating the fact graph."""

    def explain(
        self,
        input_: ExplanationInput,
        semantics: SemanticBackend,
    ) -> Iterable[ExplanationProposal]: ...

explain

explain(input_, semantics)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def explain(
    self,
    input_: ExplanationInput,
    semantics: SemanticBackend,
) -> Iterable[ExplanationProposal]: ...

ExpressionAlgebra

Bases: Protocol[IngressT_contra, ExprT]

Everything a graph does to an expression that is not a solver query.

Phase 7b's keying seam. FactGraph used to call as_z3_bool, simplify, expr_key, render_fact and slot_invariant_terms directly, which is precisely what kept the graph z3-bound after the vocabulary stopped being so: identity, normalisation, ingress and rendering are operations on the expression type, so they belong to the backend that owns that type. The z3 spelling lives in guardrail_solver.reasoning.Z3ExpressionAlgebra; a dialect backend supplies its own over an AST-derived proposition type, and a graph never needs to know which.

Two parameters because ingress and storage may be different types: what an algebra accepts (the z3 algebra takes the solver's Boolish_Bound union of authored spellings) is not what it stores (BoolRef). Where nothing wider than the stored type exists to lower from, the two coincide — the dialect algebra is [DialectProp, DialectProp] and its ingress is identity.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class ExpressionAlgebra(Protocol[IngressT_contra, ExprT]):
    """Everything a graph does to an expression that is not a solver query.

    Phase 7b's keying seam. ``FactGraph`` used to call ``as_z3_bool``,
    ``simplify``, ``expr_key``, ``render_fact`` and ``slot_invariant_terms``
    directly, which is precisely what kept the *graph* z3-bound after the
    vocabulary stopped being so: identity, normalisation, ingress and
    rendering are operations on the expression type, so they belong to the
    backend that owns that type. The z3 spelling lives in
    ``guardrail_solver.reasoning.Z3ExpressionAlgebra``; a dialect backend
    supplies its own over an AST-derived proposition type, and a graph
    never needs to know which.

    Two parameters because ingress and storage may be different types: what
    an algebra accepts (the z3 algebra takes the solver's ``Boolish_Bound``
    union of authored spellings) is not what it stores (``BoolRef``). Where
    nothing wider than the stored type exists to lower from, the two
    coincide — the dialect algebra is ``[DialectProp, DialectProp]`` and
    its ingress is identity.
    """

    def ingress(self, expr: IngressT_contra) -> ExprT:
        """Lower an authored or raw proposition into the stored type."""
        ...

    def normalise(self, expr: ExprT) -> ExprT:
        """Canonicalise a stored expression; feeds :meth:`key` and display."""
        ...

    def key(self, expr: ExprT) -> str:
        """The identity under which a graph deduplicates this expression."""
        ...

    def render(self, expr: ExprT, slots: Mapping[str, Dimension[Any]]) -> str:
        """Default human text for a fact nobody captioned."""
        ...

    def invariants(self, slots: Mapping[str, Dimension[Any]]) -> list[ExprT]:
        """Standing assumptions the mapped slots' declarations imply."""
        ...

    def declarations(self, slots: Mapping[str, Dimension[Any]]) -> Mapping[str, ExprT]:
        """The same assumptions, one per dimension: its invariant over every
        mapped slot of it, conjoined in slot order, keyed by its name.

        Keyed because an explanation cites a declaration *by dimension*: the
        expression is the algebra's and does not cross an FFI boundary, so a
        proposal names the dimension and each engine realises the declaration
        for itself (joint-premise-explanations.md step 5).
        """
        ...

ingress

ingress(expr)

Lower an authored or raw proposition into the stored type.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def ingress(self, expr: IngressT_contra) -> ExprT:
    """Lower an authored or raw proposition into the stored type."""
    ...

normalise

normalise(expr)

Canonicalise a stored expression; feeds :meth:key and display.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def normalise(self, expr: ExprT) -> ExprT:
    """Canonicalise a stored expression; feeds :meth:`key` and display."""
    ...

key

key(expr)

The identity under which a graph deduplicates this expression.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def key(self, expr: ExprT) -> str:
    """The identity under which a graph deduplicates this expression."""
    ...

render

render(expr, slots)

Default human text for a fact nobody captioned.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def render(self, expr: ExprT, slots: Mapping[str, Dimension[Any]]) -> str:
    """Default human text for a fact nobody captioned."""
    ...

invariants

invariants(slots)

Standing assumptions the mapped slots' declarations imply.

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def invariants(self, slots: Mapping[str, Dimension[Any]]) -> list[ExprT]:
    """Standing assumptions the mapped slots' declarations imply."""
    ...

declarations

declarations(slots)

The same assumptions, one per dimension: its invariant over every mapped slot of it, conjoined in slot order, keyed by its name.

Keyed because an explanation cites a declaration by dimension: the expression is the algebra's and does not cross an FFI boundary, so a proposal names the dimension and each engine realises the declaration for itself (joint-premise-explanations.md step 5).

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

def declarations(self, slots: Mapping[str, Dimension[Any]]) -> Mapping[str, ExprT]:
    """The same assumptions, one per dimension: its invariant over every
    mapped slot of it, conjoined in slot order, keyed by its name.

    Keyed because an explanation cites a declaration *by dimension*: the
    expression is the algebra's and does not cross an FFI boundary, so a
    proposal names the dimension and each engine realises the declaration
    for itself (joint-premise-explanations.md step 5).
    """
    ...

ReasoningGraphBackend

Bases: Protocol[StateT_co]

The contract a fact-graph engine must satisfy to back PuzzleSolver.

Mirrors FactGraph's own phantom-typestate contract method for method, not a looser paraphrase of it: which methods are callable in which Evidence[ConsistencyT, SaturationT] state is a property of the interface every conforming graph must uphold (checked before saturated, saturated before its explanation is computed, ...), not an artifact of FactGraph's own implementation -- so a future implementation is held to the same illegal-call-sequences-are-a-type-error guarantee FactGraph already gives its own direct callers, not a weaker one just because it goes through this seam.

Deliberately looser on one axis: add_given/add_check carry Prop[Any]/FactToken[Any] rather than FactGraph's own [E: Boolish_Bound] value-level generic -- an orthogonal precision axis from the state invariants above, out of scope here.

@runtime_checkable only checks method presence, not signatures -- enough for a lightweight isinstance sanity probe, not a substitute for real type-checking at the call sites.

.dag's ProvenanceDag return type is Python/rustworkx-shaped as of this writing: there is no non-Python graph engine yet, so this describes the one real implementation rather than a speculative abstraction over a shape nothing has needed yet -- revisit if/when a second one exists.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

@runtime_checkable
class ReasoningGraphBackend(Protocol[StateT_co]):
    """The contract a fact-graph engine must satisfy to back ``PuzzleSolver``.

    Mirrors ``FactGraph``'s own phantom-typestate contract method for
    method, not a looser paraphrase of it: which methods are callable in
    which ``Evidence[ConsistencyT, SaturationT]`` state is a property of the
    *interface* every conforming graph must uphold (checked before
    saturated, saturated before its explanation is computed, ...), not an
    artifact of ``FactGraph``'s own implementation -- so a future
    implementation is held to the same illegal-call-sequences-are-a-type-error
    guarantee ``FactGraph`` already gives its own direct callers, not a
    weaker one just because it goes through this seam.

    Deliberately looser on one axis: ``add_given``/``add_check`` carry
    ``Prop[Any]``/``FactToken[Any]`` rather than ``FactGraph``'s own
    ``[E: Boolish_Bound]`` value-level generic -- an orthogonal precision
    axis from the state invariants above, out of scope here.

    ``@runtime_checkable`` only checks method *presence*, not signatures --
    enough for a lightweight ``isinstance`` sanity probe, not a substitute
    for real type-checking at the call sites.

    ``.dag``'s ``ProvenanceDag`` return type is Python/rustworkx-shaped as of
    this writing: there is no non-Python graph engine yet, so this describes
    the one real implementation rather than a speculative abstraction over a
    shape nothing has needed yet -- revisit if/when a second one exists.
    """

    def add_given(
        self: ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]],
        prop_: Prop[Any],
        *,
        # The subject a statement is about, where the source has one -- a
        # puzzle's "alice". A wire request has no subject concept, and a
        # fact with none is drawn by its text alone rather than under a
        # name the producer made up: "Request — carol" was that name.
        subject_name: str | None = None,
        source: SourceSpan | None = None,
    ) -> tuple[
        FactToken[Any], ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]]
    ]: ...

    def add_check(
        self: ReasoningGraphBackend[StateT_co],
        prop_: Prop[Any],
        *,
        subject_name: str | None = None,
        check_label: str,
        source: SourceSpan | None = None,
    ) -> tuple[FactToken[Any], ReasoningGraphBackend[StateT_co]]: ...

    def with_reasoning_backend(
        self: ReasoningGraphBackend[StateT_co],
        backend: ReasoningBackend,
    ) -> ReasoningGraphBackend[StateT_co]: ...

    def check_consistent[SaturationT](
        self: ReasoningGraphBackend[Evidence[Unchecked, SaturationT]],
    ) -> ReasoningGraphBackend[Evidence[Consistent, SaturationT]]: ...

    def saturate(
        self: ReasoningGraphBackend[Evidence[Consistent, Unsaturated]],
    ) -> ReasoningGraphBackend[Evidence[Consistent, Saturated]]: ...

    def explanation_input(
        self: ReasoningGraphBackend[Evidence[Consistent, Saturated]],
        checks: Iterable[FactToken[Any]],
    ) -> ExplanationInput: ...

    def apply_explanation(
        self: ReasoningGraphBackend[StateT_co],
        proposal: ExplanationProposal,
    ) -> ReasoningGraphBackend[StateT_co]: ...

    def classify[SaturationT](
        self: ReasoningGraphBackend[Evidence[Consistent, SaturationT]],
        check: FactToken[Any],
    ) -> CheckVerdict: ...

    def verify_derivations(self) -> list[str]: ...

    def fact(self, fact_id: FactId) -> FactNode: ...

    def explanation_for(self, target: FactToken[Any]) -> list[str]: ...

    def base_exprs(self) -> list[BoolRef]: ...

    @property
    def nodes(self) -> Mapping[FactId, FactNode]: ...

    @property
    def reasoning_backend(self) -> ReasoningBackend: ...

    @property
    def dag(self) -> ProvenanceDag: ...

nodes property

nodes

reasoning_backend property

reasoning_backend

dag property

dag

add_given

add_given(prop_, *, subject_name=None, source=None)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def add_given(
    self: ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]],
    prop_: Prop[Any],
    *,
    # The subject a statement is about, where the source has one -- a
    # puzzle's "alice". A wire request has no subject concept, and a
    # fact with none is drawn by its text alone rather than under a
    # name the producer made up: "Request — carol" was that name.
    subject_name: str | None = None,
    source: SourceSpan | None = None,
) -> tuple[
    FactToken[Any], ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]]
]: ...

add_check

add_check(
    prop_, *, subject_name=None, check_label, source=None
)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def add_check(
    self: ReasoningGraphBackend[StateT_co],
    prop_: Prop[Any],
    *,
    subject_name: str | None = None,
    check_label: str,
    source: SourceSpan | None = None,
) -> tuple[FactToken[Any], ReasoningGraphBackend[StateT_co]]: ...

with_reasoning_backend

with_reasoning_backend(backend)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def with_reasoning_backend(
    self: ReasoningGraphBackend[StateT_co],
    backend: ReasoningBackend,
) -> ReasoningGraphBackend[StateT_co]: ...

check_consistent

check_consistent()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def check_consistent[SaturationT](
    self: ReasoningGraphBackend[Evidence[Unchecked, SaturationT]],
) -> ReasoningGraphBackend[Evidence[Consistent, SaturationT]]: ...

saturate

saturate()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def saturate(
    self: ReasoningGraphBackend[Evidence[Consistent, Unsaturated]],
) -> ReasoningGraphBackend[Evidence[Consistent, Saturated]]: ...

explanation_input

explanation_input(checks)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def explanation_input(
    self: ReasoningGraphBackend[Evidence[Consistent, Saturated]],
    checks: Iterable[FactToken[Any]],
) -> ExplanationInput: ...

apply_explanation

apply_explanation(proposal)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def apply_explanation(
    self: ReasoningGraphBackend[StateT_co],
    proposal: ExplanationProposal,
) -> ReasoningGraphBackend[StateT_co]: ...

classify

classify(check)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def classify[SaturationT](
    self: ReasoningGraphBackend[Evidence[Consistent, SaturationT]],
    check: FactToken[Any],
) -> CheckVerdict: ...

verify_derivations

verify_derivations()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def verify_derivations(self) -> list[str]: ...

fact

fact(fact_id)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def fact(self, fact_id: FactId) -> FactNode: ...

explanation_for

explanation_for(target)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def explanation_for(self, target: FactToken[Any]) -> list[str]: ...

base_exprs

base_exprs()

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def base_exprs(self) -> list[BoolRef]: ...

Saturated

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class Saturated:
    pass

SemanticBackend

Bases: Protocol

One complete decision primitive from which logical queries are derived.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

class SemanticBackend(Protocol):
    """One complete decision primitive from which logical queries are derived."""

    def solve(self, assertions: Sequence[BoolRef]) -> SolveResult: ...

solve

solve(assertions)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/types.py

def solve(self, assertions: Sequence[BoolRef]) -> SolveResult: ...

Unchecked

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class Unchecked:
    pass

Unsaturated

Source code in packages/guardrail-ir/src/guardrail_ir/reasoning_contract.py

class Unsaturated:
    pass

LinearOffset dataclass

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

@dataclass(frozen=True)
class LinearOffset:
    source: ArithRef
    offset: int

source instance-attribute

source

offset instance-attribute

offset

ConstFact dataclass

var == value, with var minted into an opaque key.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

@dataclass(frozen=True)
class ConstFact:
    """`var == value`, with `var` minted into an opaque key."""

    key: str
    value: int
    #: `_propose_simplified_equalities`' self-skip guard: whether
    #: reconstructing `var == value` is already what the fact says. `(key,
    #: value)` alone cannot decide it -- that pair is deliberately
    #: order-agnostic -- so it is precomputed where the term is still in hand.
    already_simplified: bool

key instance-attribute

key

value instance-attribute

value

already_simplified instance-attribute

already_simplified

ExplanationMatch dataclass

A check a structural engine matched to one established fact.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

@dataclass(frozen=True)
class ExplanationMatch:
    """A check a structural engine matched to one established fact."""

    check_id: str
    premise_id: str

check_id instance-attribute

check_id

premise_id instance-attribute

premise_id

LinearFact dataclass

One established fact as a structural engine sees it: x == 5 is a constant, y == x + 2 an offset, and a fact that is neither has no shape but still appears, so the engine can cite it by id.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

@dataclass(frozen=True)
class LinearFact:
    """One established fact as a structural engine sees it: `x == 5` is a
    constant, `y == x + 2` an offset, and a fact that is neither has no
    shape but still appears, so the engine can cite it by id."""

    id: str
    shape: LinearShape | None

id instance-attribute

id

shape instance-attribute

shape

OffsetFact dataclass

target == source + displacement, both sides minted into keys.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

@dataclass(frozen=True)
class OffsetFact:
    """`target == source + displacement`, both sides minted into keys."""

    target_key: str
    source_key: str
    #: `displacement`, not `minutes`: nothing on either side of this boundary
    #: consults a dimension. `linear_offset` parses `source + <integer>` for
    #: any integer, and the Rust core sums it in `i128`.
    displacement: int

target_key instance-attribute

target_key

source_key instance-attribute

source_key

displacement instance-attribute

displacement

VarEqConst dataclass

A proposed var == value, with var still an opaque key.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

@dataclass(frozen=True)
class VarEqConst:
    """A proposed `var == value`, with `var` still an opaque key."""

    key: str
    value: int
    premises: tuple[str, ...]
    rule: str

key instance-attribute

key

value instance-attribute

value

premises instance-attribute

premises

rule instance-attribute

rule

VarEqVar dataclass

A proposed left == right, both sides still opaque keys.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

@dataclass(frozen=True)
class VarEqVar:
    """A proposed `left == right`, both sides still opaque keys."""

    left_key: str
    right_key: str
    premises: tuple[str, ...]
    rule: str

left_key instance-attribute

left_key

right_key instance-attribute

right_key

premises instance-attribute

premises

rule instance-attribute

rule

empty_rustworkx_digraph

empty_rustworkx_digraph()

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def empty_rustworkx_digraph() -> ProvenanceGraph[Any]:
    return _rustworkx().PyDiGraph()

to_wire_explanation_dag

to_wire_explanation_dag(dag, *, origins=None, folded=False)

Project dag into the portable, z3-free explanation-DAG wire form.

A faithful, order-stable read: node/edge order matches dag.nodes() / dag.edges() exactly, so two equivalent DAGs always project to the same wire form regardless of graph backend. Each node also carries its content-derived key (see :func:_stable_keys) — the identity a host may hold across solves, where id is only this projection's edge vocabulary.

folded asks for the runs as well: where one rule is applied end to end (runs_in), a :class:WireReduceNode names that run's members. Nothing else moves -- every node and edge of the run stays -- so the fold is a reading a host may take or leave, and the default is to leave it.

origins maps a graph-local fact id to the authored statements that produced it (see :class:~guardrail_ir.explanation.WireFactOrigin). Only the caller that built the graph from a request knows this — the DAG itself has already forgotten, because by_expr coalesced equal givens on the way in — so it is supplied rather than derived here. Omitted, every fact honestly claims no origin: this projection never invents one, exactly as it never invents a source. Keys are computed before origins are attached, so carrying the relation cannot move an identity a host holds.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def to_wire_explanation_dag(
    dag: ProvenanceDag[ExprT],
    *,
    origins: Mapping[str, Sequence[WireFactOrigin]] | None = None,
    folded: bool = False,
) -> WireExplanationDag:
    """Project ``dag`` into the portable, z3-free explanation-DAG wire form.

    A faithful, order-stable read: node/edge order matches ``dag.nodes()`` /
    ``dag.edges()`` exactly, so two equivalent DAGs always project to the
    same wire form regardless of graph backend. Each node also carries its
    content-derived ``key`` (see :func:`_stable_keys`) — the identity a host
    may hold across solves, where ``id`` is only this projection's edge
    vocabulary.

    ``folded`` asks for the runs as well: where one rule is applied end to end
    (`runs_in`), a :class:`WireReduceNode` names that run's members. Nothing
    else moves -- every node and edge of the run stays -- so the fold is a
    reading a host may take or leave, and the default is to leave it.

    ``origins`` maps a graph-local fact ``id`` to the authored statements that
    produced it (see :class:`~guardrail_ir.explanation.WireFactOrigin`).
    Only the caller that built the graph *from a request* knows this — the DAG
    itself has already forgotten, because ``by_expr`` coalesced equal givens on
    the way in — so it is supplied rather than derived here. Omitted, every
    fact honestly claims no origin: this projection never invents one, exactly
    as it never invents a ``source``. Keys are computed before origins are
    attached, so carrying the relation cannot move an identity a host holds.
    """
    nodes: tuple[
        WireFactNode | WireDerivationNode | WireExplanationNode | WireReduceNode, ...
    ] = tuple(_wire_node(node) for node in dag.nodes())
    edges = tuple(dag.edges())
    if folded:
        # After the run's own nodes, so a reader of the list meets the members
        # before the node that names them, and hashes them before it too. A
        # run's first member is a step by construction (`runs_in`), which is
        # asserted rather than narrowed: it names the invariant relied on.
        rules: dict[GraphNodeId, str] = {
            node.id: node.rule
            for node in dag.nodes()
            if isinstance(node, (DerivationNode, ExplanationNode))
        }
        nodes += tuple(
            WireReduceNode(
                id=f"r{index}",
                key=UNKEYED,
                rule=wire_rule(rules[members[0]])[0],
                steps=(len(members) + 1) // 2,
                members=tuple(str(one) for one in members),
            )
            for index, members in enumerate(runs_in(dag), start=1)
        )
    keys = _stable_keys(
        nodes,
        edges,
        {
            str(node.id): identity_key(node.identity, node.text)
            for node in dag.facts().values()
        },
    )
    claimed = origins or {}
    return WireExplanationDag(
        nodes=tuple(
            node.model_copy(
                update={"key": keys[node.id], "origins": tuple(claimed[node.id])}
            )
            if isinstance(node, WireFactNode) and node.id in claimed
            else node.model_copy(update={"key": keys[node.id]})
            for node in nodes
        ),
        edges=tuple(
            WireProvenanceEdge(source=str(source), target=str(target))
            for source, target in edges
        ),
    )

explanation_lines

explanation_lines(dag, target_id)

Render the explanation walk for target_id over any provenance DAG.

Shared by FactGraph.explanation_for and the Rust engine's wrapper (rust.RustFactGraph), which reconstructs the same ProvenanceDag shape from its engine snapshot -- one formatting loop, not two.

Source code in packages/guardrail-ir/src/guardrail_ir/provenance.py

def explanation_lines(dag: ExplanationWalkable[ExprT], target_id: FactId) -> list[str]:
    """Render the explanation walk for ``target_id`` over any provenance DAG.

    Shared by ``FactGraph.explanation_for`` and the Rust engine's wrapper
    (``rust.RustFactGraph``), which reconstructs the same ``ProvenanceDag``
    shape from its engine snapshot -- one formatting loop, not two.
    """
    if target_id not in dag:
        raise KeyError(f"Unknown fact id: {target_id}")

    lines: list[str] = []

    for node in dag.explanation_nodes(target_id):
        if isinstance(node, (DerivationNode, ExplanationNode)):
            lines.append(f"Using rule: {node.rule}")
            continue

        if node.kind == FactKind.GIVEN:
            lines.append(f"Given: {node.text}")

        elif node.kind == FactKind.DERIVED:
            lines.append(f"Therefore: {node.text}")

        else:
            lines.append(f"Check: {node.text}")

    return lines

slot_dimensions_in

slot_dimensions_in(expr)

Collect {slot name: Dimension} from an authored expression tree.

Public because both graph engines read it, and here -- z3-free -- because one of them must import without z3. It was private while only :class:FactGraph harvested slots; :class:~guardrail_reasoning_rs.RustFactGraph now does the same, and two harvests would be two answers to "which slots did this puzzle map", which is the question every declared invariant then hangs off.

A reference leaf that carries both a path and a dimension record is a slot the solver will name path.dotted (the same convention lowering.z3_of uses); everything else recurses over :func:provenance_children, the closed by-type child set. Dimension-carrying literals have no path and are correctly skipped — they are values, not slots.

A bare SlotRef carries no dimension of its own, so it takes the one implied by the operand it is compared against — the authored-tree twin of service.infer_slot_dimensions, and the same reading lowering._sort_of already uses to sort that slot's variable. Without it a Probability-annotated field would be lowered as a real slot and then have no declared bounds asserted over it.

Source code in packages/guardrail-ir/src/guardrail_ir/dimension_values.py

def slot_dimensions_in(expr: object) -> dict[str, Dimension[Any]]:
    """Collect ``{slot name: Dimension}`` from an authored expression tree.

    Public because both graph engines read it, and here -- z3-free -- because
    one of them must import without z3. It was private while only
    :class:`FactGraph` harvested slots; :class:`~guardrail_reasoning_rs.RustFactGraph`
    now does the same, and two harvests would be two answers to "which slots
    did this puzzle map", which is the question every declared invariant then
    hangs off.

    A reference leaf that carries both a ``path`` and a dimension record is a
    slot the solver will name ``path.dotted`` (the same convention
    ``lowering.z3_of`` uses); everything else recurses over
    :func:`provenance_children`, the closed by-type child set.
    Dimension-carrying *literals* have no path and are correctly skipped —
    they are values, not slots.

    A bare ``SlotRef`` carries no dimension of its own, so it takes the one
    implied by the operand it is compared against — the authored-tree twin of
    ``service.infer_slot_dimensions``, and the same reading
    ``lowering._sort_of`` already uses to sort that slot's variable. Without it
    a ``Probability``-annotated field would be lowered as a real slot and then
    have no declared bounds asserted over it.
    """
    found: dict[str, Dimension[Any]] = {}
    _walk_slots(expr, found)
    return found

core_for_status

core_for_status(result)

The core a verdict rests on: it lives on whichever solve came back UNSAT, and a verdict with no UNSAT solve has none.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def core_for_status(result: CheckResult) -> tuple[BoolRef, ...]:
    """The core a verdict rests on: it lives on whichever solve came back
    UNSAT, and a verdict with no UNSAT solve has none."""
    if result.status is Status.VERIFIED:
        return result.false_core
    if result.status in (Status.FALSIFIED, Status.INCONSISTENT_BASE):
        return result.true_core
    return ()

refutation_core

refutation_core(result, base, check, *, backend=None)

The base terms a refutation is drawn from, as a function of the request.

core_for_status is Z3's core, which suffices and promises nothing else: it can name a term the refutation did not need, and which sufficient subset it names moves with the solver's own state. Measured 2026-10-08 on the relay with handoffs (people-and-events E1c, step 2): one request, solved twice in one process, refuted bram_0920 from eleven premises and then from thirteen, the second a superset of the first -- two minimal refutations exist, and the explanation drawn depended on what the process had solved before.

So a falsified check, and a base inconsistent by itself, are refuted from the terms deletion keeps when it visits every base term in the request's order -- the treatment _entailing_core gave a verified check's premises on 2026-09-19, for the same reason. One solve per base term; any other verdict keeps Z3's core, which nothing draws.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def refutation_core(
    result: CheckResult,
    base: Sequence[BoolRef],
    check: BoolRef,
    *,
    backend: SemanticBackend | None = None,
) -> tuple[BoolRef, ...]:
    """The base terms a refutation is drawn from, as a function of the request.

    `core_for_status` is Z3's core, which suffices and promises nothing else:
    it can name a term the refutation did not need, and which sufficient
    subset it names moves with the solver's own state. Measured 2026-10-08 on
    the relay with handoffs (people-and-events E1c, step 2): one request,
    solved twice in one process, refuted `bram_0920` from eleven premises and
    then from thirteen, the second a superset of the first -- two minimal
    refutations exist, and the explanation drawn depended on what the process
    had solved before.

    So a falsified check, and a base inconsistent by itself, are refuted from
    the terms deletion keeps when it visits every base term in the request's
    order -- the treatment `_entailing_core` gave a verified check's premises
    on 2026-09-19, for the same reason. One solve per base term; any other
    verdict keeps Z3's core, which nothing draws.
    """
    match result.status:
        case Status.FALSIFIED:
            against: tuple[BoolRef, ...] = (check,)
        case Status.INCONSISTENT_BASE:
            against = ()
        case _:
            return core_for_status(result)
    kept = deletion(base, against, _semantic_backend(backend))
    return tuple(base[index] for index in kept)

all_equivalent

all_equivalent(*predicates, backend=None)

Are all predicates provably equivalent to one another?

Entailment is a preorder, so mutual equivalence of a set is "every element lies in one strongly-connected component". Establishing that does not require all N·(N−1) ordered pairs: because the PROVED fragment of entailment is transitive (A⊨B ∧ B⊨C ⟹ A⊨C — a theorem, independent of the solver), a single covering cycle p₀ ⊨ p₁ ⊨ … ⊨ p₀ proves it in N solver calls rather than N². conjunction short-circuits on the first REFUTED link, so a definite mismatch costs even less.

Fewer than two predicates are vacuously equivalent (PROVED), with no solver call. equivalent is the binary case.

Worth keeping in view at the call sites: equivalence is strictly stronger than the entailment :meth:FactGraph.apply_explanation requires of an explanation. Using it to find explanations is a fast path with a readable result, never the rule — a check its premises merely imply is explained just as validly, and looking only for equivalence would decline to say so.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def all_equivalent(
    *predicates: BoolRef,
    backend: SemanticBackend | None = None,
) -> Entailment:
    """Are all ``predicates`` provably equivalent to one another?

    Entailment is a *preorder*, so mutual equivalence of a set is "every element
    lies in one strongly-connected component". Establishing that does **not**
    require all ``N·(N−1)`` ordered pairs: because the ``PROVED`` fragment of
    entailment is *transitive* (``A⊨B ∧ B⊨C ⟹ A⊨C`` — a theorem, independent of
    the solver), a single covering **cycle** ``p₀ ⊨ p₁ ⊨ … ⊨ p₀`` proves it in
    ``N`` solver calls rather than ``N²``. ``conjunction`` short-circuits on the
    first ``REFUTED`` link, so a definite mismatch costs even less.

    Fewer than two predicates are vacuously equivalent (``PROVED``), with no
    solver call. ``equivalent`` is the binary case.

    Worth keeping in view at the call sites: equivalence is *strictly stronger*
    than the entailment :meth:`FactGraph.apply_explanation` requires of an
    explanation. Using it to find explanations is a fast path with a readable
    result, never the rule — a check its premises merely imply is explained
    just as validly, and looking only for equivalence would decline to say so.
    """
    if len(predicates) < 2:
        return Entailment.PROVED

    cycle = zip(predicates, (*predicates[1:], predicates[0]), strict=True)
    return Entailment.conjunction(
        entails([left], right, backend=backend) for left, right in cycle
    )

check_with_core

check_with_core(
    base,
    extra,
    *,
    solver_factory=thread_solver,
    timeout_ms=None,
    rlimit=None
)

Low-level Z3 solve retaining a model, unsat core, or unknown result.

base and extra are asserted together and tracked together; the split is a calling convenience (base is usually a standing context and extra the thing being asked about), not a distinction the solver sees.

On UNSAT the result carries an unsat core: the subset of those tracked assertions z3 found sufficient for the contradiction, mapped back to the expressions that were passed in rather than to its own tracking literals. Two things about it are worth stating, because callers reason from them. It is a subset, not necessarily the smallest one — z3 promises sufficiency, not minimality. And extra is tracked like everything else, so a caller reading the core as "the context that mattered" must drop it: in the usual extra = Not(check) shape it is present in every core and is the negation being refuted, not a premise.

timeout_ms and rlimit bound the solve: a query exceeding either returns SolveStatus.TIMEOUT rather than running unbounded, so a small but solver-expensive request cannot exhaust the service. They bound different things and are set together. timeout measures elapsed time, so it describes the host; rlimit counts z3's internal steps, so the same query costs the same everywhere. Only rlimit makes the budget a property of the request, and only timeout covers the work outside z3.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def check_with_core(
    base: Sequence[BoolRef],
    extra: BoolRef,
    *,
    solver_factory: Callable[[], Any] = thread_solver,
    timeout_ms: int | None = None,
    rlimit: int | None = None,
) -> SolveResult:
    """Low-level Z3 solve retaining a model, unsat core, or unknown result.

    ``base`` and ``extra`` are asserted together and tracked together; the
    split is a calling convenience (``base`` is usually a standing context and
    ``extra`` the thing being asked about), not a distinction the solver sees.

    On ``UNSAT`` the result carries an **unsat core**: the subset of those
    tracked assertions z3 found sufficient for the contradiction, mapped back
    to the expressions that were passed in rather than to its own tracking
    literals. Two things about it are worth stating, because callers reason
    from them. It is a subset, not necessarily the *smallest* one — z3
    promises sufficiency, not minimality. And ``extra`` is tracked like
    everything else, so a caller reading the core as "the context that mattered"
    must drop it: in the usual ``extra = Not(check)`` shape it is present in
    every core and is the negation being refuted, not a premise.

    ``timeout_ms`` and ``rlimit`` bound the solve: a query exceeding either
    returns ``SolveStatus.TIMEOUT`` rather than running unbounded, so a small
    but solver-expensive request cannot exhaust the service. They bound
    different things and are set together. ``timeout`` measures elapsed time,
    so it describes the host; ``rlimit`` counts z3's internal steps, so the same
    query costs the same everywhere. Only ``rlimit`` makes the budget a property
    of the request, and only ``timeout`` covers the work outside z3.
    """
    solver = solver_factory()
    if timeout_ms is not None:
        solver.set("timeout", timeout_ms)
    if rlimit is not None:
        solver.set("rlimit", rlimit)
    # Keyed by the tracking literal's name, read from its declaration: `str`
    # of a literal is z3's pretty-printer, which was half of an explained
    # closed relay's time (E1c step 9, measured 2026-10-09).
    tracked: dict[str, BoolRef] = {}

    for i, expr in enumerate([*base, extra]):
        name = f"a{i}"
        tracked[name] = expr
        solver.assert_and_track(expr, Bool(name, ctx=z3_context()))

    before = _rlimit_count(solver)
    result = solver.check()
    steps_used = _rlimit_count(solver) - before

    if result == sat:
        return SolveResult(SolveStatus.SAT, model=solver.model(), steps_used=steps_used)

    if result == unsat:
        return SolveResult(
            SolveStatus.UNSAT,
            core=tuple(tracked[k.decl().name()] for k in solver.unsat_core()),
            steps_used=steps_used,
        )

    return SolveResult(_unknown_status(solver.reason_unknown()), steps_used=steps_used)

classify

classify(base, check, *, backend=None)

Classify check against base as VERIFIED/FALSIFIED/UNKNOWN/…

Runs the solver twice — once asserting the check, once its negation — and maps the (satisfiable, refutable) pair to a :class:Status. This is the engine puzzle mode and the workflow coverage analysis both build on.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def classify(
    base: Sequence[BoolRef],
    check: BoolRef,
    *,
    backend: SemanticBackend | None = None,
) -> CheckResult:
    """Classify ``check`` against ``base`` as VERIFIED/FALSIFIED/UNKNOWN/…

    Runs the solver twice — once asserting the check, once its negation — and
    maps the ``(satisfiable, refutable)`` pair to a :class:`Status`. This is the
    engine puzzle mode and the workflow coverage analysis both build on.
    """
    semantics = _semantic_backend(backend)
    yes = semantics.solve([*base, check])
    no = semantics.solve([*base, Not(check)])

    status = (
        Status.UNDECIDED
        if {yes.status, no.status} & NO_VERDICT
        else {
            (SolveStatus.SAT, SolveStatus.UNSAT): Status.VERIFIED,
            (SolveStatus.UNSAT, SolveStatus.SAT): Status.FALSIFIED,
            (SolveStatus.SAT, SolveStatus.SAT): Status.UNKNOWN,
            (SolveStatus.UNSAT, SolveStatus.UNSAT): Status.INCONSISTENT_BASE,
        }[(yes.status, no.status)]
    )

    return CheckResult(
        status=status,
        true_model=yes.model,
        false_model=no.model,
        true_core=yes.core,
        false_core=no.core,
    )

classify_check

classify_check(base, check)

Classify a proposition with the default reasoning backend.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def classify_check(
    base: Sequence[BoolRef],
    check: BoolRef,
) -> CheckResult:
    """Classify a proposition with the default reasoning backend."""
    return classify(base, check, backend=default_reasoning_backend().semantics)

entails

entails(premises, conclusion, *, backend=None)

Classify whether premises entail conclusion without losing unknown.

A SAT result for premises ∧ ¬conclusion is a countermodel, so it maps to REFUTED (definitely not entailed), not a mere proof failure.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def entails(
    premises: Sequence[BoolRef],
    conclusion: BoolRef,
    *,
    backend: SemanticBackend | None = None,
) -> Entailment:
    """Classify whether ``premises`` entail ``conclusion`` without losing unknown.

    A ``SAT`` result for ``premises ∧ ¬conclusion`` is a *countermodel*, so it
    maps to ``REFUTED`` (definitely not entailed), not a mere proof failure.
    """
    status = _semantic_backend(backend).solve([*premises, Not(conclusion)]).status
    if status in NO_VERDICT:
        return Entailment.UNDECIDED
    return {
        SolveStatus.UNSAT: Entailment.PROVED,
        SolveStatus.SAT: Entailment.REFUTED,
    }[status]

equivalent

equivalent(a, b, *, backend=None)

Logical equivalence of two predicates.

The binary case of :func:all_equivalent — the 2-cycle a ⊨ b ⊨ a.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def equivalent(
    a: BoolRef,
    b: BoolRef,
    *,
    backend: SemanticBackend | None = None,
) -> Entailment:
    """Logical equivalence of two predicates.

    The binary case of :func:`all_equivalent` — the 2-cycle ``a ⊨ b ⊨ a``.
    """
    return all_equivalent(a, b, backend=backend)

print_core

print_core(core)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def print_core(core: Sequence[BoolRef]) -> None:
    for expr in core:
        print(f"    {expr}")

render_fact

render_fact(expr, slots=None)

Render a z3 fact as a sentence, driven by declared dimension data.

slots maps slot names to their dimension records (see FactGraph.slot_dimensions); a mapped slot's constants render through the dimension's declared DisplayFormat and its offsets carry the declared displacement unit. Unmapped variables render plainly — this function assumes no dimension it was not told about. A fact with neither record shape falls back to z3's own str(expr).

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def render_fact(
    expr: BoolRef, slots: Mapping[str, Dimension[Any]] | None = None
) -> str:
    """Render a z3 fact as a sentence, driven by declared dimension data.

    ``slots`` maps slot names to their dimension records (see
    ``FactGraph.slot_dimensions``); a mapped slot's constants render through
    the dimension's declared ``DisplayFormat`` and its offsets carry the
    declared displacement unit. Unmapped variables render plainly — this
    function assumes no dimension it was not told about. A fact with neither
    record shape falls back to z3's own ``str(expr)``.
    """
    record, lookup = linear_record("", expr)
    realised = realise_record(record, lookup, slots if slots is not None else {})
    return realised if realised is not None else str(expr)

default_reasoning_backend cached

default_reasoning_backend()

Build the shared default backend on first use, not at import.

Two callers, two reasons. FactGraph's field default uses it so the graph dataclass can precede the backend classes in this module. And it is the module's laziness seam: DEFAULT_REASONING_BACKEND is served through __getattr__ below rather than built at import, so a module that only wants the vocabulary never pays for backend construction — the coupling Phase 7b's split exists to remove.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

@functools.cache
def default_reasoning_backend() -> ReasoningBackend:
    """Build the shared default backend on first use, not at import.

    Two callers, two reasons. ``FactGraph``'s field default uses it so the
    graph dataclass can precede the backend classes in this module. And it is
    the module's laziness seam: ``DEFAULT_REASONING_BACKEND`` is served
    through ``__getattr__`` below rather than built at import, so a module
    that only wants the vocabulary never pays for backend construction —
    the coupling Phase 7b's split exists to remove.
    """
    return ReasoningBackend()

first_statements

first_statements(established)

Each established fact -> the first established fact that says the same.

A fact and its restatement -- alice.departure == 540 derived from the given 540 == alice.departure -- say one thing, and an explanation should cite the one the reader met first. Deletion visits candidates in that order, so while both stood the earlier given was dropped and the restatement kept: one simplification step longer than citing the given, for nothing a reader needs. EYE, firing every rule, found the shorter route in each of the three corpus checks where this happened (rdf-shacl-rules-integration.md step 7; joint-premise-explanations.md 6b).

Applied after minimising, as a substitution, not before, as a removal: removing the restatement from the candidates changes what deletion reaches -- it then drops the given too and keeps three premises where two suffice. Swapping a kept restatement for its equivalent keeps the set minimal and the entailment intact.

Sameness is the structural record's -- (slot, value) or (target, source, displacement), orientation-free by construction -- so only what the records can see is folded; a fact with no linear shape is always its own first statement. Both explanation backends use it.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.py

def first_statements(
    established: Sequence[FactNode[BoolRef]],
) -> dict[FactId, FactId]:
    """Each established fact -> the first established fact that says the same.

    A fact and its restatement -- `alice.departure == 540` derived from the
    given `540 == alice.departure` -- say one thing, and an explanation should
    cite the one the reader met first. Deletion visits candidates in that
    order, so while both stood the earlier given was dropped and the
    restatement kept: one simplification step longer than citing the given,
    for nothing a reader needs. EYE, firing every rule, found the shorter
    route in each of the three corpus checks where this happened
    (rdf-shacl-rules-integration.md step 7; joint-premise-explanations.md 6b).

    Applied *after* minimising, as a substitution, not before, as a removal:
    removing the restatement from the candidates changes what deletion
    reaches -- it then drops the given too and keeps three premises where
    two suffice. Swapping a kept restatement for its equivalent keeps the set
    minimal and the entailment intact.

    Sameness is the structural record's -- `(slot, value)` or `(target,
    source, displacement)`, orientation-free by construction -- so only what
    the records can see is folded; a fact with no linear shape is always its
    own first statement. Both explanation backends use it.
    """
    first: dict[ConstFact | OffsetFact, FactId] = {}
    out: dict[FactId, FactId] = {}
    sorts = term_sorts(node.expr for node in established)
    for node in established:
        shape = node_record(node, sorts)[0].shape
        identity = (
            replace(shape, already_simplified=False)
            if isinstance(shape, ConstFact)
            else shape
        )
        out[node.id] = (
            node.id if identity is None else first.setdefault(identity, node.id)
        )
    return out

arith_key

arith_key(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def arith_key(expr: ArithRef) -> str:
    return stable_simplify(expr).sexpr()

as_bool_ref

as_bool_ref(expr)

Narrow a z3 expression to a boolean, refusing anything else.

isinstance rather than cast: BoolRef is a real class now that z3 is a followed import, so this can be checked instead of asserted. It was cast(BoolRef, expr) — a bare "trust me" over object, which is the one shape that cannot be wrong at the point it is written and cannot be right anywhere else either.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def as_bool_ref(expr: object) -> BoolRef:
    """Narrow a z3 expression to a boolean, refusing anything else.

    `isinstance` rather than `cast`: `BoolRef` is a real class now that z3 is a
    followed import, so this can be *checked* instead of asserted. It was
    `cast(BoolRef, expr)` — a bare "trust me" over `object`, which is the one
    shape that cannot be wrong at the point it is written and cannot be right
    anywhere else either.
    """
    if not isinstance(expr, BoolRef):
        raise TypeError(f"expected a z3 boolean, got {expr!r}")
    return expr

as_int

as_int(expr)

The Python value of an integer numeral, or of a whole Real one, or None.

isinstance(expr, IntNumRef) in place of is_int_value plus a cast: the two agree exactly (verified across numerals, symbols and folded expressions), and one of them narrows. is_int_value answers bool, so it left the cast to assert what it had just established.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def as_int(expr: object) -> int | None:
    """The Python value of an integer numeral, or of a whole Real one, or ``None``.

    `isinstance(expr, IntNumRef)` in place of `is_int_value` plus a cast: the two
    agree exactly (verified across numerals, symbols and folded expressions), and
    one of them narrows. `is_int_value` answers `bool`, so it left the cast to
    assert what it had just established.
    """
    if isinstance(expr, IntNumRef):
        return expr.as_long()
    # A Real numeral that is a whole number is that integer: a dense Instant's
    # 570 (dense-rational-event-time.md). One with a fraction is not, and the
    # structural engines derive nothing from it -- z3 still classifies it.
    if isinstance(expr, RatNumRef) and expr.denominator_as_long() == 1:
        return expr.numerator_as_long()
    return None

equality_sides

equality_sides(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def equality_sides(expr: BoolRef) -> tuple[ArithRef, ArithRef] | None:
    expr = as_bool_ref(stable_simplify(expr))

    if not is_eq(expr):
        return None

    lhs, rhs = expr.children()
    return cast(ArithRef, stable_simplify(lhs)), cast(ArithRef, stable_simplify(rhs))

expr_key

expr_key(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def expr_key(expr: BoolRef) -> str:
    return stable_simplify(expr).sexpr()

is_eq

is_eq(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def is_eq(expr: BoolRef) -> bool:
    return is_app_of(expr, Z3_OP_EQ)

linear_offset

linear_offset(expr)

Parse simplify(expr) as source + offset for a single symbolic source.

Only addition needs handling: Z3's simplify normalises subtraction into addition of negated terms. Anything else (pure constants, multiple symbolic terms) returns None, and callers simply derive nothing from it.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def linear_offset(expr: ArithRef) -> LinearOffset | None:
    """Parse `simplify(expr)` as `source + offset` for a single symbolic source.

    Only addition needs handling: Z3's `simplify` normalises subtraction into
    addition of negated terms. Anything else (pure constants, multiple
    symbolic terms) returns None, and callers simply derive nothing from it.
    """
    expr = cast(ArithRef, stable_simplify(expr))

    if is_numeral(expr):
        return None

    if expr.num_args() == 0:
        return LinearOffset(expr, 0)

    if expr.decl().kind() == Z3_OP_ADD:
        symbolic: list[ArithRef] = []
        offset = 0

        for child in expr.children():
            arg = cast(ArithRef, stable_simplify(child))
            value = as_int(arg)

            if value is None:
                symbolic.append(arg)
            else:
                offset += value

        if len(symbolic) == 1:
            return LinearOffset(symbolic[0], offset)

    return None

parse_constant_equality

parse_constant_equality(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def parse_constant_equality(expr: BoolRef) -> tuple[ArithRef, int] | None:
    sides = equality_sides(expr)

    if sides is None:
        return None

    lhs, rhs = sides

    rhs_value = as_int(rhs)
    if rhs_value is not None:
        return lhs, rhs_value

    lhs_value = as_int(lhs)
    if lhs_value is not None:
        return rhs, lhs_value

    return None

parse_offset_equality

parse_offset_equality(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def parse_offset_equality(expr: BoolRef) -> tuple[ArithRef, ArithRef, int] | None:
    sides = equality_sides(expr)

    if sides is None:
        return None

    lhs, rhs = sides

    parsed_rhs = linear_offset(rhs)
    if parsed_rhs is not None and not is_numeral(lhs):
        return lhs, parsed_rhs.source, parsed_rhs.offset

    parsed_lhs = linear_offset(lhs)
    if parsed_lhs is not None and not is_numeral(rhs):
        return rhs, parsed_lhs.source, parsed_lhs.offset

    return None

render_arith

render_arith(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/terms.py

def render_arith(expr: ArithRef) -> str:
    return str(expr)

explanation_proposals_from_matches

explanation_proposals_from_matches(matches)

Reconstruct ExplanationProposals from a structural engine's match output (check_id/premise_id pairs). The rule text is deliberately distinct from FactGraphExplanationBackend's "check is equivalent to a known fact": the structural engine matched normalised shapes, not full semantic equivalence, and the provenance record should say so.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

def explanation_proposals_from_matches(
    matches: Iterable[ExplanationMatch],
) -> Iterator[ExplanationProposal]:
    """Reconstruct ``ExplanationProposal``s from a structural engine's match
    output (``check_id``/``premise_id`` pairs). The rule text is deliberately
    distinct from ``FactGraphExplanationBackend``'s "check is equivalent to a
    known fact": the structural engine matched normalised shapes, not full
    semantic equivalence, and the provenance record should say so.
    """
    for match in matches:
        yield ExplanationProposal(
            check_id=FactId(match.check_id),
            premises=(FactId(match.premise_id),),
            rule=ExplanationRule.NORMALISED_MATCH,
        )

linear_records

linear_records(nodes)

Flatten facts into opaque-keyed records a structural engine can compare, plus a lookup resolving each key to the term and operand it stands for.

Shared by RustDerivationBackend/RustExplanationBackend: the shape is identical for DerivationInput.established and ExplanationInput.established/.checks -- a check is just another FactNode. A structural engine only ever compares keys for equality, so crossing the FFI as opaque strings is sufficient; since phase 1 of reasoning-wire-ir the strings are canonical atoms, not z3 spellings.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

def linear_records(
    nodes: Sequence[FactNode],
) -> tuple[list[LinearFact], dict[str, Atom]]:
    """Flatten facts into opaque-keyed records a structural engine can compare,
    plus a lookup resolving each key to the term and operand it stands for.

    Shared by ``RustDerivationBackend``/``RustExplanationBackend``: the shape
    is identical for ``DerivationInput.established`` and
    ``ExplanationInput.established``/``.checks`` -- a check is just another
    ``FactNode``. A structural engine only ever compares keys for equality, so
    crossing the FFI as opaque strings is sufficient; since phase 1 of
    reasoning-wire-ir the strings are canonical atoms, not z3 spellings.
    """
    # What a wire slot lowers to is a question of semantics, which this
    # engine answers with z3: read off the facts' own terms, so a slot that
    # only ever meets another slot still has one. The keys -- the identity --
    # come from the operands.
    sorts = term_sorts(node.expr for node in nodes)
    records: list[LinearFact] = []
    lookup: dict[str, Atom] = {}
    for node in nodes:
        record, atoms = node_record(node, sorts)
        records.append(record)
        lookup.update(atoms)
    return records, lookup

proposals_from_records

proposals_from_records(proposals, lookup)

Reconstruct DerivationProposals from a structural engine's flat, opaque-keyed output, resolving each key back to the term and operand it came from. The engine itself never constructs or returns a z3 expression.

The conclusion's operand is said in its atoms', so a derived fact is identified as its premises are: from the wire, by the canonical form.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/records.py

def proposals_from_records(
    proposals: Iterable[RecordProposal],
    lookup: Mapping[str, Atom],
) -> Iterator[DerivationProposal]:
    """Reconstruct ``DerivationProposal``s from a structural engine's flat,
    opaque-keyed output, resolving each key back to the term and operand it
    came from. The engine itself never constructs or returns a z3 expression.

    The conclusion's operand is said in its atoms', so a derived fact is
    identified as its premises are: from the wire, by the canonical form.
    """
    for proposal in proposals:
        match proposal:
            case VarEqConst(key=key, value=value):
                atom = lookup[key]
                conclusion = cast(BoolRef, atom.term == value)
                operand = (
                    None
                    if atom.operand is None
                    else WireBinary(
                        op="eq", left=atom.operand, right=_literal(atom.operand, value)
                    )
                )
            case VarEqVar(left_key=left_key, right_key=right_key):
                left, right = lookup[left_key], lookup[right_key]
                conclusion = cast(BoolRef, left.term == right.term)
                operand = (
                    None
                    if left.operand is None or right.operand is None
                    else WireBinary(op="eq", left=left.operand, right=right.operand)
                )
            case _:  # pragma: no cover - exhaustiveness guard
                assert_never(proposal)
        yield DerivationProposal(
            # No text: the graph renders a conclusion when it inserts it, with
            # its own dimension map, so the adapter needs no renderer.
            conclusion=Prop(expr=conclusion),
            premises=tuple(FactId(premise) for premise in proposal.premises),
            rule=proposal.rule,
            identity=_said(operand),
        )

dag_to_d3_html

dag_to_d3_html(
    dag, *, element_id="reasoning-d3", library="cytoscape"
)

Render a provenance DAG as a self-contained HTML snippet.

The other half of dag_to_d3_payload. That one landed without this, which left the promise it was added for only half kept: a client holding a service response could compute the payload but not the page, and the one consumer that wants a page -- a notebook cell -- is exactly the client that has no FactGraph.

Parameters:

Name	Type	Description	Default
dag	ProvenanceDag[ExprT]	The provenance DAG to render.	required
element_id	str	The HTML id attribute for the container div element.	'reasoning-d3'
library	D3Library	The chosen rendering library.	'cytoscape'

Returns:

Type	Description
str	Self-contained HTML snippet string.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/d3.py

def dag_to_d3_html[ExprT](
    dag: ProvenanceDag[ExprT],
    *,
    element_id: str = "reasoning-d3",
    library: D3Library = "cytoscape",
) -> str:
    """Render a provenance DAG as a self-contained HTML snippet.

    The other half of `dag_to_d3_payload`. That one landed without this, which
    left the promise it was added for only half kept: a client holding a
    service response could compute the payload but not the page, and the one
    consumer that wants a page -- a notebook cell -- is exactly the client that
    has no `FactGraph`.

    Args:
        dag: The provenance DAG to render.
        element_id: The HTML id attribute for the container div element.
        library: The chosen rendering library.

    Returns:
        Self-contained HTML snippet string.
    """
    payload = dag_to_d3_payload(dag, library=library)

    if library == "cytoscape":
        return _cytoscape_html(payload, element_id)

    return _d3_html(payload, element_id)

dag_to_d3_payload

dag_to_d3_payload(dag, *, library='cytoscape')

Build the JSON-able payload (meta/nodes/links) for a provenance DAG.

The DAG is all the renderer ever reads — rows come from the node kinds and links from the edges — so this, not graph_to_d3_payload, is the primitive. It is also what makes from_wire_explanation_dag's promise ("the renderers can walk it") literally true: a client holding nothing but a service response's WireExplanationDag can rebuild the DAG and render it, with no engine, no z3 and no FactGraph.

Parameters:

Name	Type	Description	Default
dag	ProvenanceDag[ExprT]	The provenance DAG to build the payload for.	required
library	D3Library	The chosen rendering library.	'cytoscape'

Returns:

Type	Description
dict[str, Any]	A dictionary containing the keys "meta", "nodes", and "links" with graph representation data.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/d3.py

def dag_to_d3_payload[ExprT](
    dag: ProvenanceDag[ExprT],
    *,
    library: D3Library = "cytoscape",
) -> dict[str, Any]:
    """Build the JSON-able payload (`meta`/`nodes`/`links`) for a provenance DAG.

    The DAG is all the renderer ever reads — rows come from the node kinds and
    links from the edges — so this, not
    [graph_to_d3_payload][guardrail_solver.reasoning.graph_to_d3_payload], is
    the primitive. It is also what makes ``from_wire_explanation_dag``'s
    promise ("the renderers can walk it") literally true: a client holding
    nothing but a service response's `WireExplanationDag` can rebuild the DAG
    and render it, with no engine, no z3 and no `FactGraph`.

    Args:
        dag: The provenance DAG to build the payload for.
        library: The chosen rendering library.

    Returns:
        A dictionary containing the keys "meta", "nodes", and "links" with graph representation data.
    """
    all_nodes = tuple(dag.nodes())
    fact_and_derivation_nodes = [
        node for node in all_nodes if isinstance(node, (FactNode, DerivationNode))
    ]

    if library == "cytoscape":
        return _cytoscape_payload(dag, all_nodes, fact_and_derivation_nodes)

    return _d3_payload(dag, all_nodes, fact_and_derivation_nodes)

graph_to_d3_html

graph_to_d3_html(
    graph, *, element_id="reasoning-d3", library="cytoscape"
)

Render a FactGraph explanation DAG as a self-contained HTML snippet.

Returns a <div> plus inline <script> that loads the chosen library from a CDN and draws the graph client-side. See D3Library and the module docstring for the trade-off between the two styles.

Parameters:

Name	Type	Description	Default
graph	ReasoningGraphBackend[StateT]	The graph to render.	required
element_id	str	The HTML id attribute for the container div element.	'reasoning-d3'
library	D3Library	The chosen rendering library.	'cytoscape'

Returns:

Type	Description
str	Self-contained HTML snippet string.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/d3.py

def graph_to_d3_html[StateT](
    graph: ReasoningGraphBackend[StateT],
    *,
    element_id: str = "reasoning-d3",
    library: D3Library = "cytoscape",
) -> str:
    """Render a [FactGraph][guardrail_solver.reasoning.FactGraph] explanation DAG as a self-contained HTML snippet.

    Returns a `<div>` plus inline `<script>` that loads the chosen
    `library` from a CDN and draws the graph client-side. See
    `D3Library` and the module docstring
    for the trade-off between the two styles.

    Args:
        graph: The graph to render.
        element_id: The HTML id attribute for the container div element.
        library: The chosen rendering library.

    Returns:
        Self-contained HTML snippet string.
    """
    return dag_to_d3_html(graph.dag, element_id=element_id, library=library)

graph_to_d3_payload

graph_to_d3_payload(graph, *, library='cytoscape')

Build the JSON-able payload (meta/nodes/links) for a graph.

library picks the payload shape to build (see D3Library and the module docstring): "cytoscape" (the default) omits per-node positions (Cytoscape computes them client-side); "d3" includes a fixed x/y/width per node computed here in Python.

The name is kept as d3_payload for backwards compatibility with existing callers.

Parameters:

Name	Type	Description	Default
graph	ReasoningGraphBackend[StateT]	The FactGraph to build the payload for.	required
library	D3Library	The chosen rendering library.	'cytoscape'

Returns:

Type	Description
dict[str, Any]	A dictionary containing the keys "meta", "nodes", and "links" with graph representation data.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/d3.py

def graph_to_d3_payload[StateT](
    graph: ReasoningGraphBackend[StateT],
    *,
    library: D3Library = "cytoscape",
) -> dict[str, Any]:
    """Build the JSON-able payload (`meta`/`nodes`/`links`) for a graph.

    `library` picks the payload shape to build (see `D3Library`
    and the module docstring): `"cytoscape"` (the default) omits per-node
    positions (Cytoscape computes them client-side); `"d3"` includes a
    fixed `x`/`y`/`width` per node computed here in Python.

    The name is kept as `d3_payload` for backwards compatibility with
    existing callers.

    Args:
        graph: The [FactGraph][guardrail_solver.reasoning.FactGraph] to build the payload for.
        library: The chosen rendering library.

    Returns:
        A dictionary containing the keys "meta", "nodes", and "links" with graph representation data.
    """
    return dag_to_d3_payload(graph.dag, library=library)

algebra_table

algebra_table(rules)

An | Operation | Result | table of a dimension's closure rules.

Signature-sorted for a deterministic build. The rules are whatever the dimension's declared structure derived, so the table cannot list an operator the algebra does not actually admit.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def algebra_table(rules: Iterable[_AlgebraRuleLike]) -> str:
    """An ``| Operation | Result |`` table of a dimension's closure rules.

    Signature-sorted for a deterministic build. The rules are whatever the
    dimension's declared structure derived, so the table cannot list an operator
    the algebra does not actually admit.
    """
    lines = ["| Operation | Result |", "|---|---|"]
    for rule in sorted(rules, key=lambda rule: (rule.op, rule.left, rule.right)):
        lines.append(f"| `{rule.left} {rule.op} {rule.right}` | `{rule.result}` |")
    return "\n".join(lines)

checks_verdict_table

checks_verdict_table(solved)

A | Check | Proposition | Verdict | table for every check in a puzzle.

Classifies each check against the solved graph's own base facts, so the verdicts are produced here rather than restated: the caller supplies only which puzzle to solve. Checks are label-sorted for a deterministic build.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def checks_verdict_table(solved: SolvedPuzzle[Any]) -> str:
    """A ``| Check | Proposition | Verdict |`` table for every check in a puzzle.

    Classifies each check against the solved graph's own base facts, so the
    verdicts are produced here rather than restated: the caller supplies only
    which puzzle to solve. Checks are label-sorted for a deterministic build.
    """
    lines = ["| Check | Proposition | Verdict |", "|---|---|---|"]
    for label in sorted(solved.check_tokens):
        token = solved.check_tokens[label]
        proposition = (solved.graph.nodes[token.id].text or "").rstrip(".")
        verdict = verdict_badge(solved.graph.classify(token).status)
        lines.append(f"| {label} | {proposition} | {verdict} |")
    return "\n".join(lines)

classification_table

classification_table(rows)

A | Proposition | Verdict | Model | table for classified candidates.

Each row is (proposition source, response). The model column is the assignment the classifier returned -- a satisfying example, deliberately not labelled "counterexample" the way the invariant table's column is, since a classification's model witnesses whichever of the two questions was answered first. Rendered by the same :func:render_assignments every other result table uses, so an absent model reads as none rather than as a blank cell.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def classification_table(rows: Iterable[tuple[str, _ClassifiedLike]]) -> str:
    """A ``| Proposition | Verdict | Model |`` table for classified candidates.

    Each row is ``(proposition source, response)``. The model column is the
    assignment the classifier returned -- a *satisfying* example, deliberately
    not labelled "counterexample" the way the invariant table's column is, since
    a classification's model witnesses whichever of the two questions was
    answered first. Rendered by the same :func:`render_assignments` every other
    result table uses, so an absent model reads as ``none`` rather than as a
    blank cell.
    """
    lines = ["| Proposition | Verdict | Model |", "|---|---|---|"]
    for source, response in rows:
        lines.append(
            f"| `{source}` | {verdict_badge(response.status)} "
            f"| {render_assignments(response.assignments)} |"
        )
    return "\n".join(lines)

coverage_block

coverage_block(response)

A coverage response as a fenced text block.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def coverage_block(response: _CoverageLike) -> str:
    """A coverage response as a fenced text block."""
    return _fenced(
        (
            f"total  = {response.total}",
            f"status = {verdict_status_name(response.status)}",
            f"gap    = {render_assignments(response.gap)}",
        )
    )

decision_block

decision_block(response)

A decision response as a fenced text block.

Overlaps read as prose rather than as raw tuples: an index pair alone does not say what went wrong, and the witness is the part a reader acts on.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def decision_block(response: _DecisionLike) -> str:
    """A decision response as a fenced text block.

    Overlaps read as prose rather than as raw tuples: an index pair alone does
    not say what went wrong, and the witness is the part a reader acts on.
    """
    overlaps = (
        "; ".join(
            f"guards {overlap.first} and {overlap.second} co-fire, "
            f"witness {render_assignments(overlap.witness)}"
            for overlap in response.overlaps
        )
        or _ABSENT
    )
    unreachable = (
        ", ".join(str(index) for index in response.unreachable)
        if response.unreachable
        else _ABSENT
    )
    return _fenced((f"overlaps    = {overlaps}", f"unreachable = {unreachable}"))

invariant_table

invariant_table(rows)

A | Precondition | Verdict | Counterexample | table.

Each row is (precondition source, response). A precondition of "(none)" renders as emphasised prose rather than code, since an absent precondition is not a snippet a reader could copy.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def invariant_table(rows: Iterable[tuple[str, _InvariantLike]]) -> str:
    """A ``| Precondition | Verdict | Counterexample |`` table.

    Each row is ``(precondition source, response)``. A precondition of
    ``"(none)"`` renders as emphasised prose rather than code, since an absent
    precondition is not a snippet a reader could copy.
    """
    lines = ["| Precondition | Verdict | Counterexample |", "|---|---|---|"]
    for source, response in rows:
        precondition = "*(none)*" if source == "(none)" else f"`{source}`"
        lines.append(
            f"| {precondition} | {verdict_badge(response.status)} "
            f"| {render_assignments(response.counterexample)} |"
        )
    return "\n".join(lines)

normalized_block

normalized_block(ir)

Normalized IR as a fenced text block: what each slot resolved to.

The counts and mappings come off the IR itself, so this reports what the normalizer inferred rather than what a page expected it to infer.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def normalized_block(ir: _NormalizedLike) -> str:
    """Normalized IR as a fenced text block: what each slot resolved to.

    The counts and mappings come off the IR itself, so this reports what the
    normalizer inferred rather than what a page expected it to infer.
    """
    return _fenced(
        (
            f"slot sorts      = {_mapping(ir.slot_sorts)}",
            f"slot dimensions = {_mapping(ir.slot_dimensions)}",
            f"invariants      = {len(ir.invariant_constraints)} realised",
        )
    )

rejection_table

rejection_table(rows)

A | Expression | Rejected with | table of real, raised exceptions.

Each row is (expression source, the exception it raised). Only the message's first line is shown, truncated: some rejections quote the whole operand record, and a table cell carrying a repr of an entire dimension declaration communicates less than its first clause does. Truncation is presentation -- the type and the leading text are the exception's own, so a page cannot claim a rejection the library did not make.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def rejection_table(rows: Iterable[tuple[str, BaseException]]) -> str:
    """A ``| Expression | Rejected with |`` table of real, raised exceptions.

    Each row is ``(expression source, the exception it raised)``. Only the
    message's first line is shown, truncated: some rejections quote the whole
    operand record, and a table cell carrying a repr of an entire dimension
    declaration communicates less than its first clause does. Truncation is
    presentation -- the type and the leading text are the exception's own, so a
    page cannot claim a rejection the library did not make.
    """
    lines = ["| Expression | Rejected with |", "|---|---|"]
    for source, error in rows:
        message = _first_line(str(error), _MESSAGE_LIMIT)
        lines.append(f"| `{source}` | `{type(error).__name__}` — {message} |")
    return "\n".join(lines)

render_assignment

render_assignment(value)

One witness/counterexample value, rendered for a documentation reader.

Rationals become exact fractions (1/5, or just 3 when the denominator is 1) rather than decimals, strings are quoted so an empty or space-carrying value is still visible, and everything else falls back to str.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def render_assignment(value: object) -> str:
    """One witness/counterexample value, rendered for a documentation reader.

    Rationals become exact fractions (``1/5``, or just ``3`` when the
    denominator is 1) rather than decimals, strings are quoted so an empty or
    space-carrying value is still visible, and everything else falls back to
    ``str``.
    """
    if isinstance(value, bool):
        # Checked before the rational/int branches: bool is an int subclass, and
        # `True` should read as `True`, not `1`.
        return str(value)
    if _is_rational(value):
        return str(value.num) if value.den == 1 else f"{value.num}/{value.den}"
    if isinstance(value, str):
        return f'"{value}"'
    return str(value)

render_assignments

render_assignments(values)

A whole witness/counterexample mapping, key-sorted for determinism.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def render_assignments(values: Mapping[str, object] | None) -> str:
    """A whole witness/counterexample mapping, key-sorted for determinism."""
    if not values:
        return _ABSENT
    inner = ", ".join(
        f"{key}: {render_assignment(value)}" for key, value in sorted(values.items())
    )
    return "{ " + inner + " }"

verdict_badge

verdict_badge(status)

A verdict as a badge-classed inline code span (attr_list syntax).

Raises KeyError for an unrecognised verdict rather than emitting an unstyled word: a silently unstyled badge on a published page is exactly the kind of quiet drift routing docs through this module is meant to prevent.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def verdict_badge(status: _Verdict | str) -> str:
    """A verdict as a badge-classed inline code span (``attr_list`` syntax).

    Raises ``KeyError`` for an unrecognised verdict rather than emitting an
    unstyled word: a silently unstyled badge on a published page is exactly the
    kind of quiet drift routing docs through this module is meant to prevent.
    """
    name = verdict_status_name(status)
    try:
        badge_class = _VERDICT_CLASS[name]
    except KeyError:
        raise KeyError(
            f"no verdict badge class for {name!r}; add it to _VERDICT_CLASS and "
            "to docs/stylesheets/verdicts.css together"
        ) from None
    return f"`{name}`{{.verdict .{badge_class}}}"

verdict_status_name

verdict_status_name(status)

The wire name of a verdict, accepting either an enum or a bare string.

Reads .value before falling back, which is load-bearing rather than defensive: Status is a str subclass, so an isinstance(status, str) check passes for a real verdict and would hand back the member itself -- whose str() is "Status.VERIFIED", not "VERIFIED". Verified directly against Status rather than assumed.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/markdown.py

def verdict_status_name(status: _Verdict | str) -> str:
    """The wire name of a verdict, accepting either an enum or a bare string.

    Reads ``.value`` *before* falling back, which is load-bearing rather than
    defensive: ``Status`` is a ``str`` subclass, so an ``isinstance(status, str)``
    check passes for a real verdict and would hand back the member itself --
    whose ``str()`` is ``"Status.VERIFIED"``, not ``"VERIFIED"``. Verified
    directly against ``Status`` rather than assumed.
    """
    if isinstance(status, _Verdict):
        value = status.value
        return value if isinstance(value, str) else str(value)
    return status

graph_to_mermaid

graph_to_mermaid(
    graph,
    *,
    focus=None,
    grouping="flat",
    include_config=True,
    include_clicks=True
)

Render a FactGraph using semantic rows.

Rows are: - Givens - Reasoning - Derived facts - Checks

Nodes are arranged left-to-right within their semantic row where the layout engine allows it. grouping picks how rows and the focus/peripheral split are conveyed visually — see MermaidGrouping and the module docstring for the trade-off between the two styles.

When focus is supplied, the focused fact and all provenance ancestors are the vivid, prominent group; unrelated graph material is muted and placed beneath it.

Derivations remain explicit

premise fact -> reasoning step -> conclusion fact

Explanation steps are collapsed

known fact -. rule .-> check

Parameters:

Name	Type	Description	Default
graph	ReasoningGraphBackend[StateT]	The FactGraph to render.	required
focus	MermaidFocus	The node/fact to focus on.	None
grouping	MermaidGrouping	The grouping/layout style.	'flat'
include_config	bool	Whether to include default Mermaid config markers.	True
include_clicks	bool	Whether to include hyperlink actions for clickable nodes.	True

Returns:

Type	Description
str	The generated Mermaid graph string.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def graph_to_mermaid[StateT](
    graph: ReasoningGraphBackend[StateT],
    *,
    focus: MermaidFocus = None,
    grouping: MermaidGrouping = "flat",
    include_config: bool = True,
    include_clicks: bool = True,
) -> str:
    """Render a [FactGraph][guardrail_solver.reasoning.FactGraph] using semantic rows.

    Rows are:
    - Givens
    - Reasoning
    - Derived facts
    - Checks

    Nodes are arranged left-to-right within their semantic row where the
    layout engine allows it. `grouping` picks how rows and the
    focus/peripheral split are conveyed visually — see `MermaidGrouping`
    and the module docstring for the trade-off between the two styles.

    When `focus` is supplied, the focused fact and all provenance ancestors
    are the vivid, prominent group; unrelated graph material is muted and
    placed beneath it.

    Derivations remain explicit:
        premise fact -> reasoning step -> conclusion fact

    Explanation steps are collapsed:
        known fact -. rule .-> check

    Args:
        graph: The [FactGraph][guardrail_solver.reasoning.FactGraph] to render.
        focus: The node/fact to focus on.
        grouping: The grouping/layout style.
        include_config: Whether to include default Mermaid config markers.
        include_clicks: Whether to include hyperlink actions for clickable nodes.

    Returns:
        The generated Mermaid graph string.
    """
    target_id = _focus_fact_id(focus)

    if target_id is not None and target_id not in graph.dag:
        raise KeyError(f"Mermaid focus does not belong to this graph: {target_id}")

    all_nodes = tuple(graph.dag.nodes())
    all_node_ids = frozenset(node.id for node in all_nodes)

    relevant_ids = (
        graph.dag.explanation_node_ids(target_id)
        if target_id is not None
        else all_node_ids
    )
    peripheral_ids = all_node_ids - relevant_ids

    relevant_nodes = tuple(node for node in all_nodes if node.id in relevant_ids)
    peripheral_nodes = tuple(node for node in all_nodes if node.id in peripheral_ids)

    relevant_rows = partition_rows(relevant_nodes)
    peripheral_rows = partition_rows(peripheral_nodes)

    relevant_facts = tuple(
        node for node in relevant_nodes if isinstance(node, FactNode)
    )
    peripheral_facts = tuple(
        node for node in peripheral_nodes if isinstance(node, FactNode)
    )

    relevant_steps = tuple(
        node
        for node in relevant_nodes
        if isinstance(node, (DerivationNode, ExplanationNode))
    )
    peripheral_steps = tuple(
        node
        for node in peripheral_nodes
        if isinstance(node, (DerivationNode, ExplanationNode))
    )

    predecessors: dict[GraphNodeId, list[GraphNodeId]] = {}
    successors: dict[GraphNodeId, list[GraphNodeId]] = {}

    for source_id, target_node_id in graph.dag.edges():
        predecessors.setdefault(target_node_id, []).append(source_id)
        successors.setdefault(source_id, []).append(target_node_id)

    lines: list[str] = []

    if include_config:
        lines.append(
            _MERMAID_INIT_DIRECTIVE_FLAT
            if grouping == "flat"
            else _MERMAID_INIT_DIRECTIVE_SUBGRAPH
        )

    lines.append("flowchart TB")
    lines.append("")

    focus_title = "Explanation"

    if target_id is not None:
        target = graph.fact(target_id)

        if target.kind is FactKind.CHECK and target.check_label is not None:
            focus_title = f"Explanation for Check {target.check_label}"

    focus_anchors: tuple[tuple[str, GraphNodeId], ...] = ()
    peripheral_anchors: tuple[tuple[str, GraphNodeId], ...] = ()
    focus_row_ids: tuple[str, ...] = ()
    peripheral_row_ids: tuple[str, ...] = ()

    if grouping == "flat":
        lines.append(mermaid_label_declaration("explanation_label", focus_title))
        focus_anchors = _render_semantic_rows_flat(
            lines,
            rows=relevant_rows,
            include_subject=True,
            muted=False,
            indent="    ",
        )

        if peripheral_ids:
            lines.append("")
            lines.append(
                mermaid_label_declaration("peripheral_label", "Other facts and checks")
            )
            peripheral_anchors = _render_semantic_rows_flat(
                lines,
                rows=peripheral_rows,
                include_subject=True,
                muted=True,
                indent="    ",
            )
    else:
        lines.append(
            f'    subgraph explanation_region["{mermaid_escape(focus_title)}"]'
        )
        focus_row_ids = _render_semantic_rows_subgraph(
            lines,
            rows=relevant_rows,
            include_subject=True,
            muted=False,
            indent="        ",
        )
        lines.append("    end")

        if peripheral_ids:
            lines.append("")
            lines.append('    subgraph peripheral_region["Other facts and checks"]')
            peripheral_row_ids = _render_semantic_rows_subgraph(
                lines,
                rows=peripheral_rows,
                include_subject=True,
                muted=True,
                indent="        ",
            )
            lines.append("    end")

    lines.append("")

    edge_indices: dict[Literal["focus", "muted", "invisible"], list[int]] = {
        "focus": [],
        "muted": [],
        "invisible": [],
    }
    link_index = 0

    def append_edge(
        declaration: str,
        *,
        edge_class: Literal["focus", "muted", "invisible"],
    ) -> None:
        nonlocal link_index

        lines.append(f"    {declaration}")
        edge_indices[edge_class].append(link_index)
        link_index += 1

    # Explicit derivation edges:
    #
    #     premise -> reasoning -> conclusion
    for node in (*relevant_steps, *peripheral_steps):
        if not isinstance(node, DerivationNode):
            continue

        step_id = mermaid_derivation_id(node.id)
        focused_step = node.id in relevant_ids

        for premise_id in predecessors.get(node.id, ()):
            append_edge(
                f'{mermaid_graph_node_id(premise_id)} -->|"uses"| {step_id}',
                edge_class=(
                    "focus" if focused_step and premise_id in relevant_ids else "muted"
                ),
            )

        for conclusion_id in successors.get(node.id, ()):
            append_edge(
                f'{step_id} -->|"derives"| {mermaid_graph_node_id(conclusion_id)}',
                edge_class=(
                    "focus"
                    if focused_step and conclusion_id in relevant_ids
                    else "muted"
                ),
            )

    # Collapsed explanation edges:
    #
    #     established fact -. rule .-> check
    for node in (*relevant_steps, *peripheral_steps):
        if not isinstance(node, ExplanationNode):
            continue

        edge_label = mermaid_escape(node.rule)

        for premise_id in predecessors.get(node.id, ()):
            for conclusion_id in successors.get(node.id, ()):
                append_edge(
                    f"{mermaid_graph_node_id(premise_id)} "
                    f'-. "{edge_label}" .-> '
                    f"{mermaid_graph_node_id(conclusion_id)}",
                    edge_class=(
                        "focus"
                        if (
                            premise_id in relevant_ids and conclusion_id in relevant_ids
                        )
                        else "muted"
                    ),
                )

    # Keep nodes within each semantic row arranged left-to-right.
    #
    # These invisible edges constrain layout only; they do not represent
    # provenance.
    for row in (
        *_row_node_ids(relevant_rows),
        *_row_node_ids(peripheral_rows),
    ):
        for earlier, later in zip(
            row,
            row[1:],
            strict=False,
        ):
            append_edge(
                f"{mermaid_graph_node_id(earlier)} ~~~ {mermaid_graph_node_id(later)}",
                edge_class="invisible",
            )

    if grouping == "flat":
        # Anchor each row's floating label beside its first node.
        for label_id, first_node_id in (*focus_anchors, *peripheral_anchors):
            append_edge(
                f"{label_id} ~~~ {mermaid_graph_node_id(first_node_id)}",
                edge_class="invisible",
            )

    # Keep semantic rows in top-to-bottom order even where adjacent categories
    # have no direct provenance edge.
    for rows in (relevant_rows, peripheral_rows):
        non_empty_rows = tuple(row for row in _row_node_ids(rows) if row)

        for upper_row, lower_row in zip(
            non_empty_rows,
            non_empty_rows[1:],
            strict=False,
        ):
            append_edge(
                f"{mermaid_graph_node_id(upper_row[0])} "
                f"~~~ {mermaid_graph_node_id(lower_row[0])}",
                edge_class="invisible",
            )

    if grouping == "flat":
        # Anchor each section label above its own first row.
        if focus_anchors:
            append_edge(
                f"explanation_label ~~~ {focus_anchors[0][0]}",
                edge_class="invisible",
            )
        if peripheral_anchors:
            append_edge(
                f"peripheral_label ~~~ {peripheral_anchors[0][0]}",
                edge_class="invisible",
            )

    # Keep the peripheral section below the focused explanation.
    if relevant_facts and peripheral_facts:
        focus_anchor = target_id or relevant_facts[-1].id
        peripheral_anchor = peripheral_facts[0].id

        append_edge(
            f"{mermaid_node_id(focus_anchor)} ~~~ {mermaid_node_id(peripheral_anchor)}",
            edge_class="invisible",
        )

    lines.append("")
    lines.extend(f"    classDef {name} {style};" for name, style in _FOCUS_CLASS_DEFS)
    lines.append("")
    lines.extend(f"    classDef {name} {style};" for name, style in _MUTED_CLASS_DEFS)

    lines.append("")

    if grouping == "flat":
        _append_class_assignment(lines, ("explanation_label",), "sectionLabel")
        if peripheral_anchors:
            _append_class_assignment(lines, ("peripheral_label",), "mutedSectionLabel")

    for rows, anchors, prefix in (
        (relevant_rows, focus_anchors, "focus"),
        (peripheral_rows, peripheral_anchors, "muted"),
    ):
        # Only the focus region can contain the target check; the
        # peripheral region never does, so nothing is excluded there.
        excluded_check_id = target_id if prefix == "focus" else None

        _append_class_assignment(
            lines,
            (mermaid_node_id(node.id) for node in rows.givens),
            f"{prefix}Given",
        )
        _append_class_assignment(
            lines,
            (mermaid_derivation_id(node.id) for node in rows.reasoning),
            f"{prefix}Reasoning",
        )
        _append_class_assignment(
            lines,
            (mermaid_node_id(node.id) for node in rows.derived),
            f"{prefix}Derived",
        )
        _append_class_assignment(
            lines,
            (
                mermaid_node_id(node.id)
                for node in rows.checks
                if node.id != excluded_check_id
            ),
            f"{prefix}Check",
        )

        if grouping == "flat":
            _append_class_assignment(
                lines,
                (label_id for label_id, _ in anchors),
                "rowLabel" if prefix == "focus" else "mutedRowLabel",
            )

        if prefix == "focus" and target_id is not None:
            target = graph.fact(target_id)

            target_class = {
                FactKind.GIVEN: "focusGiven",
                FactKind.DERIVED: "focusDerived",
                FactKind.CHECK: "targetCheck",
            }[target.kind]

            _append_class_assignment(
                lines,
                (mermaid_node_id(target_id),),
                target_class,
            )

    if grouping == "subgraph":
        lines.extend(
            [
                "",
                "    style explanation_region "
                "fill:#FFFFFF,stroke:#455A64,stroke-width:2px;",
            ]
        )

        if peripheral_ids:
            lines.append(
                "    style peripheral_region "
                "fill:#FAFAFA,stroke:#D5D5D5,stroke-width:1px,"
                "stroke-dasharray:5 5;"
            )

        for row_id in focus_row_ids:
            lines.append(
                f"    style {row_id} fill:#FCFDFE,stroke:#C6D0D7,stroke-width:1px;"
            )

        for row_id in peripheral_row_ids:
            lines.append(
                f"    style {row_id} fill:#FCFCFC,stroke:#E0E0E0,stroke-width:1px;"
            )

    lines.append("")

    link_styles: tuple[tuple[Literal["focus", "muted", "invisible"], str], ...] = (
        ("focus", "stroke:#37474F,stroke-width:3px,opacity:1"),
        ("muted", "stroke:#C5C5C5,stroke-width:1px,opacity:0.42"),
        ("invisible", "stroke:transparent,stroke-width:0px,opacity:0"),
    )
    for edge_class, style in link_styles:
        _append_link_style(lines, edge_indices[edge_class], style)

    if include_clicks:
        clickable_facts = tuple(
            fact for fact in graph.nodes.values() if fact.source is not None
        )

        if clickable_facts:
            lines.append("")

        for fact in clickable_facts:
            assert fact.source is not None
            lines.append(
                f"    click {mermaid_node_id(fact.id)} "
                f'"{mermaid_escape(mermaid_source_url(fact.source))}" '
                f'"Go to source"'
            )

    return "\n".join(lines)

graph_to_mermaid_markdown

graph_to_mermaid_markdown(
    graph,
    *,
    focus=None,
    grouping="flat",
    include_config=True,
    include_clicks=True
)

Render a FactGraph as a fenced Mermaid Markdown block.

Parameters:

Name	Type	Description	Default
graph	FactGraph[StateT]	The FactGraph to render.	required
focus	MermaidFocus	The node/fact to focus on.	None
grouping	MermaidGrouping	The grouping/layout style.	'flat'
include_config	bool	Whether to include default Mermaid config markers.	True
include_clicks	bool	Whether to include hyperlink actions for clickable nodes.	True

Returns:

Type	Description
str	The fenced Mermaid Markdown block string.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def graph_to_mermaid_markdown[StateT](
    graph: FactGraph[StateT],
    *,
    focus: MermaidFocus = None,
    grouping: MermaidGrouping = "flat",
    include_config: bool = True,
    include_clicks: bool = True,
) -> str:
    """Render a [FactGraph][guardrail_solver.reasoning.FactGraph] as a fenced Mermaid Markdown block.

    Args:
        graph: The [FactGraph][guardrail_solver.reasoning.FactGraph] to render.
        focus: The node/fact to focus on.
        grouping: The grouping/layout style.
        include_config: Whether to include default Mermaid config markers.
        include_clicks: Whether to include hyperlink actions for clickable nodes.

    Returns:
        The fenced Mermaid Markdown block string.
    """
    mermaid = graph_to_mermaid(
        graph,
        focus=focus,
        grouping=grouping,
        include_config=include_config,
        include_clicks=include_clicks,
    )
    return f"```mermaid\n{mermaid}\n```"

mermaid_fact_declaration

mermaid_fact_declaration(node, *, include_subject)

Declare a fact using Mermaid's native Markdown wrapping.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def mermaid_fact_declaration(
    node: FactNode,
    *,
    include_subject: bool,
) -> str:
    """Declare a fact using Mermaid's native Markdown wrapping."""
    node_id = mermaid_node_id(node.id)
    label = mermaid_fact_label(
        node,
        include_subject=include_subject,
    )

    if node.kind is FactKind.GIVEN:
        return f'{node_id}["`{label}`"]'

    # mermaid_fact_label (above) already raised for any kind other than
    # GIVEN/DERIVED/CHECK, via mermaid_fact_heading's own exhaustiveness check.
    return f'{node_id}("`{label}`")'

mermaid_fact_label

mermaid_fact_label(node, *, include_subject)

Render a natively wrapping label without internal provenance ids.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def mermaid_fact_label(
    node: FactNode,
    *,
    include_subject: bool,
) -> str:
    """Render a natively wrapping label without internal provenance ids."""
    parts = [f"**{mermaid_fact_heading(node)}**"]

    if include_subject and node.subject is not None:
        parts.append(node.subject.capitalize())

    parts.append(node.text)

    return mermaid_markdown_label(parts)

mermaid_graph_node_id

mermaid_graph_node_id(node_id)

Return the Mermaid id corresponding to a provenance graph node.

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/renderers/mermaid.py

def mermaid_graph_node_id(node_id: GraphNodeId) -> str:
    """Return the Mermaid id corresponding to a provenance graph node."""
    if isinstance(node_id, FactId):
        return mermaid_node_id(node_id)

    if isinstance(node_id, DerivationId):
        return mermaid_derivation_id(node_id)

    raise TypeError(f"Unknown graph node id: {node_id!r}")