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 a stub function decorated with @clauz3.trusted. Its @clauz3.requires(...) precondition is an obligation at every call site.

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

import clauz3


@clauz3.requires(lambda addr, msg: "@" in addr, message='addr must contain "@"')
@clauz3.trusted
@clauz3.mock
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 effect(send_email) relation, passing the imported trusted function directly. The string form effect("send_email") also names this effect.

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

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

from tools.email.trusted.effects import send_email

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)


@contract
def bob_gets_x() -> ContractSpec:
    """Bob only ever receives the message "x".

    Deliberately written on one line: two relation lambdas sharing a physical
    line used to compile to the same body (gh-125), so this is the fixture for
    the end-to-end regression in ``tests/test_email_prover.py``.
    """
    # fmt: off
    return Email.where(lambda e: e.addr == "bob@example.com").all(lambda e: e.msg == "x")  # noqa: E501
    # fmt: on

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

Of course, this case is trivial. The contract is somewhat superfluous here as it's easy for a person to see the one-line main() function and infer it only emails the one person. But it serves to illustrate the simplest case where a user need only read the contract and not the program.

In a real world scenario, the agent may author a more complex program that is harder for a person to quickly reason over.

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

The static prover is only the first layer. The @clauz3.requires on send_email (addr must contain "@") is also a runtime check. 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")

Choosing no_guarantees() removes the email-effect guarantee; it does not remove preconditions. The prover still rejects a call whose address lacks "@". The same precondition is also enforced at runtime, including when the trusted function is called directly without a proof:

>>> 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
PreContractError: addr must contain "@" (where addr='not-an-email', msg='hi')

Same check, different time: the prover discharges it ahead of execution, the boundary 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"
prove := "uv run clauz3 prove --trusted-root " + trusted
# Proves each case in one process: *_pass.py must prove, *_fail.py must not.
prove-cases := "uv run python -m clauz3._prove_cases --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 clauz3 lint {{trusted}}/effects.py

# alias_import_fail.py:
#   Issue #129: the guarantee is spelled through an import alias. Before the fix
#   the decorator was dropped and this printed "proved!".
cases: while-loop-skip aug-assign-fail aug-assign-rewritten-fail
    {{prove-cases}} cases/*_pass.py cases/*_fail.py

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

case1:
    {{prove}} cases/only_bob_pass.py

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

# Distinguish unsupported syntax from a refuted guarantee.
while-loop-skip:
    out=$({{prove}} cases/while_loop_skip.py 2>&1); status=$?; echo "$out"; test $status -ne 0 && echo "$out" | grep -qF "main: skipped unsupported program body"

# `+=` on a str is proved like its desugaring: a refuted guarantee, not a skip.
aug-assign-fail:
    out=$({{prove}} cases/aug_assign_fail.py 2>&1); status=$?; echo "$out"; test $status -ne 0 && echo "$out" | grep -qF "main: failed guarantee"

aug-assign-rewritten-fail:
    out=$({{prove}} cases/aug_assign_rewritten_fail.py 2>&1); status=$?; echo "$out"; test $status -ne 0 && echo "$out" | grep -qF "main: failed guarantee"