Bank — all cases

Every case file under examples/bank/cases/, inlined. _pass cases prove; _fail cases are refuted. Exact conclusions are pinned in tests/test_bank_prover.py.

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

examples/bank/cases/aug_assign_loop_fail.py

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

import clauz3


# Same accumulator as aug_assign_loop_pass.py; the cap is 10 too tight.
@clauz3.guarantee(bank.max_spend(90))
def main() -> None:
    amount = 0
    for _ in range(4):
        amount += 10
        withdraw("checking", amount)

examples/bank/cases/aug_assign_loop_pass.py

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

import clauz3


# `amount` is 10, 20, 30, 40 across the unrolled loop, so the withdrawals
# total exactly 100. `range(4)` is unrolled, so the accumulator is modelled
# per iteration; over trusted query results the same body is refused.
@clauz3.guarantee(bank.max_spend(100))
def main() -> None:
    amount = 0
    for _ in range(4):
        amount += 10
        withdraw("checking", amount)

examples/bank/cases/for_loop_sum_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(40))
def main() -> None:
    """withdraw in 5 increments, $10 each time"""
    for _ in range(5):
        withdraw("checking", 10)

examples/bank/cases/for_loop_sum_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(100))
def main() -> None:
    for _ in range(5):
        withdraw("checking", 10)

examples/bank/cases/max_spend_branch_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(use_savings: bool) -> None:
    """withdraw $5 from savings or checking"""
    if use_savings:
        withdraw("savings", 5)
    else:
        withdraw("checking", 5)

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)

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)

examples/bank/cases/negative_amount_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", -1)

examples/bank/cases/only_account_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.only_account("checking"))
def main() -> None:
    withdraw("savings", 1)

examples/bank/cases/only_account_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.only_account("checking"))
def main() -> None:
    withdraw("checking", 1)
    withdraw("checking", 2)

examples/bank/cases/pay_bill_cap_too_tight_fail.py

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

import clauz3


@clauz3.guarantee(bank.max_spend(499))
def main() -> None:
    owed = balance("card")
    if owed > 500:
        withdraw("card", 500)  # code can spend 500, tighter than the declared 499
    else:
        withdraw("card", owed)

examples/bank/cases/pay_bill_capped_pass.py

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

import clauz3


@clauz3.guarantee(bank.max_spend(500))
@clauz3.guarantee(bank.only_account("card"))
def main() -> None:
    owed = balance("card")
    if owed > 500:
        withdraw("card", 500)
    else:
        withdraw("card", owed)

examples/bank/cases/pay_bill_uncapped_fail.py

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

import clauz3


@clauz3.guarantee(bank.max_spend(500))
def main() -> None:
    owed = balance("card")
    withdraw("card", owed)  # no cap: a large outstanding balance overspends