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.

ItemKindEffectsProvedCheckedAssumedFailed
pub recent_ordersfnsql.read, alloc2000
load_basketfnsql.read, alloc3000
record_orderfnsql.write, alloc0000
pub handle_checkoutfnsql.read, sql.write, io.net, io.clock, alloc1000

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

checkout.handle_checkout → app.auth.require (io.clock, io.net)checkout.handle_checkout → checkout.load_basket (alloc, sql.read)checkout.handle_checkout → std.sql.narrowcheckout.handle_checkout → std.list.is_emptycheckout.handle_checkout → vendor.payments.charge (alloc, io.net)checkout.handle_checkout → checkout.record_order (alloc, sql.write)checkout.load_basket → std.sql.selectcheckout.load_basket → std.sql.textcheckout.load_basket → std.sql.query (alloc, sql.read)std.list.is_empty → std.list.lencheckout.record_order → std.sql.statementcheckout.record_order → std.sql.textcheckout.record_order → std.sql.textcheckout.record_order → std.sql.intcheckout.record_order → std.sql.execute (alloc, sql.write)callable only with app.auth.AuthedCustomer, which only app.auth.require producescheckout.handle_checkout · may alloc, io.clock, io.net, sql.read, sql.write · 1 proved, 0 checkedhandle_checkoutcheckoutapp.auth.require · may io.clock, io.net · 2 proved, 0 checkedrequireapp.authcheckout.load_basket · may alloc, sql.read · 3 proved, 0 checked · 1 assumeload_basketcheckoutstd.sql.narrow · 0 proved, 0 checkednarrowstd.sqlstd.list.is_empty · 1 proved, 0 checkedis_emptystd.listvendor.payments.charge · may alloc, io.net · 1 proved, 0 checked · 1 assumechargevendor.paymentscheckout.record_order · may alloc, sql.write · 0 proved, 0 checked · 1 assumerecord_ordercheckoutstd.sql.select · 0 proved, 0 checkedselectstd.sqlstd.sql.text · 0 proved, 0 checkedtextstd.sqlstd.sql.query · may alloc, sql.read · 0 proved, 0 checkedquerystd.sqlstd.list.len · 0 proved, 0 checkedlenstd.liststd.sql.statement · 0 proved, 0 checkedstatementstd.sqlstd.sql.int · 0 proved, 0 checkedintstd.sqlstd.sql.execute · may alloc, sql.write · 0 proved, 0 checkedexecutestd.sql

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

ObligationInStatusDischarged by
requires parse_select(text: text) is Okload_basketprovedpinnedconst evaluator
requires columns_match(text: text, record: row) is Okload_basketprovedpinnedconst evaluator
refinement it >= 0load_basketprovedz3
refinement it >= 0handle_checkoutprovedz3
ensures result is Ok implies caller == customerrequireprovedz3
ensures result is Ok implies caller == customerrequireprovedz3
refinement it >= 0chargeprovedz3
ensures result == (len(xs: xs) == 0)is_emptyprovedz3

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`.”