Bank — all cases

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

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

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