Trading — all cases¶

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

See the curated walk-through for the Dogwood policy these cases port and for what the port leaves behind.

`examples/trading/cases/approved_sale_pass.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals, sell_shares
from tools.trading.trusted.schemas import ApprovalRow


@clauz3.guarantee(trading.approvals_only_desk("equities"))
@clauz3.guarantee(trading.approvals_only_where({"approved": True}))
@clauz3.guarantee(trading.stock_from(ApprovalRow, "stock"))
@clauz3.guarantee(trading.shares_from(ApprovalRow, "shares"))
@clauz3.guarantee(trading.orders_at_most(50))
def main() -> None:
    for row in list_approvals("equities", where={"approved": True}):
        sell_shares(row.stock, row.shares)

`examples/trading/cases/literal_sale_fail.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import sell_shares
from tools.trading.trusted.schemas import ApprovalRow


@clauz3.guarantee(trading.stock_from(ApprovalRow, "stock"))
def main() -> None:
    sell_shares("ACME", 100)  # literal — no approval row backs this

`examples/trading/cases/no_sales_pass.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals


@clauz3.guarantee(trading.none())
def main() -> None:
    _rows = list_approvals("equities", where={"approved": True})  # read, don't trade

`examples/trading/cases/orders_too_tight_fail.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals, sell_shares
from tools.trading.trusted.schemas import ApprovalRow


@clauz3.guarantee(trading.stock_from(ApprovalRow, "stock"))
@clauz3.guarantee(trading.shares_from(ApprovalRow, "shares"))
@clauz3.guarantee(trading.orders_at_most(10))
def main() -> None:
    # The provenance clauses hold. The count does not: `list_approvals` is
    # capped at 50 rows, so the loop can place up to 50 orders. This is what
    # pins `orders_at_most` — without it, a vacuous count bound would still let
    # `approved_sale_pass.py` prove.
    for row in list_approvals("equities", where={"approved": True}):
        sell_shares(row.stock, row.shares)

`examples/trading/cases/quantity_mismatch_fail.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals, sell_shares
from tools.trading.trusted.schemas import ApprovalRow


@clauz3.guarantee(trading.stock_from(ApprovalRow, "stock"))
@clauz3.guarantee(trading.shares_from(ApprovalRow, "shares"))
def main() -> None:
    # The stock is approved; the quantity is the agent's own. This is the case
    # a stock-only gate would wave through.
    for row in list_approvals("equities", where={"approved": True}):
        sell_shares(row.stock, 500)

`examples/trading/cases/row_mixing_hole_pass.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals, sell_shares
from tools.trading.trusted.schemas import ApprovalRow


# A KNOWN, DOCUMENTED HOLE, kept as a case so it is a tested fact rather than a
# prose claim. See "Row mixing" in docs/examples/trading.md.
#
# `stock_from` and `shares_from` are independent clauses, and column-ref
# equality is a structural match on `<field>(Select(<approval array>, ?))` that
# ignores the index. So every stock sold is an approved stock, every quantity
# sold is an approved quantity, and they need not come from the same row: this
# sells row 0's approved quantity for *every* approved name.
#
# It proves today. If a future prover change adds row-identity binding, this
# case starts failing — which is the signal to close the hole in the docs, the
# README row, and the contracts module docstring in the same commit.
@clauz3.guarantee(trading.approvals_only_desk("equities"))
@clauz3.guarantee(trading.approvals_only_where({"approved": True}))
@clauz3.guarantee(trading.stock_from(ApprovalRow, "stock"))
@clauz3.guarantee(trading.shares_from(ApprovalRow, "shares"))
def main() -> None:
    rows = list_approvals("equities", where={"approved": True})
    for row in rows:
        sell_shares(row.stock, rows[0].shares)

`examples/trading/cases/sells_with_none_fail.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals, sell_shares


@clauz3.guarantee(trading.none())
def main() -> None:
    # Claims it places no orders, then places one per approval row. The
    # counterpart to `no_sales_pass.py`: together they pin `none()` in both
    # directions.
    for row in list_approvals("equities", where={"approved": True}):
        sell_shares(row.stock, row.shares)

`examples/trading/cases/trading_no_guarantees_pass.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import sell_shares


@clauz3.guarantee(trading.no_guarantees())
def main() -> None:
    # The explicit null contract. This sells an arbitrary stock in an arbitrary
    # quantity with no approval anywhere, and proves — because the agent is
    # openly asking for unconstrained trading authority rather than claiming a
    # gate it does not have. Weak, but not silent.
    sell_shares("ACME", 100)

`examples/trading/cases/unapproved_source_fail.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals, sell_shares
from tools.trading.trusted.schemas import ApprovalRow


@clauz3.guarantee(trading.approvals_only_where({"approved": True}))
@clauz3.guarantee(trading.stock_from(ApprovalRow, "stock"))
@clauz3.guarantee(trading.shares_from(ApprovalRow, "shares"))
def main() -> None:
    # Every *requested* sale, not every *approved* one — the rows this loop
    # sells from include the ones the desk turned down.
    for row in list_approvals("equities", where={"desk": "equities"}):
        sell_shares(row.stock, row.shares)

`examples/trading/cases/wrong_desk_fail.py`¶

# ruff: noqa
import clauz3
from tools.trading.trusted import contracts as trading
from tools.trading.trusted.effects import list_approvals, sell_shares
from tools.trading.trusted.schemas import ApprovalRow


@clauz3.guarantee(trading.approvals_only_desk("equities"))
@clauz3.guarantee(trading.stock_from(ApprovalRow, "stock"))
@clauz3.guarantee(trading.shares_from(ApprovalRow, "shares"))
def main() -> None:
    # Every order is backed by an approval — from another desk's record.
    for row in list_approvals("derivatives", where={"approved": True}):
        sell_shares(row.stock, row.shares)

Trading — all cases¶

examples/trading/cases/approved_sale_pass.py¶

examples/trading/cases/literal_sale_fail.py¶

examples/trading/cases/no_sales_pass.py¶

examples/trading/cases/orders_too_tight_fail.py¶

examples/trading/cases/quantity_mismatch_fail.py¶

examples/trading/cases/row_mixing_hole_pass.py¶

examples/trading/cases/sells_with_none_fail.py¶

examples/trading/cases/trading_no_guarantees_pass.py¶

examples/trading/cases/unapproved_source_fail.py¶

examples/trading/cases/wrong_desk_fail.py¶