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()

Derivation dataclass

Source code in src/guardrail_calculus/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 src/guardrail_calculus/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 rx.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)
            # 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 not isinstance(conclusion, FactNode):
                raise ValueError(
                    f"Provenance steps need exactly one fact conclusion: {payload.id}"
                )
            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 _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 = rx.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 = rx.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,
        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)
        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,
    ) -> ProvenanceDag[ExprT]:
        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 rx.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)
        relevant_indices = [self._index_by_id[node_id] for node_id in relevant_ids]
        sub = self._graph.subgraph(relevant_indices)
        index_by_id = {sub.get_node_data(idx).id: idx for idx in sub.node_indices()}
        return self._replace_graph(sub, index_by_id)

from_rustworkx classmethod

from_rustworkx(graph)

Copy, validate, and adopt a raw interoperability graph.

Source code in src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/provenance.py

def validate(self) -> None:
    """Establish the complete typed provenance topology at one boundary."""
    if not rx.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)
        # 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 not isinstance(conclusion, FactNode):
            raise ValueError(
                f"Provenance steps need exactly one fact conclusion: {payload.id}"
            )
        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 src/guardrail_calculus/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 src/guardrail_calculus/provenance.py

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

explanation

explanation(step_id)

Source code in src/guardrail_calculus/provenance.py

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

facts

facts()

Source code in src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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)

explanation_node_ids

explanation_node_ids(target_id)

Return the target and every provenance node contributing to it.

Source code in src/guardrail_calculus/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 = rx.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 src/guardrail_calculus/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 src/guardrail_calculus/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 = rx.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 src/guardrail_calculus/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 src/guardrail_calculus/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)

Source code in src/guardrail_calculus/provenance.py

def with_derivation(
    self,
    derivation: DerivationNode,
    *,
    premises: tuple[FactId, ...],
    conclusion: FactId,
) -> ProvenanceDag[ExprT]:
    return self._with_step(
        derivation,
        premises=premises,
        conclusion=conclusion,
    )

with_explanation

with_explanation(explanation, *, premises, check)

Source code in src/guardrail_calculus/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 src/guardrail_calculus/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 rx.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 src/guardrail_calculus/provenance.py

def slice_for(self, target_id: FactId) -> ProvenanceDag[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)
    index_by_id = {sub.get_node_data(idx).id: idx for idx in sub.node_indices()}
    return self._replace_graph(sub, index_by_id)

DerivationId dataclass

Source code in src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/provenance.py

@dataclass(frozen=True)
class DerivationProposal(Generic[ExprT]):
    conclusion: Prop[ExprT]
    premises: tuple[FactId, ...]
    rule: str
    source: SourceSpan | None = None

conclusion instance-attribute

conclusion

premises instance-attribute

premises

rule instance-attribute

rule

source class-attribute instance-attribute

source = None

ExplanationInput dataclass

Bases: Generic[ExprT]

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

Source code in src/guardrail_calculus/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], ...]

established instance-attribute

established

checks instance-attribute

checks

ExplanationNode dataclass

Source code in src/guardrail_calculus/provenance.py

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

id instance-attribute

id

rule instance-attribute

rule

ExplanationProposal dataclass

Source code in src/guardrail_calculus/provenance.py

@dataclass(frozen=True)
class ExplanationProposal:
    check_id: FactId
    premises: tuple[FactId, ...]
    rule: str

check_id instance-attribute

check_id

premises instance-attribute

premises

rule instance-attribute

rule

FactId dataclass

Source code in src/guardrail_calculus/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 src/guardrail_calculus/provenance.py

class FactKind(str, Enum):
    GIVEN = "GIVEN"
    DERIVED = "DERIVED"
    CHECK = "CHECK"

GIVEN class-attribute instance-attribute

GIVEN = 'GIVEN'

DERIVED class-attribute instance-attribute

DERIVED = 'DERIVED'

CHECK class-attribute instance-attribute

CHECK = 'CHECK'

FactNode dataclass

Bases: Generic[ExprT]

Source code in src/guardrail_calculus/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

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

FactToken dataclass

Bases: Generic[ExprT]

Source code in src/guardrail_calculus/provenance.py

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

id instance-attribute

id

SourceSpan dataclass

Source code in src/guardrail_calculus/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 _insert_fact(
        self,
        node: FactNode[BoolRef],
        *,
        index_expression: bool,
    ) -> tuple[FactId, FactGraph[StateT]]:
        by_expr = (
            {**self.by_expr, self._algebra.key(node.expr): 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,
        subject_name: str,
        source: SourceSpan | None,
    ) -> tuple[FactId, FactGraph[StateT], bool]:
        expr = self._algebra.normalise(expr)
        key = self._algebra.key(expr)
        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),
                subject=subject_name,
                source=source,
            ),
            index_expression=True,
        )
        return fact_id, graph, True

    def _with_check(
        self,
        *,
        expr: BoolRef,
        text: str | None,
        subject_name: str,
        check_label: str,
        source: SourceSpan | 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),
                subject=subject_name,
                check_label=check_label,
                source=source,
            ),
            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,
        source: SourceSpan | 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,
            subject_name=subject_name,
            source=source,
        )
        return FactToken[E](fact_id), graph

    def add_check[E: Boolish_Bound](
        self,
        prop_: Prop[E],
        *,
        subject_name: str,
        check_label: str,
        source: SourceSpan | 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,
            subject_name=subject_name,
            check_label=check_label,
            source=source,
        )
        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._algebra.key(expr)
        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),
            source=proposal.source,
        )
        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,
            ),
        )

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

    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,
        )

    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: BoolRef,
    ) -> CheckResult:
        return classify(
            self.base_exprs(), check, backend=self.reasoning_backend.semantics
        )

    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]:
        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}")
        premises = self._premise_nodes(proposal.premises)
        if (
            self.reasoning_backend.notary.notarise(
                [premise.expr for premise in premises],
                check_node.expr,
                self.reasoning_backend.semantics,
            )
            is not Entailment.PROVED
        ):
            raise ValueError("Explanation premises do not entail the check.")
        step = ExplanationNode(
            id=self._fresh_derivation_id(),
            rule=proposal.rule,
        )
        return replace(
            self,
            dag=self.dag.with_explanation(
                step,
                premises=proposal.premises,
                check=proposal.check_id,
            ),
            next_derivation_index=self.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, source=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,
    source: SourceSpan | 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,
        subject_name=subject_name,
        source=source,
    )
    return FactToken[E](fact_id), graph

add_check

add_check(prop_, *, subject_name, check_label, source=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,
    check_label: str,
    source: SourceSpan | 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,
        subject_name=subject_name,
        check_label=check_label,
        source=source,
    )
    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 is not FactKind.CHECK
    )

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,
    )

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)

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

def classify[SaturationT](
    self: FactGraph[Evidence[Consistent, SaturationT]],
    check: BoolRef,
) -> CheckResult:
    return classify(
        self.base_exprs(), check, backend=self.reasoning_backend.semantics
    )

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)

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

def apply_explanation(
    self,
    proposal: ExplanationProposal,
) -> FactGraph[StateT]:
    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}")
    premises = self._premise_nodes(proposal.premises)
    if (
        self.reasoning_backend.notary.notarise(
            [premise.expr for premise in premises],
            check_node.expr,
            self.reasoning_backend.semantics,
        )
        is not Entailment.PROVED
    ):
        raise ValueError("Explanation premises do not entail the check.")
    step = ExplanationNode(
        id=self._fresh_derivation_id(),
        rule=proposal.rule,
    )
    return replace(
        self,
        dag=self.dag.with_explanation(
            step,
            premises=proposal.premises,
            check=proposal.check_id,
        ),
        next_derivation_index=self.next_derivation_index + 1,
    )

FactGraphExplanationBackend dataclass

Use shared semantic equivalence to propose check explanations.

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

@dataclass(frozen=True)
class FactGraphExplanationBackend:
    """Use shared semantic equivalence to propose check explanations."""

    def explain(
        self,
        input_: ExplanationInput[BoolRef],
        semantics: SemanticBackend,
    ) -> Iterable[ExplanationProposal]:
        for check_node in input_.checks:
            for node in input_.established:
                if (
                    equivalent(node.expr, check_node.expr, backend=semantics)
                    is Entailment.PROVED
                ):
                    yield ExplanationProposal(
                        check_id=check_node.id,
                        premises=(node.id,),
                        rule="check is equivalent to a known fact",
                    )
                    break

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:
        for node in input_.established:
            if (
                equivalent(node.expr, check_node.expr, backend=semantics)
                is Entailment.PROVED
            ):
                yield ExplanationProposal(
                    check_id=check_node.id,
                    premises=(node.id,),
                    rule="check is equivalent to a known fact",
                )
                break

ForwardDerivationBackend dataclass

Current Python fixed-point rules behind the derivation interface.

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

@dataclass(frozen=True)
class ForwardDerivationBackend:
    """Current Python fixed-point rules behind the derivation interface."""

    def derive(
        self,
        input_: DerivationInput[BoolRef],
    ) -> Iterable[DerivationProposal[BoolRef]]:
        yield from _propose_simplified_equalities(input_)
        yield from _propose_offset_constants(input_)
        yield from _propose_equalities_from_shared_constants(input_)

derive

derive(input_)

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

def derive(
    self,
    input_: DerivationInput[BoolRef],
) -> Iterable[DerivationProposal[BoolRef]]:
    yield from _propose_simplified_equalities(input_)
    yield from _propose_offset_constants(input_)
    yield from _propose_equalities_from_shared_constants(input_)

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

LinearOffset dataclass

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

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

source instance-attribute

source

offset instance-attribute

offset

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."""
        if not is_dataclass(puzzle):
            raise TypeError(f"Expected dataclass puzzle schema, got {puzzle!r}")

        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(puzzle):
            subject_name = field_info.name
            block = getattr(puzzle, subject_name)

            if not isinstance(block, SubjectFacts):
                raise TypeError(
                    f"Puzzle field {subject_name!r} is not SubjectFacts: {block!r}"
                )

            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.

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."""
    if not is_dataclass(puzzle):
        raise TypeError(f"Expected dataclass puzzle schema, got {puzzle!r}")

    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(puzzle):
        subject_name = field_info.name
        block = getattr(puzzle, subject_name)

        if not isinstance(block, SubjectFacts):
            raise TypeError(
                f"Puzzle field {subject_name!r} is not SubjectFacts: {block!r}"
            )

        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(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))

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(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))

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=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),
            solver_factory=self.solver_factory,
            timeout_ms=self.timeout_ms,
            rlimit=self.rlimit,
        )

solver_factory class-attribute instance-attribute

solver_factory = field(default=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),
        solver_factory=self.solver_factory,
        timeout_ms=self.timeout_ms,
        rlimit=self.rlimit,
    )

Consistent

Source code in src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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."""
        ...

ingress

ingress(expr)

Lower an authored or raw proposition into the stored type.

Source code in src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/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 src/guardrail_calculus/reasoning_contract.py

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

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],
        *,
        subject_name: str,
        source: SourceSpan | None = None,
    ) -> tuple[
        FactToken[Any], ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]]
    ]: ...

    def add_check(
        self: ReasoningGraphBackend[StateT_co],
        prop_: Prop[Any],
        *,
        subject_name: str,
        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: BoolRef,
    ) -> CheckResult: ...

    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, 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],
    *,
    subject_name: str,
    source: SourceSpan | None = None,
) -> tuple[
    FactToken[Any], ReasoningGraphBackend[Evidence[Unchecked, Unsaturated]]
]: ...

add_check

add_check(prop_, *, subject_name, 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,
    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: BoolRef,
) -> CheckResult: ...

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 src/guardrail_calculus/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 src/guardrail_calculus/reasoning_contract.py

class Unchecked:
    pass

Unsaturated

Source code in src/guardrail_calculus/reasoning_contract.py

class Unsaturated:
    pass

empty_rustworkx_digraph

empty_rustworkx_digraph()

Source code in src/guardrail_calculus/provenance.py

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

to_wire_explanation_dag

to_wire_explanation_dag(dag)

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.

Source code in src/guardrail_calculus/provenance.py

def to_wire_explanation_dag(dag: ProvenanceDag[ExprT]) -> 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.
    """
    return WireExplanationDag(
        schema_version=EXPLANATION_SCHEMA_VERSION,
        nodes=tuple(_wire_node(node) for node in dag.nodes()),
        edges=tuple(
            WireProvenanceEdge(source=str(source), target=str(target))
            for source, target in dag.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 src/guardrail_calculus/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

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.

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.
    """
    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
    )

arith_key

arith_key(expr)

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

def arith_key(expr: ArithRef) -> str:
    return 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/_python.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 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/_python.py

def as_int(expr: object) -> int | None:
    """The Python value of an integer numeral, 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()
    return None

check_with_core

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

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

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] = Solver,
    timeout_ms: int | None = None,
    rlimit: int | None = None,
) -> SolveResult:
    """Low-level Z3 solve retaining a model, unsat core, or unknown result.

    ``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)
    tracked: dict[str, BoolRef] = {}

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

    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[str(k)] 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]

equality_sides

equality_sides(expr)

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

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

    if not is_eq(expr):
        return None

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

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)

expr_key

expr_key(expr)

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

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

is_eq

is_eq(expr)

Source code in packages/guardrail-solver/src/guardrail_solver/reasoning/_python.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/_python.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, simplify(expr))

    if is_int_value(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, 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/_python.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/_python.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 as_int(lhs) is None:
        return lhs, parsed_rhs.source, parsed_rhs.offset

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

    return None

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_arith

render_arith(expr)

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

def render_arith(expr: ArithRef) -> str:
    return str(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.

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.
    """
    slot_map: Mapping[str, Dimension[Any]] = slots if slots is not None else {}
    constant = parse_constant_equality(expr)
    if constant is not None:
        var, value = constant
        rendered = _slot_display_value(render_arith(var), value, slot_map)
        return f"{render_arith(var)} is {rendered}."

    offset = parse_offset_equality(expr)
    if offset is not None:
        target, source, amount = offset
        unit = _offset_unit(render_arith(target), render_arith(source), slot_map)

        if amount < 0:
            return (
                f"{render_arith(target)} is {-amount}{unit} before "
                f"{render_arith(source)}."
            )
        if amount > 0:
            return (
                f"{render_arith(target)} is {amount}{unit} after "
                f"{render_arith(source)}."
            )
        return f"{render_arith(target)} is the same as {render_arith(source)}."

    return 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()

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[Mapping[str, Any]],
) -> 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="check matches a known fact after linear-arithmetic normalization",
        )

linear_records

linear_records(nodes)

Flatten facts into opaque, JSON-ready records a structural engine can compare by key, plus a lookup resolving each key back to its live ArithRef.

Shared by RustDerivationBackend/RustExplanationBackend: the shape is identical for DerivationInput.established and ExplanationInput.established/.checks -- a check is just another FactNode. Only the caller's use of the records differs. A structural engine only ever compares key/target_key/source_key for equality -- it never needs to interpret the ArithRef they stand for, which is why crossing the FFI boundary as opaque strings is sufficient.

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

def linear_records(
    nodes: Sequence[FactNode],
) -> tuple[list[dict[str, Any]], dict[str, ArithRef]]:
    """Flatten facts into opaque, JSON-ready records a structural engine can
    compare by key, plus a lookup resolving each key back to its live
    ``ArithRef``.

    Shared by ``RustDerivationBackend``/``RustExplanationBackend``: the shape
    is identical for ``DerivationInput.established`` and
    ``ExplanationInput.established``/``.checks`` -- a check is just another
    ``FactNode``. Only the caller's use of the records differs. A structural
    engine only ever compares ``key``/``target_key``/``source_key`` for
    equality -- it never needs to interpret the ``ArithRef`` they stand for,
    which is why crossing the FFI boundary as opaque strings is sufficient.
    """
    records: list[dict[str, Any]] = []
    lookup: dict[str, ArithRef] = {}

    for node in nodes:
        record: dict[str, Any] = {"id": str(node.id), "const": None, "offset": None}

        constant = parse_constant_equality(node.expr)
        if constant is not None:
            var, value = constant
            key = arith_key(var)
            lookup[key] = var
            record["const"] = {
                "key": key,
                "value": value,
                # _propose_simplified_equalities' self-skip guard: whether
                # reconstructing `var == value` is already what this fact says.
                # (key, value) alone can't decide this -- that pair is
                # deliberately order-agnostic -- so it must be precomputed here.
                "already_simplified": (
                    expr_key(cast(BoolRef, var == value)) == expr_key(node.expr)
                ),
            }

        offset = parse_offset_equality(node.expr)
        if offset is not None:
            target, source, minutes = offset
            target_key = arith_key(target)
            source_key = arith_key(source)
            lookup[target_key] = target
            lookup[source_key] = source
            record["offset"] = {
                "target_key": target_key,
                "source_key": source_key,
                "minutes": minutes,
            }

        records.append(record)

    return records, lookup

proposals_from_records

proposals_from_records(
    proposals, lookup, slot_dimensions=None
)

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

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

def proposals_from_records(
    proposals: Iterable[Mapping[str, Any]],
    lookup: Mapping[str, ArithRef],
    slot_dimensions: Mapping[str, Dimension[Any]] | None = None,
) -> Iterator[DerivationProposal]:
    """Reconstruct ``DerivationProposal``s from a structural engine's flat,
    opaque-keyed output, resolving each key back to the live ``ArithRef`` it
    came from. The engine itself never constructs or returns a z3 expression.
    """
    for item in proposals:
        if item["kind"] == "var_eq_const":
            conclusion = cast(BoolRef, lookup[item["key"]] == item["value"])
        else:
            conclusion = cast(
                BoolRef, lookup[item["left_key"]] == lookup[item["right_key"]]
            )

        yield DerivationProposal(
            conclusion=_derived_prop(conclusion, slot_dimensions or {}),
            premises=tuple(FactId(premise) for premise in item["premises"]),
            rule=item["rule"],
        )

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.
    """
    base = solved.graph.base_exprs()
    lines = ["| Check | Proposition | Verdict |", "|---|---|---|"]
    for label in sorted(solved.check_tokens):
        node = solved.graph.nodes[solved.check_tokens[label].id]
        proposition = (node.text or "").rstrip(".")
        verdict = verdict_badge(classify_check(base, node.expr).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}")