Home automation example

The home-automation example is the everyday-stakes counterpart to the LIMS example. Same relation primitives — allowlists, numeric aggregation, per-fact bounds — applied to thermostats, door locks, and grocery orders.

Trusted module

set_thermostat and order_grocery carry chained-comparison preconditions (30 <= temp_f <= 90, qty > 0 and usd > 0); unlock_door has no sensible per-call value bound, so the meaningful guard is an agent-stated allowlist or an explicit single-door veto. unlock_door and lock_door also declare successor-state axioms over a DoorLocked fluent, used by the door-state-at-end contracts below.

examples/home-automation/tools/home/trusted/effects.py

import deal

from clauz3.fluent import effect, fluent

# Successor-state fluent: every door starts locked; ``unlock_door`` clears the
# bit and ``lock_door`` sets it. Contracts in ``contracts.py`` query the final
# valuation (e.g. "all doors locked at end"). Because the per-call effect bits
# below live in the trusted layer, the *trusted* layer enforces them — the
# agent cannot lie about having re-locked a door the way an honor-system
# ``end_session(front_locked)`` precondition would allow.
DoorLocked = fluent("door_locked", key=str, value=bool, initial=True)


@deal.pre(
    lambda zone, temp_f: 30 <= temp_f <= 90,
    message="temp_f must be a sane indoor range [30, 90]",
)
@deal.has("trusted")
def set_thermostat(zone: str, temp_f: int) -> None:
    """MOCK trusted thermostat setpoint.

    Sets ``zone`` thermostat to ``temp_f`` Fahrenheit. The trusted layer
    bounds the per-call value to a sane indoor range; allowed zones and a
    user-facing comfort range are agent-stated guarantees.
    """
    pass


@deal.pre(lambda door: len(door) > 0, message="door must be non-empty")
@deal.has("trusted")
@effect(lambda door: DoorLocked.set(door, False))
def unlock_door(door: str) -> None:
    """MOCK trusted door unlock.

    Unlocks ``door``. There is no per-call value the trusted layer can
    sensibly bound here; the meaningful guard is an agent-stated door
    allowlist or an explicit ``never_unlock_door`` contract. Records the
    successor-state effect ``DoorLocked[door] = False``.
    """
    pass


@deal.pre(lambda door: len(door) > 0, message="door must be non-empty")
@deal.has("trusted")
@effect(lambda door: DoorLocked.set(door, True))
def lock_door(door: str) -> None:
    """MOCK trusted door lock.

    Locks ``door``, recording the successor-state effect
    ``DoorLocked[door] = True``.
    """
    pass


@deal.pre(
    lambda item, qty, usd: qty > 0 and usd > 0,
    message="qty and usd must be positive",
)
@deal.has("trusted")
def order_grocery(item: str, qty: int, usd: int) -> None:
    """MOCK trusted grocery order.

    Adds ``qty`` units of ``item`` at ``usd`` total to the next delivery.
    Per-call positivity is enforced by the trusted layer; the household
    budget is an agent-stated guarantee.
    """
    pass

The contract vocabulary covers comfort range, door allowlists and vetoes, and grocery budget and item-count bounds.

examples/home-automation/tools/home/trusted/contracts.py

"""Home-automation predicates built from generic trusted effect facts.

These are the everyday-stakes counterpart to the lab example: thermostats,
door locks, and grocery orders. The relation primitives are the same — value
allowlists, numeric aggregation, per-fact bounds — applied to a different
effect vocabulary.
"""

from clauz3.spec import ContractSpec, contract, effect
from clauz3.spec import no_guarantees as core_no_guarantees

from .effects import DoorLocked

Thermostat = effect("set_thermostat")
Unlock = effect("unlock_door")
Grocery = effect("order_grocery")


@contract
def no_guarantees() -> ContractSpec:
    """Make no guarantees about home effects."""
    return core_no_guarantees()


# ── Thermostat ────────────────────────────────────────────────────────────────


@contract
def temp_between(min_f: int, max_f: int) -> ContractSpec:
    """Guarantee every thermostat set is within ``[min_f, max_f]`` Fahrenheit."""
    return Thermostat.all(lambda e: e.temp_f >= min_f and e.temp_f <= max_f)


@contract
def only_zones(allowed: list[str]) -> ContractSpec:
    """Guarantee every thermostat set targets a zone in ``allowed``."""
    return Thermostat.all(lambda e: e.zone in allowed)


# ── Door locks ───────────────────────────────────────────────────────────────


@contract
def no_unlocks() -> ContractSpec:
    """Guarantee no door is unlocked."""
    return Unlock.empty()


@contract
def only_unlock_doors(allowed: list[str]) -> ContractSpec:
    """Guarantee any door unlocked is in ``allowed``."""
    return Unlock.all(lambda e: e.door in allowed)


@contract
def never_unlock_door(door: str) -> ContractSpec:
    """Guarantee ``door`` is never unlocked.

    Distinct from ``only_unlock_doors``: this lets a user veto one specific
    door without enumerating an allowlist of the others.
    """
    return Unlock.where(lambda e: e.door == door).empty()


# ── Door state at end (fluents) ──────────────────────────────────────────────
#
# Unlike ``no_unlocks`` / ``never_unlock_door`` above, which forbid the unlock
# *event* anywhere in the trace, these guarantee the final *state*: a door may
# be unlocked mid-program as long as it is re-locked before the program ends.


@contract
def all_doors_locked_at_end() -> ContractSpec:
    """Guarantee every door is locked once the program finishes.

    A door may be unlocked partway through (to enter, fetch something, leave),
    as long as a later ``lock_door`` call restores it before the end.
    """
    return DoorLocked.final.all(lambda d: d.value == True)  # noqa: E712


@contract
def door_locked_at_end(door: str) -> ContractSpec:
    """Guarantee ``door`` is locked once the program finishes."""
    return DoorLocked.final[door] == True  # noqa: E712


# ── Groceries ────────────────────────────────────────────────────────────────


@contract
def grocery_budget(max_usd: int) -> ContractSpec:
    """Guarantee total grocery spend is at most ``max_usd``."""
    return Grocery.sum(lambda e: e.usd) <= max_usd


@contract
def grocery_items_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` grocery line items are ordered."""
    return Grocery.count() <= count


@contract
def no_groceries() -> ContractSpec:
    """Guarantee no grocery order is placed."""
    return Grocery.empty()

A composed "away mode"

Compose several guarantees to describe a mode. "Away mode" caps the temperature, leaves only the back door usable for a dog walker, and bounds any emergency grocery top-up:

examples/home-automation/cases/away_mode_pass.py

# ruff: noqa: F821
from tools.home.trusted import contracts as home
from tools.home.trusted.effects import order_grocery, set_thermostat, unlock_door

import clauz3


@clauz3.guarantee(home.temp_between(55, 65))
@clauz3.guarantee(home.never_unlock_door("front"))
@clauz3.guarantee(home.only_unlock_doors(["back"]))
@clauz3.guarantee(home.grocery_budget(30))
@clauz3.guarantee(home.grocery_items_at_most(2))
def main() -> None:
    set_thermostat("living_room", 58)
    set_thermostat("bedroom", 60)
    unlock_door("back")
    order_grocery("milk", 1, 8)
    order_grocery("bread", 1, 5)

Allowlist vs single-door veto

only_unlock_doors(allowed) and never_unlock_door(door) are intentionally both available. An allowlist is best when the set of acceptable doors is small; a single-door veto is best when the user wants to forbid one door without enumerating the rest.

examples/home-automation/cases/never_unlock_front_door_pass.py

# ruff: noqa: F821
from tools.home.trusted import contracts as home
from tools.home.trusted.effects import unlock_door

import clauz3


@clauz3.guarantee(home.never_unlock_door("front"))
def main() -> None:
    unlock_door("back")
    unlock_door("garage")

examples/home-automation/cases/never_unlock_front_door_fail.py

# ruff: noqa: F821
from tools.home.trusted import contracts as home
from tools.home.trusted.effects import unlock_door

import clauz3


@clauz3.guarantee(home.never_unlock_door("front"))
def main() -> None:
    unlock_door("back")
    unlock_door("front")

Door state at the end (fluents)

The contracts above forbid an unlock event anywhere in the trace. But a common errand — unlock the front door, fetch a delivery, lock up again — needs to unlock mid-program; what the user actually cares about is that the door is locked when the program ends.

That is a post-state property, and it is order-sensitive: unlock; lock and lock; unlock record the same multiset of facts but leave the door in opposite states. The relation language cannot tell them apart; a fluent can. The contracts query the DoorLocked fluent's final valuation:

examples/home-automation/cases/locked_at_end_pass.py

# ruff: noqa: F821
from tools.home.trusted import contracts as home
from tools.home.trusted.effects import lock_door, order_grocery, unlock_door

import clauz3


# The classic errand: unlock the front door, fetch a delivery, lock up again.
# The door is unlocked mid-program but re-locked before the end, so the
# final-state guarantee holds even though an unlock event occurred.
@clauz3.guarantee(home.all_doors_locked_at_end())
@clauz3.guarantee(home.door_locked_at_end("front"))
def main() -> None:
    unlock_door("front")
    order_grocery("milk", 1, 8)
    lock_door("front")

The door is unlocked partway through but re-locked before the end, so all_doors_locked_at_end() holds. Leaving any door open fails — and unlike a balanced unlock/lock count, the final-state check pins down which door is left open:

examples/home-automation/cases/locked_at_end_fail.py

# ruff: noqa: F821
from tools.home.trusted import contracts as home
from tools.home.trusted.effects import lock_door, unlock_door

import clauz3


# Unlocks the back door and re-locks it, but unlocks the front door and never
# re-locks it. ``all_doors_locked_at_end`` must fail: the final state has the
# front door open. A balanced unlock/lock *count* would not catch this — the
# trace has two unlocks and one lock, but even an equal count could leave the
# wrong door open. Only the final-state fluent rules it out.
@clauz3.guarantee(home.all_doors_locked_at_end())
def main() -> None:
    unlock_door("back")
    lock_door("back")
    unlock_door("front")

Reach for all_doors_locked_at_end() / door_locked_at_end(door) when the user cares how the house is left, and for never_unlock_door / no_unlocks when they want to forbid the unlock from ever happening at all.

All cases

Browse the full set on the all-cases page.

How they run

examples/home-automation/Justfile

trusted := "tools/home/trusted"
effects := trusted + "/effects.py"
prove := "uv run clauz3 prove --trusted-root " + trusted

test: lint cases

lint:
    uv run python -m deal lint {{effects}}

cases: temp-range-pass temp-range-fail only-unlock-doors-pass only-unlock-doors-fail never-unlock-front-door-pass never-unlock-front-door-fail grocery-budget-pass grocery-budget-fail away-mode-pass grocery-qty-precondition-fail home-no-guarantees-pass locked-at-end-pass locked-at-end-fail

temp-range-pass:
    {{prove}} cases/temp_range_pass.py

temp-range-fail:
    if {{prove}} cases/temp_range_fail.py; then exit 1; fi

only-unlock-doors-pass:
    {{prove}} cases/only_unlock_doors_pass.py

only-unlock-doors-fail:
    if {{prove}} cases/only_unlock_doors_fail.py; then exit 1; fi

never-unlock-front-door-pass:
    {{prove}} cases/never_unlock_front_door_pass.py

never-unlock-front-door-fail:
    if {{prove}} cases/never_unlock_front_door_fail.py; then exit 1; fi

grocery-budget-pass:
    {{prove}} cases/grocery_budget_pass.py

grocery-budget-fail:
    if {{prove}} cases/grocery_budget_fail.py; then exit 1; fi

away-mode-pass:
    {{prove}} cases/away_mode_pass.py

grocery-qty-precondition-fail:
    if {{prove}} cases/grocery_qty_precondition_fail.py; then exit 1; fi

home-no-guarantees-pass:
    {{prove}} cases/home_no_guarantees_pass.py

locked-at-end-pass:
    {{prove}} cases/locked_at_end_pass.py

locked-at-end-fail:
    if {{prove}} cases/locked_at_end_fail.py; then exit 1; fi