> For the complete documentation index, see [llms.txt](https://docs.moduluszk.io/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.moduluszk.io/predicates-in-practice.md).

# Predicates in practice

### A market and a loan

The two pages before this one describe the model. This page shows it working, by rendering two familiar designs as predicates: a constant-product market of the kind Uniswap popularised, and an over-collateralised lending pool of the kind Aave popularised. The renderings are written for this model and for reading; they are illustrations of those designs, never descriptions of those protocols' deployed contracts, which differ in detail. 

Four ground rules first. The formulas are standard first-order notation over the transition: the state consumed, the state produced, and the values the transaction presents; every value a formula mentions is presented by the transaction itself, so the sentences are checked as given, which is exactly the model of the proofs page. The illustrations assume the chain's base accounting: quantities are non-negative, reserve and cash fields denote value the record itself holds, and every asset balances across a transaction, so a predicate states an application's policy on top of that accounting rather than restating it. Three things stand in for designs that are open on purpose: an oracle price, with price > 0, for the open read-primitive question; an elapsed time Δτ ≥ 0, for the open transaction-context surface; and the successor link, each produced pool or position record standing under the same predicate as the record it succeeds, for the covenant question named on the predicates page. The predicates take all three as given and are agnostic to how each arrives. And everything below uses arithmetic, order, and equality, relations the language ships today: the comparisons <, >, ≤, ≥ and ≠ are goals that compile into the predicate as committed slack, non-negativity ships as natural, and mod and all\_distinct ship alongside them. One relation is abstract: authorised, whose concrete built-in form is the open surface item named on the predicates page. The placeholder standing in for it today asserts only that an owner is named, so nothing on this page should read as though the draw is authenticated.