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 decorated with @clauz3.trusted and a @clauz3.requires(...) non-negativity precondition. The prover lifts that precondition into a proof obligation at every call site.

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

import clauz3


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

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


@clauz3.ensures(lambda result: result >= 0, message="balance must be non-negative")
@clauz3.trusted
@clauz3.mock
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 effect(withdraw), the relation for calls to the imported trusted function.

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

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

from tools.bank.trusted.effects import withdraw

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

test: lint cases

lint:
    uv run clauz3 lint {{trusted}}/effects.py

cases:
    {{prove-cases}} cases/*_pass.py cases/*_fail.py