Home automation — all cases

Every case file under examples/home-automation/cases/, inlined. _pass cases should prove; _fail cases should be rejected by the prover.

See the curated walk-through for context on the trusted module and contract vocabulary.

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)

examples/home-automation/cases/grocery_budget_fail.py

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

import clauz3


@clauz3.guarantee(home.grocery_budget(20))
def main() -> None:
    order_grocery("milk", 2, 8)
    order_grocery("steak", 1, 18)

examples/home-automation/cases/grocery_budget_pass.py

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

import clauz3


@clauz3.guarantee(home.grocery_budget(50))
def main() -> None:
    order_grocery("milk", 2, 8)
    order_grocery("bread", 1, 5)
    order_grocery("eggs", 1, 6)

examples/home-automation/cases/grocery_qty_precondition_fail.py

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

import clauz3


@clauz3.guarantee(home.grocery_budget(50))
def main() -> None:
    order_grocery("milk", 0, 8)

examples/home-automation/cases/home_no_guarantees_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.no_guarantees())
def main() -> None:
    set_thermostat("attic", 88)
    unlock_door("front")
    order_grocery("caviar", 5, 400)

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")

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")

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")

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/only_unlock_doors_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.only_unlock_doors(["back", "garage"]))
def main() -> None:
    unlock_door("back")
    unlock_door("front")

examples/home-automation/cases/only_unlock_doors_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.only_unlock_doors(["back", "garage"]))
def main() -> None:
    unlock_door("back")
    unlock_door("garage")

examples/home-automation/cases/temp_range_fail.py

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

import clauz3


@clauz3.guarantee(home.temp_between(60, 72))
def main() -> None:
    set_thermostat("living_room", 68)
    set_thermostat("bedroom", 85)

examples/home-automation/cases/temp_range_pass.py

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

import clauz3


@clauz3.guarantee(home.temp_between(60, 72))
def main() -> None:
    set_thermostat("living_room", 68)
    set_thermostat("bedroom", 65)