Example: checkout
The third worked example (spec §18.3). A payment endpoint across four modules, with a sealed type as evidence of authentication, an asserted claim, a policy on assumptions, and the path report the home page renders.
auth.AuthedCustomer is pub sealed: readable anywhere, constructible only inside app.auth, and the only producer is auth.require, so any function demanding one is callable only after a successful check. Idempotent is an asserted claim: it propagates like an effect, and each place it is assumed is recorded with a justification. The path passes with three assumptions, of which exactly one is outside the project — the payment vendor’s — and the policy names it. That assumption carries a verify block, and test_env.onus is the test module that supplies the fake capabilities onus test --assumptions runs it against.
examples/checkout/checkout.onus
module checkout
import std.sql
import std.io
import app.auth
import app.contracts
import vendor.payments
record Request {
caller: Text
customer: Text
idempotency_key: Text
}
record Order {
customer: Text
amount_pence: Int where it >= 0
}
record Basket {
items: List[Order]
total: Int where it >= 0
}
-- auth.AuthedCustomer is `pub sealed` (§3.10): readable anywhere, constructible only inside app.auth.
-- The only producer is auth.require, so any function demanding one is callable only after a successful auth check.
pub fn recent_orders(
db: sql.Db[ReadOnly, schema: "orders"],
who: auth.AuthedCustomer
) -> Result[List[Order], sql.Error] may sql.read, alloc {
-- ensures forall o: Order in result: o.customer == who.id
-- is proved from the statement's where clause once parse_select returns a Spec (§18.3); deferred.
let stmt: sql.Select[Order] = sql.select[
text: "select * from orders where customer_id = $1 order by created desc limit 50"
](params: [sql.text(x: who.id)], row: Order)
return sql.query(db: db, statement: stmt)
}
fn load_basket(
db: sql.Db[ReadOnly],
who: auth.AuthedCustomer
) -> Result[Basket, sql.Error] may sql.read, alloc
claims Idempotent
{
assume Idempotent "A select reads only; it has no observable effect."
let stmt: sql.Select[Order] = sql.select[text: "select * from baskets where customer_id = $1"](
params: [sql.text(x: who.id)],
row: Order
)
let items: List[Order] = try sql.query(db: db, statement: stmt)
return Ok(value: Basket { items: items, total: 0 })
}
fn record_order(
db: sql.Db[ReadWrite, schema: "orders"],
who: auth.AuthedCustomer,
basket: Basket,
receipt: payments.Receipt
) -> Result[Unit, sql.Error] may sql.write, alloc
claims Idempotent
{
assume Idempotent "The insert is `on conflict (receipt_id) do nothing`."
let stmt: sql.Statement = sql.statement[
text: "insert into orders (customer_id, receipt_id, amount_pence) values ($1, $2, $3) on conflict (receipt_id) do nothing"
](params: [sql.text(x: who.id), sql.text(x: receipt.id), sql.int(x: basket.total)])
return sql.execute(db: db, statement: stmt)
}
union CheckoutError =
| Unauthorised of detail: auth.Error
| Storage of detail: sql.Error
| Payment of detail: payments.Error
| Empty
pub fn handle_checkout(
req: Request,
clock: io.Clock,
db: sql.Db[ReadWrite, schema: "orders"],
pay: payments.Client,
auth: auth.Service
) -> Result[payments.Receipt, CheckoutError] may sql.read, sql.write, io.net, io.clock, alloc
claims Idempotent
{
let who: auth.AuthedCustomer = try auth.require(
service: auth,
caller: req.caller,
customer: req.customer,
clock: clock
) else e: Unauthorised(detail: e)
let basket: Basket = try load_basket(db: sql.narrow(db: db, to: ReadOnly), who: who)
else e: Storage(detail: e)
if List.is_empty(xs: basket.items) {
return Err(error: Empty)
}
let receipt: payments.Receipt = try payments.charge(
client: pay,
key: req.idempotency_key,
amount: basket.total,
who: who
) else e: Payment(detail: e)
try record_order(db: db, who: who, basket: basket, receipt: receipt) else e: Storage(detail: e)
return Ok(value: receipt)
}
policy no_third_party_assumes
forbid assume outside { self, std.* }
path checkout
entry handle_checkout
effects <= { sql.read, sql.write, io.net, io.clock, alloc }
require { Idempotent }
policy no_third_party_assumes except { vendor.payments.charge }examples/checkout/app/auth.onus
module app.auth
import std.io
import app.contracts
-- AuthedCustomer is evidence: only `require` produces one (§3.10).
pub sealed record AuthedCustomer {
id: Text
}
pub union Error =
| Unknown of caller: Text
| Expired
pub capability Service
grants io.net
pub fn require(
service: Service,
caller: Text,
customer: Text,
clock: io.Clock
) -> Result[AuthedCustomer, Error] may io.net
claims Idempotent
ensures result is Ok implies caller == customer
{
if caller == customer {
return Ok(value: AuthedCustomer { id: customer })
}
return Err(error: Unknown(caller: caller))
}examples/checkout/app/contracts.onus
module app.contracts
pub claim Idempotent "Calling twice with the same arguments has the same observable effect as calling once."examples/checkout/vendor/payments.onus
module vendor.payments
import std.io
import app.auth
import app.contracts
pub capability Client
grants io.net
pub union Error =
| Declined of reason: Text
pub record Receipt {
id: Text
amount: Int where it >= 0
}
pub fn charge(
client: Client,
key: Text,
amount: Int where it >= 0,
who: auth.AuthedCustomer
) -> Result[Receipt, Error] may io.net, alloc
claims Idempotent
{
assume Idempotent "Vendor API deduplicates on key for 24h; see contract §4.2"
verify(client: Client, service: auth.Service, clock: io.Clock) may io.net, alloc {
let who: auth.AuthedCustomer = try auth.require(
service: service,
caller: "verify",
customer: "verify",
clock: clock
) else _: false
let a: Receipt = try charge(client: client, key: "verify-1", amount: 100, who: who)
else _: false
let b: Receipt = try charge(client: client, key: "verify-1", amount: 100, who: who)
else _: false
a.id == b.id
}
return Ok(value: Receipt { id: key ++ "/" ++ who.id, amount: amount })
}examples/checkout/test_env.onus
test module test_env
import std.io
import app.auth
import vendor.payments
-- The environment for `onus test --assumptions` (§20.2): how each capability a verify block needs is constructed.
-- Root capabilities (io.Clock) come from the runtime unless a function here returns them.
pub fn client() -> payments.Client {
return fake payments.Client {}
}
pub fn service() -> auth.Service {
return fake auth.Service {}
}Ledger
What onus review reported for this example, from examples/checkout/review/review.json. The review page it wrote is served unchanged.
Module checkout: 6 proved · 0 checked · 0 assumed · 0 failed. Written by onus review on 3 September 2026.
| Item | Kind | Effects | Proved | Checked | Assumed | Failed |
|---|---|---|---|---|---|---|
| pub recent_orders | fn | sql.read, alloc | 2 | 0 | 0 | 0 |
| load_basket | fn | sql.read, alloc | 3 | 0 | 0 | 0 |
| record_order | fn | sql.write, alloc | 0 | 0 | 0 | 0 |
| pub handle_checkout | fn | sql.read, sql.write, io.net, io.clock, alloc | 1 | 0 | 0 | 0 |
Path checkout
path checkout · entry checkout.handle_checkout · 14 functions reachable · effects within alloc, io.clock, io.net, sql.read, sql.write · requires app.contracts.Idempotent · passes
entryfunctionintrinsiccarries an assumeassumption outside the project, permitted by except
Obligations on the path: 8 proved · 0 checked · 0 assumed · 0 failed · capabilities constructed on the path: sql.Db[ReadOnly] at checkout.handle_checkout:89:44
| Obligation | In | Status | Discharged by |
|---|---|---|---|
requires parse_select(text: text) is Ok | load_basket | provedpinned | const evaluator |
requires columns_match(text: text, record: row) is Ok | load_basket | provedpinned | const evaluator |
refinement it >= 0 | load_basket | proved | z3 |
refinement it >= 0 | handle_checkout | proved | z3 |
ensures result is Ok implies caller == customer | require | proved | z3 |
ensures result is Ok implies caller == customer | require | proved | z3 |
refinement it >= 0 | charge | proved | z3 |
ensures result == (len(xs: xs) == 0) | is_empty | proved | z3 |
Assumptions on the path (3)
- app.contracts.Idempotent at checkout.load_basketin scope
“A select reads only; it has no observable effect.” - app.contracts.Idempotent at vendor.payments.chargeoutside the project · permitted by except
“Vendor API deduplicates on key for 24h; see contract §4.2” - app.contracts.Idempotent at checkout.record_orderin scope
“The insert is `on conflict (receipt_id) do nothing`.”