Trading example (a Dogwood approval gate, ported)

This example ports one scenario from Dogwood — AWS's temporal extension to Cedar — into clauz3, to see what survives the translation and what does not.

Dogwood's headline example is an approval gate on share sales:

permit ( principal, action == AgentCore::Action::"SellShares", resource )
when temporal {
    formerly within 1h AgentCore::Action::"ApproveSale"::response{
        input.stock:     context.input.stock,
        input.shares:    context.input.shares,
        output.approved: true
    }
};

Read it as four separate requirements, because they port very differently:

Clause	What it demands	Ports to clauz3?
ApproveSale::response exists	the sale is backed by an approval	yes — as provenance
output.approved: true	it was granted, not merely requested	yes — as a source filter
input.stock / input.shares match	the approval was for this sale	partly — as column binding, per argument but not per row
within 1h	the approval is fresh	no

The first three are questions about where a value came from. clauz3 answers those from the program text alone. The fourth is a question about when something happened, and there is nothing in a program to answer it with.

The trusted module

Two capabilities, neither of them starved. The agent may read the desk's approval record with any filter, and may sell any stock in any quantity.

examples/trading/tools/trading/trusted/effects.py

"""Trusted effects for a trading-desk agent.

This layer is the clauz3 side of a port of Dogwood's approval-gate policy
(see ``docs/examples/trading.md``). Dogwood permits ``SellShares`` only when a
matching ``ApproveSale`` *response* is found in the last hour of event history.
Here there is no event history: the agent may read the approval record and may
place orders, and the gate is a contract pinning every order's arguments to a
row of that record.

Neither capability is withheld to make the agent safe. ``list_approvals`` can
read any desk's approvals with any filter, and ``sell_shares`` can sell any
stock in any quantity. Safety comes from the contracts in ``contracts.py``.
"""

from tools.trading.trusted.schemas import ApprovalRow

import clauz3


@clauz3.trusted
@clauz3.ensures(lambda result: len(result) <= 50)
def list_approvals(desk: str, where: dict[str, object]) -> list[ApprovalRow]:
    """MOCK: return the desk's sale approvals, filtered by ``where``.

    The prover never runs this body. It records a ``list_approvals`` fact whose
    fields are ``desk`` and ``where``, and materializes a symbolic
    ``list[ApprovalRow]`` so a for-loop over the result can be reasoned about.
    The ``@deal.post`` length cap is what bounds that loop.
    """
    return []


@clauz3.trusted
def sell_shares(stock: str, shares: int) -> None:
    """MOCK: place a sell order.

    Real capability, deliberately unrestricted at the function level. *Which*
    stock and *how many* shares are contract questions, answered by
    ``stock_from`` and ``shares_from``.
    """
    pass

list_approvals's @clauz3.ensures length cap is what lets the prover bound the loop over its result. The schema's fields become the row shape the prover binds against — note that rows exist for rejected requests too, which is what makes the query filter load-bearing rather than decorative:

examples/trading/tools/trading/trusted/schemas.py

import clauz3


class ApprovalRow(clauz3.Row):
    """A sale approval recorded by the trading desk's approval system.

    ``approved`` is the desk's decision. Rows exist for rejected requests too,
    which is why the ``where`` filter on a query is load-bearing.
    """

    stock: str
    shares: int
    approver: str
    approved: bool

The contracts are the gate. approvals_only_desk and approvals_only_where pin the source, stock_from and shares_from pin the data flow:

examples/trading/tools/trading/trusted/contracts.py

"""Approval-gate contracts for the trading-desk example.

These are the clauz3 rendering of Dogwood's approval-gate policy:

    permit ( principal, action == AgentCore::Action::"SellShares", resource )
    when temporal {
        formerly within 1h AgentCore::Action::"ApproveSale"::response{
            input.stock:     context.input.stock,
            input.shares:    context.input.shares,
            output.approved: true
        }
    };

Dogwood asks whether a matching approval *event* occurred recently.
These contracts ask a question with no time in it: does every order's
argument provably *come from* an approved row?

- ``approvals_only_where`` constrains the **source**: every approval query must
  carry a specific filter, which is where ``output.approved: true`` lands.
- ``stock_from`` and ``shares_from`` constrain the **data flow**: the values
  handed to ``sell_shares`` must symbolically be columns of a queried approval
  row -- not literals the agent typed, and not a quantity of its own choosing.

  These are two independent clauses, and each pins its argument to *some*
  approved row rather than to a common one. Column-ref equality is a
  structural match on ``<field>(Select(<approval array>, ?))`` that ignores the
  index, so ``sell_shares(row.stock, rows[0].shares)`` satisfies both while
  mixing rows. That is weaker than Dogwood's
  ``formerly ... {input.stock: ..., input.shares: ...}``, which matches one
  event. Row-correlated binding needs row identity the prover does not carry
  today; see ``docs/examples/trading.md``.

What has no rendering here is ``within 1h``. See ``docs/examples/trading.md``.
"""

from tools.trading.trusted.effects import list_approvals, sell_shares

from clauz3.spec import ContractSpec, contract, effect
from clauz3.spec import no_guarantees as core_no_guarantees

Approvals = effect(list_approvals)
Sell = effect(sell_shares)


@contract
def approvals_only_where(filter_dict: dict[str, object]) -> ContractSpec:
    """Guarantee every ``list_approvals`` query uses exactly this filter.

    Source provenance: it fixes which approval rows may enter the plan at all.
    A query that omits ``{"approved": True}`` reads rejected requests too.
    """
    return Approvals.all(lambda e: e.where == filter_dict)


@contract
def approvals_only_desk(desk: str) -> ContractSpec:
    """Guarantee every ``list_approvals`` query reads this desk's record.

    The quoted Dogwood policy does not scope the desk either, but unlike the
    holes in the walk-through this one is closable with an ordinary provenance
    clause, so it is closed rather than caveated.
    """
    return Approvals.all(lambda e: e.desk == desk)


@contract
def stock_from(schema: type, field: str) -> ContractSpec:
    """Guarantee every sold stock is ``schema``.``field`` of a queried approval."""
    column = getattr(schema, field)
    return Sell.all(lambda e: e.stock == column)


@contract
def shares_from(schema: type, field: str) -> ContractSpec:
    """Guarantee every sold quantity is ``schema``.``field`` of a queried approval.

    This is the half that catches "approved to sell 10, sold 500". Pinning the
    stock alone is not the policy Dogwood writes.
    """
    column = getattr(schema, field)
    return Sell.all(lambda e: e.shares == column)


@contract
def orders_at_most(n: int) -> ContractSpec:
    """Guarantee at most n sell orders are placed."""
    return Sell.count() <= n


@contract
def none() -> ContractSpec:
    """Guarantee no sell order is placed."""
    return Sell.empty()


@contract
def no_guarantees() -> ContractSpec:
    """Make no guarantees about trading effects."""
    return core_no_guarantees()

The passing cases

The agent queries its own desk's approved sales and places exactly the approved order for each one. All five guarantees discharge on every branch, before any order is placed:

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)

Two more programs prove, for different reasons. no_sales_pass.py reads the approval record and trades nothing, discharging none() — the read effect is uncovered, but a query is not an order:

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

And trading_no_guarantees_pass.py sells an unapproved stock with the explicit null contract. It proves, because the agent is openly asking for unconstrained trading authority rather than claiming a gate it does not have. That is the point of no_guarantees(): it is semantically the same as saying nothing, and visibly different from it.

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)

The failing cases

Each one violates a different clause of the Dogwood policy.

No approval at all. A literal order isn't the column of any queried row, so stock_from fails. This is Dogwood's "no matching ApproveSale::response."

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

Approval requested, not granted. The loop is honest — every order does come from an approval row — but the query pulled every request, including the ones the desk turned down. approvals_only_where fails. This is output.approved: true.

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)

Right stock, wrong quantity. Approved to sell whatever the desk signed off on; sells 500. stock_from still holds, and shares_from fails. This is input.shares: context.input.shares, and it is the case a stock-only gate waves through:

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)

Another desk's approvals. Every order is backed by a genuine approval, from a record this program has no business reading. approvals_only_desk fails:

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)

Two more failing cases exist to pin the aggregate contracts rather than to illustrate a Dogwood clause. orders_too_tight_fail.py asserts orders_at_most(10) over the same 50-bounded loop, and sells_with_none_fail.py asserts none() while placing orders. Without them, a count contract that degenerated to a trivially-true bound would still let approved_sale_pass.py prove and nothing in the suite would notice.

What did not port, and why it matters

within 1h has no rendering here, and neither does anything else that needs history. Four concrete holes remain open in the clauz3 version:

• Row mixing. This is the one that is not about time, and the one a reader is most likely to assume is closed. stock_from and shares_from are independent clauses, and each pins its argument to some approved row, not to a common one. Column-ref equality is a structural match on <field>(Select(<approval array>, ?)) that ignores the index, so:

for row in rows:
    sell_shares(row.stock, rows[0].shares)

proves, and sells row 0's approved quantity for every approved stock — a desk approval of 10,000 shares of a penny stock authorises 10,000 shares of every other approved name. Dogwood's formerly ... {input.stock: ..., input.shares: ...} matches a single event and denies this. Closing it needs row-identity binding the prover does not carry today.

This one is not left as prose. cases/row_mixing_hole_pass.py is the program above, wired into the suite as a passing case, so the hole is a tested fact: if a future prover change closes it, that case starts failing and forces this section, the README row, and the contracts docstring to be updated in the same commit. - Staleness. An approval granted last year is as good as one granted a minute ago. - Reuse. Nothing stops the same approval row from backing a sale on every run, forever. Dogwood's window bounds reuse as a side effect of bounding recency; provenance does not. - Cross-run volume. orders_at_most(50) bounds this program. Five proved programs place 250 orders.

These are not incidental gaps — they are the class of property that is only answerable from an event log, and they are exactly what Dogwood is for.

Why the trade is not obviously in Dogwood's favour

The temptation is to read the table above as "Dogwood does more." It says something narrower: Dogwood asks more, and pays for it in what it must be able to trust.

To decide formerly within 1h, the monitor needs an event history that is:

• complete — every relevant tool call reached the gateway. A sub-agent with its own tool surface, a direct SDK call, or a second harness is invisible, and an invisible ApproveSale doesn't cause a false deny, it causes the sale to be denied while an invisible sale isn't seen at all.
• consistently ordered and timestamped — metric windows need clock agreement across whoever produced the events. Dogwood's own roadmap lists absolute-time windows as future work.
• correctly scoped — whose hour is it? In a multi-agent ensemble, an approval granted to agent A being consumed by agent B is either the feature or the vulnerability, and the language has to be told which. Multi-agent orchestration is likewise on the roadmap rather than in the language.
• authentic and durable — Dogwood's README is explicit that the reference interpreter addresses none of event authentication, timestamp integrity, or trace durability.

That is a substantial environment contract, and it grows with the number of moving pieces in the system. The clauz3 gate needs the trusted layer to be honest and the prover to be correct; both are in front of you at proof time, and neither gets harder when a second agent joins.

So the honest summary is not that one subsumes the other. It is that this example converts a temporal question into a provenance question, and provenance is answerable from the artifact in hand:

	Dogwood's gate	This example's gate
Question	did a matching approval event occur recently?	does every order's argument come from an approved row?
Evidence	the session's event log	the program text
Must trust	gateway completeness, clocks, scoping, log integrity	the trusted layer, the prover
Decides	per call, mid-run	once, before any order
Catches staleness and reuse	yes	no
Degrades with system complexity	yes	no

Both halves are worth having, and the composition — proving the contract, then metering the proved bound against a windowed budget at approval time — is sketched in Background.

All cases

Browse the full set on the all-cases page.

How they run

examples/trading/Justfile

trading_trusted := "tools/trading/trusted"
prove := "uv run clauz3 prove --trusted-root " + trading_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 " + trading_trusted

test: lint cases

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

# row_mixing_hole_pass.py:
#   A documented hole, pinned so it is a tested fact rather than a prose claim.
#   If this starts failing, the prover gained row-identity binding: close the
#   "Row mixing" bullet in docs/examples/trading.md, the README row, and the
#   contracts module docstring in the same commit.
cases:
    {{prove-cases}} cases/*_pass.py cases/*_fail.py