Facts & propositions (guardrail_calculus.facts)

Propositions and the type-level chain of labelled checks shared by the builder surface and the reasoning layer.

facts

Propositions and the typed check chain.

Prop wraps a boolean expression with optional human text; Check, Nil, and Snoc form the type-level list of labelled checks accumulated by subject builders, and SubjectFacts is the sealed block a subject contributes to a puzzle.

Shared by the builder surface and the reasoning layer; imports only the kernel and the dimensions module, so it stays cycle-free.

ExprT module-attribute

ExprT = TypeVar('ExprT')

PropT module-attribute

PropT = TypeVar('PropT', bound=Prop)

BoolishT module-attribute

BoolishT = TypeVar('BoolishT', bound=Boolish_Bound)

Given_Bound module-attribute

Given_Bound = Prop[Any] | None

Prop dataclass

Bases: Generic[ExprT]

A proposition: a boolean expression plus optional human-facing text.

Prop is what .given(...) and .check(...) store. text is the sentence shown in explanations; when omitted it falls back to the expression's own label. bind re-roots the proxy _ to a concrete subject during ingestion.

Attributes:

Name	Type	Description
expr	ExprT	The underlying expression (e.g., a BoolExpr).
text	str | None	Human-facing description of the proposition.

Source code in src/guardrail_calculus/facts.py

@dataclass(frozen=True)
class Prop(Generic[ExprT]):
    """A proposition: a boolean expression plus optional human-facing text.

    [Prop][guardrail_calculus.facts.Prop] is what `.given(...)` and `.check(...)` store.
    `text` is the sentence shown in explanations; when omitted it falls back to the
    expression's own label. `bind` re-roots the proxy `_` to a concrete subject during ingestion.

    Attributes:
        expr: The underlying expression (e.g., a [BoolExpr][guardrail_kernel.expressions.BoolExpr]).
        text: Human-facing description of the proposition.
    """

    expr: ExprT
    text: str | None = None

    @property
    def display_text(self) -> str | None:
        if self.text is not None:
            return self.text

        if is_bool_like(self.expr):
            return cast(BoolLike, self.expr).label

        return None

    def bind(self, subject_name: str) -> Prop[BoolExpr[Any]]:
        if not isinstance(self.expr, BoolExpr):
            raise TypeError(f"Only BoolExpr props can be bound, got {self.expr!r}")

        return Prop(
            expr=bind_bool_expr(self.expr, subject_name=subject_name),
            text=self.text,
        )

expr instance-attribute

expr

text class-attribute instance-attribute

text = None

display_text property

display_text

bind

bind(subject_name)

Source code in src/guardrail_calculus/facts.py

def bind(self, subject_name: str) -> Prop[BoolExpr[Any]]:
    if not isinstance(self.expr, BoolExpr):
        raise TypeError(f"Only BoolExpr props can be bound, got {self.expr!r}")

    return Prop(
        expr=bind_bool_expr(self.expr, subject_name=subject_name),
        text=self.text,
    )

ChecksLike

Bases: Protocol

Structural protocol for the type-level check chain.

Implemented by Nil and Snoc.

Source code in src/guardrail_calculus/facts.py

class ChecksLike(Protocol):
    """Structural protocol for the type-level check chain.

    Implemented by [Nil][guardrail_calculus.facts.Nil] and [Snoc][guardrail_calculus.facts.Snoc].
    """

    def items(self) -> Iterable[tuple[str, Prop[Any]]]: ...

items

items()

Source code in src/guardrail_calculus/facts.py

def items(self) -> Iterable[tuple[str, Prop[Any]]]: ...

Check dataclass

A single labelled candidate proposition, e.g. check "A" over a prop.

The label is kept in the type (LabelT) so a solved puzzle can be indexed by literal label with the result type preserved.

Attributes:

Name	Type	Description
label	LabelT	The literal string label identifying the check.
prop	PropT	The checked Prop proposition.

Source code in src/guardrail_calculus/facts.py

@dataclass(frozen=True)
class Check[LabelT: str, PropT: Prop[Any]]:
    """A single labelled candidate proposition, e.g. check `"A"` over a prop.

    The label is kept in the type (`LabelT`) so a solved puzzle can be indexed
    by literal label with the result type preserved.

    Attributes:
        label: The literal string label identifying the check.
        prop: The checked [Prop][guardrail_calculus.facts.Prop] proposition.
    """

    label: LabelT
    prop: PropT

label instance-attribute

label

prop instance-attribute

prop

Nil dataclass

The empty check chain (cons-list base case).

See Snoc for the recursive case.

Source code in src/guardrail_calculus/facts.py

@dataclass(frozen=True)
class Nil:
    """The empty check chain (cons-list base case).

    See [Snoc][guardrail_calculus.facts.Snoc] for the recursive case.
    """

    def items(self) -> Iterable[tuple[str, Prop[Any]]]:
        return ()

items

items()

Source code in src/guardrail_calculus/facts.py

def items(self) -> Iterable[tuple[str, Prop[Any]]]:
    return ()

Snoc dataclass

A check chain: everything in init followed by one more last.

Builders accumulate checks by snoc-ing, so the full sequence of labels and props is recoverable both at runtime (items) and in the static type.

Attributes:

Name	Type	Description
init	InitT	The preceding part of the check chain.
last	LastT	The last Check added to the chain.

Source code in src/guardrail_calculus/facts.py

@dataclass(frozen=True)
class Snoc[InitT: ChecksLike, LastT: Check[Any, Any]]:
    """A check chain: everything in `init` followed by one more `last`.

    Builders accumulate checks by snoc-ing, so the full sequence of labels and
    props is recoverable both at runtime (`items`) and in the static type.

    Attributes:
        init: The preceding part of the check chain.
        last: The last [Check][guardrail_calculus.facts.Check] added to the chain.
    """

    init: InitT
    last: LastT

    def items(self) -> Iterable[tuple[str, Prop[Any]]]:
        yield from self.init.items()
        yield self.last.label, self.last.prop

init instance-attribute

init

last instance-attribute

last

items

items()

Source code in src/guardrail_calculus/facts.py

def items(self) -> Iterable[tuple[str, Prop[Any]]]:
    yield from self.init.items()
    yield self.last.label, self.last.prop

SubjectFacts dataclass

The sealed block one subject contributes to a puzzle.

Produced by subject()...block(). given is the subject's premise (if any), checks is its type-level chain of candidate propositions, and own is the self-reference used inside the block.

Attributes:

Name	Type	Description
own	OwnT	The self-reference proxy for this subject.
given	GivenT	The subject's premise/given premise.
checks	ChecksT	The chain of checks to be validated.

Source code in src/guardrail_calculus/facts.py

@dataclass(frozen=True)
class SubjectFacts[
    GivenT: Given_Bound = None,
    ChecksT: ChecksLike = Nil,
    OwnT = Any,
]:
    """The sealed block one subject contributes to a puzzle.

    Produced by `subject()...block()`. `given` is the subject's premise (if
    any), `checks` is its type-level chain of candidate propositions, and
    `own` is the self-reference used inside the block.

    Attributes:
        own: The self-reference proxy for this subject.
        given: The subject's premise/given premise.
        checks: The chain of checks to be validated.
    """

    own: OwnT
    given: GivenT
    checks: ChecksT
    _z3_dim: Literal["subject"] = field(
        default="subject",
        init=False,
        repr=False,
        compare=False,
    )

own instance-attribute

own

given instance-attribute

given

checks instance-attribute

checks

prop

prop(value: Prop[ExprT]) -> Prop[ExprT]

prop(value: ExprT) -> Prop[ExprT]

prop(value)

Coerce a boolean expression (or an existing Prop) into a Prop.

Parameters:

Name	Type	Description	Default
value	Boolish_Bound | Prop[Any]	The expression or existing proposition to coerce.	required

Returns:

Type	Description
Prop[Any]	A coerced Prop container.

Source code in src/guardrail_calculus/facts.py

def prop(value: Boolish_Bound | Prop[Any]) -> Prop[Any]:
    """Coerce a boolean expression (or an existing [Prop][guardrail_calculus.facts.Prop]) into a [Prop][guardrail_calculus.facts.Prop].

    Args:
        value: The expression or existing proposition to coerce.

    Returns:
        A coerced [Prop][guardrail_calculus.facts.Prop] container.
    """
    if isinstance(value, Prop):
        return value

    return Prop(expr=value)