Facts & propositions (guardrail_ir.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

RoleFiller module-attribute

RoleFiller = 'SubjectRef[Any]'

NO_PARTICULARS module-attribute

NO_PARTICULARS = Particulars()

At

At = PointRef[_Time] | PointValue[_Time, int]

LoggedSpan

LoggedSpan = Predicate[
    _And[
        Predicate[
            _Ge[PointRef[_Time], PointValue[_Time, int]]
        ],
        Predicate[
            _Lt[
                PointRef[_Time],
                PointExpr[
                    _Time,
                    _Add[
                        PointValue[_Time, int],
                        DisplacementValue[_Time, int],
                    ],
                ],
            ]
        ],
    ]
]

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.

Examples:

>>> from guardrail_ir.facts import Prop
>>> p = Prop(True, "My Premise")
>>> p.display_text
'My Premise'

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

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

    [Prop][guardrail_ir.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.

    Examples:
        >>> from guardrail_ir.facts import Prop
        >>> p = Prop(True, "My Premise")
        >>> p.display_text
        'My Premise'
    """

    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 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 packages/guardrail-ir/src/guardrail_ir/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 packages/guardrail-ir/src/guardrail_ir/facts.py

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

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

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

items

items()

Source code in packages/guardrail-ir/src/guardrail_ir/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.

Examples:

>>> from guardrail_ir.facts import Check, Prop
>>> c = Check("A", Prop(True))
>>> c.label
'A'

Source code in packages/guardrail-ir/src/guardrail_ir/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_ir.facts.Prop] proposition.

    Examples:
        >>> from guardrail_ir.facts import Check, Prop
        >>> c = Check("A", Prop(True))
        >>> c.label
        'A'
    """

    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.

Examples:

>>> from guardrail_ir.facts import Nil
>>> list(Nil().items())
[]

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

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

    See [Snoc][guardrail_ir.facts.Snoc] for the recursive case.

    Examples:
        >>> from guardrail_ir.facts import Nil
        >>> list(Nil().items())
        []
    """

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

items

items()

Source code in packages/guardrail-ir/src/guardrail_ir/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.

Examples:

>>> from guardrail_ir.facts import Nil, Check, Prop, Snoc
>>> chain = Snoc(Nil(), Check("A", Prop(True)))
>>> tuple(label for label, _ in chain.items())
('A',)

Source code in packages/guardrail-ir/src/guardrail_ir/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_ir.facts.Check] added to the chain.

    Examples:
        >>> from guardrail_ir.facts import Nil, Check, Prop, Snoc
        >>> chain = Snoc(Nil(), Check("A", Prop(True)))
        >>> tuple(label for label, _ in chain.items())
        ('A',)
    """

    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 packages/guardrail-ir/src/guardrail_ir/facts.py

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

Entity dataclass

Who or what a subject is, as its author says: presentation only.

people-and-events-in-explanations.md E1b. The name is the author's words for the person, carried on the request so the realiser never holds one; absent, the text keeps the subject's path. The kind is authored too, never read off a name: a role may admit only people, and a sentence asks "who" of a person and "which" of a thing.

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

@dataclass(frozen=True)
class Entity:
    """Who or what a subject is, as its author says: presentation only.

    people-and-events-in-explanations.md E1b. The name is the author's
    words for the person, carried on the request so the realiser never
    holds one; absent, the text keeps the subject's path. The kind is
    authored too, never read off a name: a role may admit only people, and a
    sentence asks "who" of a person and "which" of a thing.
    """

    kind: EntityKind
    name: str | None = None

kind instance-attribute

kind

name class-attribute instance-attribute

name = None

Occurrence dataclass

Something that happens, with its participants and its time.

Its identity is id, the author's -- never a subject's path or a display name. It is the term a puzzle reasons about (people-and-events-in-explanations.md E1c): its time is :attr:time, and givens and checks are written on that, never on a field of a person -- blake_departs.at(drew_departs.time - duration_hours(1)), blake_departs.time > avery_departs.time.

Its time's slot is named by the occurrence, occurrence.<id> on the wire (E1c step 5c, the owner's spelling): not a field of any subject, so two occurrences of one type for one principal -- Drew departs, and departs again -- keep their own times with nothing more said. Telling them apart in text is E3's.

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

@dataclass(frozen=True)
class Occurrence:
    """Something that happens, with its participants and its time.

    Its identity is ``id``, the author's -- never a subject's path or a
    display name. It is the term a puzzle reasons about
    (people-and-events-in-explanations.md E1c): its time is :attr:`time`, and
    givens and checks are written on that, never on a field of a person --
    ``blake_departs.at(drew_departs.time - duration_hours(1))``,
    ``blake_departs.time > avery_departs.time``.

    Its time's slot is named by the occurrence, ``occurrence.<id>`` on the
    wire (E1c step 5c, the owner's spelling): not a field of any subject, so
    two occurrences of one type for one principal -- Drew departs, and
    departs again -- keep their own times with nothing more said. Telling
    them apart in text is E3's.
    """

    id: str
    type: EventType
    roles: Mapping[str, RoleFiller]

    def __post_init__(self) -> None:
        for name in self.roles:
            self.type.role(name)
        missing = [role.name for role in self.type.roles if role.name not in self.roles]
        if missing:
            raise ValueError(
                f"occurrence {self.id!r} of {self.type.name} fills no {missing}"
            )
        for name, filler in self.roles.items():
            if not isinstance(filler, SubjectRef):
                raise TypeError(
                    f"occurrence {self.id!r}: its {name} is a named subject "
                    f"(`r.<name>.own`), not {filler!r}"
                )

    @property
    def time_path(self) -> tuple[str, str]:
        """The slot its time lowers to: ``("occurrence", id)``."""
        return (OCCURRENCE, self.id)

    if TYPE_CHECKING:
        # `PointRef` is a declaration-only facade over one runtime class,
        # `PointReference` (dimension_values.py), declared apart from it as
        # that module declares its facades: the event type's time is an
        # `Instant`, the family `TimeAlgebraFamily` names.
        @property
        def time(self) -> PointRef[TimeAlgebraFamily]:
            """When it happens: a point in its event type's time dimension."""
            ...

    else:

        @property
        def time(self) -> PointReference:
            """When it happens: a point in its event type's time dimension."""
            # Deferred, as `SubjectRef.__getattr__` defers it:
            # dimension_values imports from the modules this one does.
            from guardrail_ir.dimension_values import PointReference

            return PointReference(
                Path(self.time_path),
                _dimension=builtin_registry().get(self.type.time),
            )

    def at[Other](
        self, when: _PointOperand[TimeAlgebraFamily, Other]
    ) -> Predicate[_Eq[PointRef[TimeAlgebraFamily], Other]]:
        """It happened exactly at ``when``: ``blake_departs.at(clock_hm(8,
        30))``, or relative to another, ``blake_departs.at(drew_departs.time
        - duration_hours(1))``. Exactness is a claim: a time written to a
        precision is :meth:`logged`."""
        return self.time @ when

    def logged(
        self,
        when: PointValue[TimeAlgebraFamily, int],
        precision: DisplacementValue[TimeAlgebraFamily, int] | None = None,
    ) -> LoggedSpan:
        """It was recorded at ``when``, to ``precision`` -- a minute unless
        said: it happened at some instant in ``[when, when + precision)``
        (state-over-time.md S0, the owner's decision). Two occurrences logged
        in one minute may have happened in either order."""
        from guardrail_ir.dimension_value_builtins import duration_minutes

        width = duration_minutes(1) if precision is None else precision
        return (when <= self.time) & (self.time < when + width)

id instance-attribute

id

type instance-attribute

type

roles instance-attribute

roles

time_path property

time_path

The slot its time lowers to: ("occurrence", id).

time property

time

When it happens: a point in its event type's time dimension.

at

at(when)

It happened exactly at when: blake_departs.at(clock_hm(8, 30)), or relative to another, blake_departs.at(drew_departs.time - duration_hours(1)). Exactness is a claim: a time written to a precision is :meth:logged.

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

def at[Other](
    self, when: _PointOperand[TimeAlgebraFamily, Other]
) -> Predicate[_Eq[PointRef[TimeAlgebraFamily], Other]]:
    """It happened exactly at ``when``: ``blake_departs.at(clock_hm(8,
    30))``, or relative to another, ``blake_departs.at(drew_departs.time
    - duration_hours(1))``. Exactness is a claim: a time written to a
    precision is :meth:`logged`."""
    return self.time @ when

logged

logged(when, precision=None)

It was recorded at when, to precision -- a minute unless said: it happened at some instant in [when, when + precision) (state-over-time.md S0, the owner's decision). Two occurrences logged in one minute may have happened in either order.

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

def logged(
    self,
    when: PointValue[TimeAlgebraFamily, int],
    precision: DisplacementValue[TimeAlgebraFamily, int] | None = None,
) -> LoggedSpan:
    """It was recorded at ``when``, to ``precision`` -- a minute unless
    said: it happened at some instant in ``[when, when + precision)``
    (state-over-time.md S0, the owner's decision). Two occurrences logged
    in one minute may have happened in either order."""
    from guardrail_ir.dimension_value_builtins import duration_minutes

    width = duration_minutes(1) if precision is None else precision
    return (when <= self.time) & (self.time < when + width)

Absence dataclass

No occurrence of type whose roles roles fill, anywhere in [start, end] (state-over-time.md S0's absence window): "no handoff from Bram in [09:00, 09:30]". A role it leaves out is any subject.

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

@dataclass(frozen=True)
class Absence:
    """No occurrence of ``type`` whose roles ``roles`` fill, anywhere in
    ``[start, end]`` (state-over-time.md S0's absence window): "no handoff
    from Bram in [09:00, 09:30]". A role it leaves out is any subject."""

    type: EventType
    roles: Mapping[str, RoleFiller]
    start: At
    end: At

    def __post_init__(self) -> None:
        for name, filler in self.roles.items():
            self.type.role(name)
            if not isinstance(filler, SubjectRef):
                raise TypeError(
                    f"an absence of {self.type.name}: its {name} is a named "
                    f"subject (`r.<name>.own`), not {filler!r}"
                )

type instance-attribute

type

roles instance-attribute

roles

start instance-attribute

start

end instance-attribute

end

Initially dataclass

What a block says holds, or does not, at the start (E1c).

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

@dataclass(frozen=True)
class Initially:
    """What a block says holds, or does not, at the start (E1c)."""

    state: StateOf
    holds: bool

state instance-attribute

state

holds instance-attribute

holds

Particulars dataclass

What its author says a subject is and takes part in (E1b).

Carried whole from the builder to the sealed block: the entity, and the occurrences authored beside the subject's givens.

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

@dataclass(frozen=True)
class Particulars:
    """What its author says a subject is and takes part in (E1b).

    Carried whole from the builder to the sealed block: the entity, and the
    occurrences authored beside the subject's givens.
    """

    entity: Entity | None = None
    occurrences: tuple[Occurrence, ...] = ()
    initially: tuple[Initially, ...] = ()
    absences: tuple[Absence, ...] = ()
    #: Event types whose log is complete: every one that happened is
    #: declared (state-over-time.md S0, closure as scoped data).
    closed: tuple[EventType, ...] = ()

entity class-attribute instance-attribute

entity = None

occurrences class-attribute instance-attribute

occurrences = ()

initially class-attribute instance-attribute

initially = ()

absences class-attribute instance-attribute

absences = ()

closed class-attribute instance-attribute

closed = ()

SubjectBlock

Bases: Protocol

What a request is assembled from, of any subject block: its given, its checks and its particulars -- read-only, so every :class:SubjectFacts, whatever its type arguments, is one (backend.blocks_to_solve_request).

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

class SubjectBlock(Protocol):
    """What a request is assembled from, of any subject block: its given,
    its checks and its particulars -- read-only, so every
    :class:`SubjectFacts`, whatever its type arguments, is one
    (``backend.blocks_to_solve_request``)."""

    @property
    def given(self) -> Given_Bound: ...
    @property
    def checks(self) -> ChecksLike: ...
    @property
    def particulars(self) -> Particulars: ...

given property

given

checks property

checks

particulars property

particulars

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.

Examples:

>>> from guardrail_ir.facts import SubjectFacts, Nil
>>> block = SubjectFacts(own="my_subject", given=None, checks=Nil())
>>> block.own
'my_subject'

Source code in packages/guardrail-ir/src/guardrail_ir/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.

    Examples:
        >>> from guardrail_ir.facts import SubjectFacts, Nil
        >>> block = SubjectFacts(own="my_subject", given=None, checks=Nil())
        >>> block.own
        'my_subject'
    """

    own: OwnT
    given: GivenT
    checks: ChecksT
    #: Who the subject is and what happens with it taking part (E1b).
    particulars: Particulars = NO_PARTICULARS
    _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

particulars class-attribute instance-attribute

particulars = NO_PARTICULARS

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.

Examples:

>>> from guardrail_ir.facts import prop

>>> p = prop(True)

>>> p.expr
True

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

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

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

    Returns:
        A coerced [Prop][guardrail_ir.facts.Prop] container.

    Examples:
        >>> from guardrail_ir.facts import prop

        >>> p = prop(True)

        >>> p.expr
        True
    """
    if isinstance(value, Prop):
        return value

    return Prop(expr=value)

occurrence

occurrence(id, event_type, **roles)

An occurrence of event_type, its roles filled by subjects.

blake_departs = occurrence("blake_departs", DEPARTURE, agent=r.blake.own); then blake_departs.time is when Blake departs, and a block declares it with .occurs(blake_departs).

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

def occurrence(id: str, event_type: EventType, **roles: Any) -> Occurrence:
    """An occurrence of ``event_type``, its roles filled by subjects.

    ``blake_departs = occurrence("blake_departs", DEPARTURE, agent=r.blake.own)``;
    then ``blake_departs.time`` is when Blake departs, and a block declares it
    with ``.occurs(blake_departs)``.
    """
    return Occurrence(id=id, type=event_type, roles=roles)