Email-from-DB — all cases

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

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

examples/email-from-db/cases/all_trivial_loop_pass.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email


@clauz3.guarantee(contracts.at_most(100))
def main() -> None:
    for row in db_query("users"):
        send_email(row.email, "hi")

examples/email-from-db/cases/count_pass.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email


@clauz3.guarantee(contracts.count_at_most(100))
def main() -> None:
    for row in db_query("users"):
        send_email(row.email, "Hello!")

examples/email-from-db/cases/count_too_tight_fail.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email


@clauz3.guarantee(
    contracts.count_at_most(10)
)  # too tight; db_query can return up to 100
def main() -> None:
    for row in db_query("users"):
        send_email(row.email, "hi")

examples/email-from-db/cases/email_loop_fail.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email


@clauz3.guarantee(contracts.none())
def main() -> None:
    for row in db_query("users"):
        send_email(row.email, "hi")

examples/email-from-db/cases/literal_address_fail.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import send_email
from tools.db.trusted.schemas import UserRow


@clauz3.guarantee(contracts.addresses_from(UserRow, "email"))
def main() -> None:
    send_email("admin@example.com", "manual")  # literal, not from query

examples/email-from-db/cases/mixed_source_fail.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email
from tools.db.trusted.schemas import UserRow


@clauz3.guarantee(contracts.addresses_from(UserRow, "email"))
def main() -> None:
    send_email("admin@example.com", "manual")  # literal — should fail
    for row in db_query("users"):
        send_email(row.email, "newsletter")

examples/email-from-db/cases/newsletter_pass.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email
from tools.db.trusted.schemas import UserRow


@clauz3.guarantee(contracts.addresses_from(UserRow, "email"))
@clauz3.guarantee(contracts.count_at_most(100))
def main() -> None:
    for row in db_query("users", where={"consented": True}):
        send_email(row.email, "Newsletter is out!")

examples/email-from-db/cases/no_emails_with_loop_pass.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query


@clauz3.guarantee(contracts.none())
def main() -> None:
    _rows = db_query("users")  # query but don't email

examples/email-from-db/cases/unique_recipients_loop_fail.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email


@clauz3.guarantee(contracts.unique_recipients())
def main() -> None:
    for row in db_query("users"):
        send_email(row.email, "hi")

examples/email-from-db/cases/wrong_column_fail.py

# ruff: noqa
import clauz3
from tools.db.trusted import contracts
from tools.db.trusted.effects import db_query, send_email
from tools.db.trusted.schemas import UserRow


@clauz3.guarantee(contracts.addresses_from(UserRow, "email"))
def main() -> None:
    for row in db_query("users"):
        send_email(row.name, "hi")  # name, not email — wrong column!