The complete worked example

This is the full source behind the front-page presentation — the same puzzle, all four subjects, executed and validated during this site's build, not transcribed by hand.

The puzzle

Source: src/guardrail_calculus/examples/landing_hero_puzzle.py

from __future__ import annotations

from dataclasses import dataclass
from typing import Any, TypeAlias

from guardrail_calculus import (
    DEPARTURE,
    EntityKind,
    SubjectFacts,
    SubjectRef,
    clock_from_hhmm,
    duration_hours,
    occurrence,
    ref,
    subject,
)


@dataclass(frozen=True)
class LandingHeroSubject:
    """A traveller in the landing-page hero puzzle. No fields: a departure is
    an occurrence (people-and-events-in-explanations.md E1c)."""


@dataclass(frozen=True)
class LandingHeroPuzzle[
    AveryT: SubjectFacts[Any, Any, Any],
    BlakeT: SubjectFacts[Any, Any, Any],
    CaseyT: SubjectFacts[Any, Any, Any],
    DrewT: SubjectFacts[Any, Any, Any],
]:
    avery: AveryT
    blake: BlakeT
    casey: CaseyT
    drew: DrewT


SubjectRefFacts: TypeAlias = SubjectFacts[None, Any, SubjectRef[LandingHeroSubject]]

LandingHeroPuzzleRefs: TypeAlias = LandingHeroPuzzle[
    SubjectRefFacts,
    SubjectRefFacts,
    SubjectRefFacts,
    SubjectRefFacts,
]


r = ref[LandingHeroPuzzleRefs]

avery_departs = occurrence("avery_departs", DEPARTURE, agent=r.avery.own)
blake_departs = occurrence("blake_departs", DEPARTURE, agent=r.blake.own)
casey_departs = occurrence("casey_departs", DEPARTURE, agent=r.casey.own)
drew_departs = occurrence("drew_departs", DEPARTURE, agent=r.drew.own)


def _build_landing_hero_puzzle():
    """docs/dev/sprints/roadmap/+1/landing-page.md Phase 1: the canonical flight
    puzzle (guardrail_calculus.examples.flight_puzzle) with two edits, so the hero
    shows VERIFIED, FALSIFIED and a contingent UNKNOWN in one small example instead
    of four UNKNOWNs and one VERIFIED. Avery's 06:20 moves from check "A" to a
    given (so check "B" can be falsified against it), and Casey's given ("departs
    at the same time as Avery") is dropped so Casey stays genuinely unconstrained --
    the contingent UNKNOWN, not a backend limit.
    """
    return LandingHeroPuzzle(
        avery=(
            subject(name="Avery", kind=EntityKind.PERSON)
            .occurs(avery_departs)
            .given(
                avery_departs.at(clock_from_hhmm(620)).annotate(
                    "Avery departs at 06:20."
                )
            )
            .block()
        ),
        blake=(
            subject(name="Blake", kind=EntityKind.PERSON)
            .occurs(blake_departs)
            .given(
                blake_departs.at(drew_departs.time - duration_hours(1)).annotate(
                    "Blake departs one hour before Drew."
                )
            )
            .check(
                "B",
                blake_departs.at(avery_departs.time).annotate(
                    "Blake departs when Avery does."
                ),
            )
            .check(
                "C",
                blake_departs.at(clock_from_hhmm(830)).annotate(
                    "Blake departs at 08:30."
                ),
            )
            .check(
                "D",
                (blake_departs.time > avery_departs.time).annotate(
                    "Blake departs after Avery."
                ),
            )
            .block()
        ),
        casey=(
            subject(name="Casey", kind=EntityKind.PERSON)
            .occurs(casey_departs)
            .check(
                "E",
                (
                    casey_departs.time + duration_hours(8) <= clock_from_hhmm(1520)
                ).annotate("Casey's 8-hour journey ends by 15:20."),
            )
            .block()
        ),
        drew=(
            subject(name="Drew", kind=EntityKind.PERSON)
            .occurs(drew_departs)
            .given(
                (drew_departs.at(clock_from_hhmm(1730) - duration_hours(8))).annotate(
                    "Drew departs 8 hours before 17:30."
                )
            )
            .block()
        ),
    )


landing_hero_puzzle = _build_landing_hero_puzzle()

The verdicts

Solving it and classifying every check against the base facts:

Check	Proposition	Verdict
B	Blake departs when Avery does	FALSIFIED
C	Blake departs at 08:30	VERIFIED
D	Blake departs after Avery	VERIFIED
E	Casey's 8-hour journey ends by 15:20	UNKNOWN

C and D follow from Drew's and Blake's givens by direct derivation. B is refuted by the same derivation — Blake's departure time is fixed at 08:30, and nothing says Avery's matches it. E is genuinely undecided: Casey carries no given at all, so her departure time is unconstrained, and the rule set correctly reports that as UNKNOWN rather than guessing.

Pinned by packages/guardrail-solver/tests/test_landing_hero_puzzle.py — a future change to the solver breaks that test, not this page.

The provenance graph

Every node below is either a given, a derivation step, or a check; every edge is a real dependency the solver traced, not an illustration.

See how reasoning works for what the node shapes and edge types mean, and how a check's verdict is decided from satisfiability and refutability.