Email — all cases

Every case file under examples/email/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/email/cases/at_most_two_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.at_most(2))
def main() -> None:
    send_email("bob@example.com", "hi")
    send_email("ann@example.com", "hi")
    send_email("cal@example.com", "hi")

examples/email/cases/at_most_two_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.at_most(2))
def main() -> None:
    send_email("bob@example.com", "hi")
    send_email("ann@example.com", "hi")

examples/email/cases/bob_at_most_two_branch_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.recipient_at_most("bob@example.com", 2))
def main(use_third: bool) -> None:
    send_email("bob@example.com", "first")
    send_email("bob@example.com", "second")
    if use_third:
        send_email("ann@example.com", "third")
    else:
        send_email("cal@example.com", "third")

examples/email/cases/bob_at_most_two_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.recipient_at_most("bob@example.com", 2))
def main() -> None:
    send_email("bob@example.com", "first")
    send_email("ann@example.com", "hi")
    send_email("bob@example.com", "second")
    send_email("bob@example.com", "third")

examples/email/cases/bob_at_most_two_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.recipient_at_most("bob@example.com", 2))
def main() -> None:
    send_email("bob@example.com", "first")
    send_email("ann@example.com", "hi")
    send_email("bob@example.com", "second")

examples/email/cases/content_length_branch_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.content_length_at_most(5))
def main(choice: bool) -> None:
    if choice:
        send_email("bob@example.com", "first")
    else:
        send_email("ann@example.com", "next")

examples/email/cases/content_length_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.content_length_at_most(5))
def main() -> None:
    send_email("bob@example.com", "too long")

examples/email/cases/content_length_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.content_length_at_most(5))
def main() -> None:
    send_email("bob@example.com", "hello")
    send_email("ann@example.com", "hi")

examples/email/cases/dead_branch_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.none())
def main() -> None:
    if False:
        send_email("ann@example.com", "hi")

examples/email/cases/helper_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


def notify_ann() -> None:
    send_email("ann@example.com", "hi")


@clauz3.guarantee(emails.only(["bob@example.com"]))
def main() -> None:
    notify_ann()

examples/email/cases/helper_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


def notify_bob() -> None:
    send_email("bob@example.com", "hi")


@clauz3.guarantee(emails.only(["bob@example.com"]))
def main() -> None:
    notify_bob()

examples/email/cases/no_guarantees_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.no_guarantees())
def main() -> None:
    send_email("bob@example.com", "long unrestricted content")
    send_email("ann@example.com", "different content")
    send_email("bob@example.com", "duplicate recipient")

examples/email/cases/nobody_emailed_twice_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


def notify(addr: str, msg: str) -> None:
    send_email(addr, msg)


@clauz3.guarantee(emails.unique_recipients())
def main() -> None:
    notify("bob@example.com", "first")
    notify("bob@example.com", "second")

examples/email/cases/none_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.none())
def main() -> None:
    send_email("bob@example.com", "hi")

examples/email/cases/none_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails

import clauz3


@clauz3.guarantee(emails.none())
def main() -> None:
    pass

examples/email/cases/only_bob_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.only(["bob@example.com"]))
def main() -> None:
    send_email("ann@example.com", "hi")

examples/email/cases/only_bob_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.only(["bob@example.com"]))
def main() -> None:
    send_email("bob@example.com", "hi")

examples/email/cases/policy_ask.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.no_guarantees())
def main() -> None:
    # Not blocked, but not within the auto-pass allow-list either, so no rule
    # fires and a human decides.
    send_email("stranger@partner.com", "intro")

examples/email/cases/policy_reject.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.no_guarantees())
def main() -> None:
    # Reaches a blocked recipient, so it cannot prove the deny rule's
    # avoidance obligation: the approval policy auto-rejects it.
    send_email("ceo@example.com", "please approve the acquisition")

examples/email/cases/precondition_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.only(["bob@example.com"]))
def main() -> None:
    send_email("not-an-email", "hi")

examples/email/cases/same_content_branch_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.same_content("bob@example.com", "ann@example.com"))
def main(use_first_message: bool) -> None:
    if use_first_message:
        send_email("bob@example.com", "first")
        send_email("ann@example.com", "first")
    else:
        send_email("bob@example.com", "second")
        send_email("ann@example.com", "second")

examples/email/cases/same_content_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.same_content("bob@example.com", "ann@example.com"))
def main() -> None:
    send_email("bob@example.com", "for bob")
    send_email("ann@example.com", "for ann")

examples/email/cases/same_content_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.same_content("bob@example.com", "ann@example.com"))
def main() -> None:
    send_email("bob@example.com", "shared")
    send_email("ann@example.com", "shared")

examples/email/cases/unique_recipients_branch_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.unique_recipients())
def main(use_first_message: bool) -> None:
    if use_first_message:
        send_email("bob@example.com", "first")
    else:
        send_email("bob@example.com", "second")

examples/email/cases/unique_recipients_fail.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.unique_recipients())
def main() -> None:
    send_email("bob@example.com", "first")
    send_email("bob@example.com", "second")

examples/email/cases/unique_recipients_pass.py

# ruff: noqa: F821
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3


@clauz3.guarantee(emails.unique_recipients())
def main() -> None:
    send_email("bob@example.com", "hi")
    send_email("ann@example.com", "hi")