> 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/an-over-collaterallised-loan.md). # An over-collaterallised loan The lending pool is a market record with a cash field C, and a position record with fields col for collateral posted and d for debt owed. Parameters arrive as rational constants written with explicit numerators and denominators so that every formula stays over the integers: a loan-to value limit c\_n/c\_d, a liquidation threshold t\_n/t\_d with c\_n·t\_d ≤ t\_n·c\_d so the threshold sits at or above the borrowing limit, and a liquidation bonus b\_n/b\_d. The transaction presents the price of one collateral unit in the debt asset, scaled by a unit q, and the elapsed time Δτ since the position was last touched; both are the assumption-level inputs of the ground rules. Interest first, because it shows a pattern. Whitepapers write compound interest as an exponential. Deployed systems update state whenever a position is touched, and compounding emerges from touch composing with touch. The per-touch accrual at rate r per second, in unit u, is the pair of inequalities

u·(d_acc − d) ≤ d·r·Δτ ∧ d·r·Δτ < u·(d_acc − d) + u

which is d\_acc = d + ⌊d·r·Δτ/u⌋ written without a division symbol; even the rounding is two comparisons. Every touch below conjoins this pair first, and d\_acc names the debt after it. Production pools run many borrowers off one shared accrual index that every position reads, storing index-scaled debt, which keeps every aggregate a field updated per transition and keeps totals and positions rounding-consistent; that is the accumulator pattern, and it is why no formula here ever sums over all users. This page keeps one market and one borrower so that every line stays checkable at sight. Borrowing an amount Δ against the accrued position:

Δ > 0 ∧ d' = d_acc + Δ ∧ C' = C − Δ

col' = col ∧ owner' = owner

c_d·q·d' ≤ c_n·price·col

authorised(tx, owner)

The safety inequality is the entire policy: the debt after the draw stays within the loan-to-value fraction of the collateral's value, cross-multiplied so that only integers appear. A borrower, an auditor, and a regulator read the same inequality. The identity line carries the frame conditions, stated rather than assumed, the same discipline as the funded-pool guard. Cash sufficiency is one conjunct, C' ≥ 0. Under a base accounting that holds every quantity non-negative it is implied rather than stated, and a predicate written against the language today states it, in the same spirit as the funded-pool guard: the condition sits where reading finds it. Repayment mirrors the draw, reducing d and raising C, and withdrawing collateral re-checks the same safety inequality against the reduced col. Liquidation is where the model shows its teeth. Eligibility is the threshold inequality flipping:

t_d·q·d_acc > t_n·price·col

and when it holds, anyone may repay a part ρ of the debt and seize collateral at the stated bonus:

0 < ρ ∧ 0 < seize ∧ 2·ρ ≤ d_acc ∧ seize ≤ col ∧ b_d·seize·price ≤ (b_d + b_n)·ρ·q

d' = d_acc − ρ ∧ col' = col − seize ∧ C' = C + ρ ∧ owner' = owner

No authorisation from the position's owner appears, on purpose: permissionless liquidation is a property of the sentence, granted by the eligibility inequality itself rather than by a keeper whitelist. The close factor is the single term 2·ρ ≤ d\_acc, and the bonus is one cross-multiplied bound on what may be seized. The lower bound on seize is the same discipline as the lower bound on ρ: reserve and cash fields are held non-negative by the ground rules, but seize is a value the transaction presents, so it earns its own conjunct, and without it the under-constrained transition is admitted rather than unprovable. Refusal semantics does quiet work here too: a liquidation attempt against a healthy position is unprovable, so it never reaches the chain, never costs a failed transaction, and never needs a code path to reject it. What no predicate can supply, on this chain or any other, is the liquidators themselves; whether they show up is an incentive question, and what the sentence enforces is that when they do, only eligible positions can be touched and only on the stated terms.