Email — all cases

Every case file under examples/email/cases/, inlined. _pass cases prove; _fail cases are refuted; _skip cases leave the supported subset. Exact conclusions are pinned in tests/test_email_prover.py. policy_* files are approval-policy fixtures, not proof-outcome cases.

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

examples/email/cases/alias_import_fail.py

# ruff: noqa: F821
# Issue #129: before the fix this reported ``proved!`` because the aliased
# decorator was silently ignored, and the approval request the human sees
# listed no guarantees at all.
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3 as c


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

examples/email/cases/alias_import_pass.py

# ruff: noqa: F821
# Issue #129: ``import clauz3 as c`` names the same decorator as ``import
# clauz3``, so the guarantee must be honoured rather than dropped.
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

import clauz3 as c


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

examples/email/cases/aliased_guarantee_name_fail.py

# ruff: noqa: F821
# Issue #129: ``from clauz3 import guarantee as g`` is the other spelling the
# prover and the approval request used to drop.
from tools.email.trusted import contracts as emails
from tools.email.trusted.effects import send_email

from clauz3 import guarantee as g


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

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/aug_assign_fail.py

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

import clauz3


# `msg += ...` on a str is a plain rebinding, `msg = msg + ...`, so the prover
# tracks the concatenation and refutes the length bound. It is the same
# program as aug_assign_rewritten_fail.py, spelled with `+=`; before #109 it
# skipped because no handler was registered for `astroid.AugAssign`.
@clauz3.guarantee(emails.content_length_at_most(5))
def main() -> None:
    msg = "hi"
    msg += " a much longer body than the contract allows"
    send_email("bob@example.com", msg)

examples/email/cases/aug_assign_pass.py

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

import clauz3


# `msg += "!"` is `msg = msg + "!"`: a str is immutable, so augmented
# assignment rebinds the name and the prover tracks the new value.
@clauz3.guarantee(emails.content_length_at_most(5))
def main() -> None:
    msg = "hi"
    msg += "!"
    send_email("bob@example.com", msg)

examples/email/cases/aug_assign_rewritten_fail.py

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

import clauz3


# The desugared form of aug_assign_fail.py: spelled `msg = msg + ...`, the
# same concatenation is refuted the same way. The pair pins that the `+=`
# handler (#109) proves exactly what its desugaring proves.
@clauz3.guarantee(emails.content_length_at_most(5))
def main() -> None:
    msg = "hi"
    msg = msg + " a much longer body than the contract allows"
    send_email("bob@example.com", msg)

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/bob_gets_x_one_line_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.bob_gets_x())
def main() -> None:
    send_email("bob@example.com", "y")

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

examples/email/cases/while_loop_skip.py

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

import clauz3


# `while` is outside the proved subset: neither the prover nor the
# interpreter registers a handler for `astroid.While`, so this program skips
# and `clauz3 run` refuses it before asking for approval. The loop is bounded
# and the guarantee holds; the skip is about the construct, not the content.
@clauz3.guarantee(emails.only(["bob@example.com"]))
def main() -> None:
    n = 0
    while n < 2:
        send_email("bob@example.com", "hi")
        n = n + 1