Email example¶

The email example is the canonical worked case. The trusted module exposes one side-effecting function (send_email) and a small vocabulary of domain contracts (only, none, unique_recipients, content_length_at_most, same_content, no_guarantees). Agent code in cases/ uses @clauz3.guarantee(...) to express what should be true about the program's effects.

Trusted module¶

The trusted effect is just a stub function decorated with @deal.has(...) and a precondition.

examples/email/tools/email/trusted/effects.py

import deal


@deal.pre(lambda addr, msg: "@" in addr, message='addr must contain "@"')
@deal.has("trusted")
def send_email(addr: str, msg: str) -> None:
    """trusted email sender.

    Note: this is a mock function for testing, it won't *actually* send an email

    Arguments:
      addr: recipient. Must be a valid email address
      msg: body of email
    """
    pass

The contract module defines the domain vocabulary on top of the generic effect("send_email") relation.

examples/email/tools/email/trusted/contracts.py

"""Email-specific predicates built from generic trusted effect facts."""

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

Email = effect("send_email")


@contract
def only(addresses: list[str]) -> ContractSpec:
    """Guarantee that every sent email targets one of these addresses."""
    return Email.all(lambda e: e.addr in addresses)


@contract
def none() -> ContractSpec:
    """Guarantee that no email is sent."""
    return Email.empty()


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


@contract
def unique_recipients() -> ContractSpec:
    """Guarantee that no reachable execution emails the same address twice."""
    return Email.distinct(lambda e: e.addr)


@contract
def at_most(count: int) -> ContractSpec:
    """Guarantee that at most count emails are sent."""
    return Email.count() <= count


@contract
def recipient_at_most(addr: str, count: int) -> ContractSpec:
    """Guarantee that addr is emailed at most count times."""
    return Email.where(lambda e: e.addr == addr).count() <= count


@contract
def content_length_at_most(max_chars: int) -> ContractSpec:
    """Guarantee that no sent email content is longer than max_chars."""
    return Email.all(lambda e: len(e.msg) <= max_chars)


@contract
def same_content(left_addr: str, right_addr: str) -> ContractSpec:
    """Guarantee that both addresses receive at least one identical message."""
    left_emails = Email.where(lambda e: e.addr == left_addr)
    right_emails = Email.where(lambda e: e.addr == right_addr)
    return left_emails.shares_value(right_emails, lambda e: e.msg)

A passing case¶

Sending one email to an allow-listed address discharges emails.only([...]).

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

A failing case¶

The same guarantee with a non-allow-listed recipient is rejected by the prover.

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

The runtime layer (deal as a backstop)¶

The static prover is only the first layer. The @deal.pre on send_email (addr must contain "@") is also a runtime contract. The two layers act on the same artifact at different times.

Statically, precondition_fail.py is rejected by the prover before anything runs, because it cannot discharge that precondition for the call below:

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

The same precondition is what deal enforces at runtime. If the program is run outside a successful proof — a weak or no_guarantees() contract, or runtime-only mode — deal still raises on the bad call at the trusted boundary:

>>> from tools.email.trusted.effects import send_email
>>> send_email("bob@example.com", "hi")        # precondition holds: runs
>>> send_email("not-an-email", "hi")           # precondition violated
deal.PreContractError: addr must contain "@" (where addr='not-an-email', msg='hi')

Same check, different time: the prover discharges it ahead of execution, deal enforces it at execution. See Concepts: static proof vs runtime.

All cases¶

Every file under cases/ is a small program plus its declared guarantee. Cases with _pass suffix should prove; cases with _fail should be rejected. Browse the full set on the all-cases page.

How they run¶

The example Justfile invokes clauz3 prove against each case. _fail cases are wrapped so a non-zero exit is the expected outcome.

examples/email/Justfile

trusted := "tools/email/trusted"
effects := trusted + "/effects.py"
prove := "uv run clauz3 prove --trusted-root " + trusted
policy-check := "uv run clauz3 policy-check --policy approval-policy.json --trusted-root " + trusted + " --import-root ."

test: lint cases policy

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

cases: only-bob-pass only-bob-fail none-pass none-fail no-guarantees-pass helper-pass helper-fail precondition-fail dead-branch-pass unique-recipients-pass unique-recipients-fail unique-recipients-branch-pass nobody-emailed-twice-fail at-most-two-pass at-most-two-fail bob-at-most-two-pass bob-at-most-two-fail bob-at-most-two-branch-pass content-length-pass content-length-fail content-length-branch-pass same-content-pass same-content-fail same-content-branch-pass

policy: policy-auto-pass policy-auto-reject policy-ask

policy-auto-pass:
    {{policy-check}} --expect auto_approved cases/only_bob_pass.py

policy-auto-reject:
    {{policy-check}} --expect auto_rejected cases/policy_reject.py

policy-ask:
    {{policy-check}} --expect ask cases/policy_ask.py

only-bob-pass:
    {{prove}} cases/only_bob_pass.py

only-bob-fail:
    if {{prove}} cases/only_bob_fail.py; then exit 1; fi

none-pass:
    {{prove}} cases/none_pass.py

none-fail:
    if {{prove}} cases/none_fail.py; then exit 1; fi

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

helper-pass:
    {{prove}} cases/helper_pass.py

helper-fail:
    if {{prove}} cases/helper_fail.py; then exit 1; fi

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

dead-branch-pass:
    {{prove}} cases/dead_branch_pass.py

unique-recipients-pass:
    {{prove}} cases/unique_recipients_pass.py

unique-recipients-fail:
    if {{prove}} cases/unique_recipients_fail.py; then exit 1; fi

unique-recipients-branch-pass:
    {{prove}} cases/unique_recipients_branch_pass.py

nobody-emailed-twice-fail:
    if {{prove}} cases/nobody_emailed_twice_fail.py; then exit 1; fi

at-most-two-pass:
    {{prove}} cases/at_most_two_pass.py

at-most-two-fail:
    if {{prove}} cases/at_most_two_fail.py; then exit 1; fi

bob-at-most-two-pass:
    {{prove}} cases/bob_at_most_two_pass.py

bob-at-most-two-fail:
    if {{prove}} cases/bob_at_most_two_fail.py; then exit 1; fi

bob-at-most-two-branch-pass:
    {{prove}} cases/bob_at_most_two_branch_pass.py

content-length-pass:
    {{prove}} cases/content_length_pass.py

content-length-fail:
    if {{prove}} cases/content_length_fail.py; then exit 1; fi

content-length-branch-pass:
    {{prove}} cases/content_length_branch_pass.py

same-content-pass:
    {{prove}} cases/same_content_pass.py

same-content-fail:
    if {{prove}} cases/same_content_fail.py; then exit 1; fi

same-content-branch-pass:
    {{prove}} cases/same_content_branch_pass.py

case1: only-bob-pass

case1-fail: only-bob-fail