Bank example

The bank example shows the relation algebra's numeric aggregation side. The trusted module exposes a single side-effecting withdraw(account, amount) function, and the contract vocabulary covers two domain predicates: max_spend(limit) (a sum over all withdrawals) and only_account(account) (a universal over the account field).

Trusted module

The trusted effect is a stub with a non-negativity precondition. The prover lifts that precondition into a proof obligation at every call site.

examples/bank/tools/bank/trusted/effects.py

import deal


@deal.pre(lambda account, amount: amount >= 0, message="amount must be non-negative")
@deal.has("trusted")
def withdraw(account: str, amount: int) -> None:
    """MOCK trusted withdrawal.

    Contract: amount must be non-negative.
    """
    pass


@deal.post(lambda result: result >= 0, message="balance must be non-negative")
@deal.has("bank_read")
def balance(account: str) -> int:
    """MOCK trusted balance lookup (amount outstanding on an account).

    Contract: the returned balance is non-negative.
    """
    return 0

Two contract helpers wrap the generic effect("withdraw") relation.

examples/bank/tools/bank/trusted/contracts.py

"""Bank predicates built from generic trusted effect facts."""

from clauz3.spec import ContractSpec, contract, effect

Withdraw = effect("withdraw")


@contract
def max_spend(limit: int) -> ContractSpec:
    """Guarantee that total withdrawals are at most limit."""
    return Withdraw.sum(lambda w: w.amount) <= limit


@contract
def only_account(account: str) -> ContractSpec:
    """Guarantee that every withdrawal targets this account."""
    return Withdraw.all(lambda w: w.account == account)

A passing case

The sum of two withdrawals is exactly the spending limit, so bank.max_spend(5) is discharged.

examples/bank/cases/max_spend_pass.py

# ruff: noqa: F821
from tools.bank.trusted import contracts as bank
from tools.bank.trusted.effects import withdraw

import clauz3


@clauz3.guarantee(bank.max_spend(5))
def main() -> None:
    withdraw("checking", 2)
    withdraw("checking", 3)

A failing case

Bumping one of the amounts above the limit causes the proof to fail.

examples/bank/cases/max_spend_fail.py

# ruff: noqa: F821
from tools.bank.trusted import contracts as bank
from tools.bank.trusted.effects import withdraw

import clauz3


@clauz3.guarantee(bank.max_spend(5))
def main() -> None:
    withdraw("checking", 2)
    withdraw("checking", 4)

All cases

Browse the full set on the all-cases page.

How they run

examples/bank/Justfile

trusted := "tools/bank/trusted"
effects := trusted + "/effects.py"
prove := "uv run clauz3 prove --trusted-root " + trusted

test: lint cases

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

cases: max-spend-pass max-spend-fail max-spend-branch-pass for-loop-sum-pass for-loop-sum-fail only-account-pass only-account-fail negative-amount-fail pay-bill-capped-pass pay-bill-uncapped-fail pay-bill-cap-too-tight-fail

max-spend-pass:
    {{prove}} cases/max_spend_pass.py

max-spend-fail:
    if {{prove}} cases/max_spend_fail.py; then exit 1; fi

max-spend-branch-pass:
    {{prove}} cases/max_spend_branch_pass.py

for-loop-sum-pass:
    {{prove}} cases/for_loop_sum_pass.py

for-loop-sum-fail:
    if {{prove}} cases/for_loop_sum_fail.py; then exit 1; fi

only-account-pass:
    {{prove}} cases/only_account_pass.py

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

negative-amount-fail:
    if {{prove}} cases/negative_amount_fail.py; then exit 1; fi

pay-bill-capped-pass:
    {{prove}} cases/pay_bill_capped_pass.py

pay-bill-uncapped-fail:
    if {{prove}} cases/pay_bill_uncapped_fail.py; then exit 1; fi

pay-bill-cap-too-tight-fail:
    if {{prove}} cases/pay_bill_cap_too_tight_fail.py; then exit 1; fi