The complete worked example

This is the full source behind the hero example on the front page — 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 (
    SubjectFacts,
    SubjectRef,
    clock_from_hhmm,
    duration_hours,
    ref,
    subject,
    subject_ref,
)
from guardrail_calculus.dimension_value_builtins import ClockRef


@dataclass(frozen=True)
class LandingHeroSubject:
    """The subject schema for the landing-page hero puzzle: a departure observable."""

    departure: ClockRef


@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]
_ = subject_ref[LandingHeroSubject]


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()
            .given(
                (_.departure @ clock_from_hhmm(620)).annotate("Avery departs at 06:20.")
            )
            .block()
        ),
        blake=(
            subject()
            .given(
                (_.departure @ (r.drew.own.departure - duration_hours(1))).annotate(
                    "Blake departs one hour before Drew."
                )
            )
            .check(
                "B",
                (_.departure @ r.avery.own.departure).annotate(
                    "Blake departs when Avery does."
                ),
            )
            .check(
                "C",
                (_.departure @ clock_from_hhmm(830)).annotate(
                    "Blake departs at 08:30."
                ),
            )
            .check(
                "D",
                (_.departure > r.avery.own.departure).annotate(
                    "Blake departs after Avery."
                ),
            )
            .block()
        ),
        casey=(
            subject()
            .check(
                "E",
                (_.departure + duration_hours(8) <= clock_from_hhmm(1520)).annotate(
                    "Casey's 8-hour journey ends by 15:20."
                ),
            )
            .block()
        ),
        drew=(
            subject()
            .given(
                (_.departure @ (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 tests/examples/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.