Onus review: checkout

assume	at	justification	permitted by
`app.contracts.Idempotent`	`checkout.load_basket`	A select reads only; it has no observable effect.	permitted by scope
`app.contracts.Idempotent`	`vendor.payments.charge`	Vendor API deduplicates on key for 24h; see contract §4.2	permitted by except
`app.contracts.Idempotent`	`checkout.record_order`	The insert is `on conflict (receipt_id) do nothing`.	permitted by scope

type	constructed at	assumes
`sql.Db[ReadOnly]`	`checkout.handle_checkout:89:44`	none recorded

status	kind	obligation	in	at	by
proved (pinned)	requires	`parse_select(text: text) is Ok`	`checkout.load_basket`	`examples/checkout/checkout.onus:45:33`	const evaluator
proved (pinned)	requires	`columns_match(text: text, record: row) is Ok`	`checkout.load_basket`	`examples/checkout/checkout.onus:45:33`	const evaluator
proved	refinement	`it >= 0`	`checkout.load_basket`	`examples/checkout/checkout.onus:50:50`	z3
proved	refinement	`it >= 0`	`checkout.handle_checkout`	`examples/checkout/checkout.onus:97:13`	z3
proved	ensures	`result is Ok implies caller == customer`	`app.auth.require`	`/Users/jamesrandall/code/onus/examples/checkout/app/auth.onus:27:5`	z3
proved	ensures	`result is Ok implies caller == customer`	`app.auth.require`	`/Users/jamesrandall/code/onus/examples/checkout/app/auth.onus:29:3`	z3
proved	refinement	`it >= 0`	`vendor.payments.charge`	`/Users/jamesrandall/code/onus/examples/checkout/vendor/payments.onus:26:64`	z3
proved	ensures	`result == (len(xs: xs) == 0)`	`std.list.is_empty`	`/Users/jamesrandall/code/onus/packages/stdlib/std/list.onus:12:3`	z3

module `checkout`

b3:516166b94e67f6e878aaf51f4546679c89c1d31d1779d8885705dcfd62bf1764 · imports std.sql, std.io, app.auth, app.contracts, vendor.payments · 6 proved · 2 assumed claims · 0 recover sites · 0 of 4 bodies opened

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
}

pub fn recent_orders(
  db: sql.Db[ReadOnly, schema: "orders"],
  who: auth.AuthedCustomer
) -> Result[List[Order], sql.Error] may sql.read, alloc

effects sql.read, alloc · 2 proved

{ ... } expand body (counted)

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

effects sql.read, alloc · claims Idempotent · 3 proved

assume Idempotent — A select reads only; it has no observable effect. (examples/checkout/checkout.onus:44:3)

{ ... } expand body (counted)

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

effects sql.write, alloc · claims Idempotent · 0 proved

assume Idempotent — The insert is `on conflict (receipt_id) do nothing`. (examples/checkout/checkout.onus:61:3)

{ ... } expand body (counted)

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

effects sql.read, sql.write, io.net, io.clock, alloc · claims Idempotent · 1 proved

{ ... } expand body (counted)

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 }

module `app.auth`

b3:32dc8527866c6e8fd3fc53427a9f3dc3c9228f9f006732e2d284d06efb0af0e9 · imports std.io, app.contracts · 2 proved · 0 assumed claims · 0 recover sites · sealed AuthedCustomer · 0 of 1 bodies opened

-- 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, io.clock

effects io.net, io.clock · claims Idempotent · 2 proved

ensures result is Ok implies caller == customer

{ ... } expand body (counted)

pub fn require(
  service: Service,
  caller: Text,
  customer: Text,
  clock: io.Clock
) -> Result[AuthedCustomer, Error] may io.net, io.clock
  claims Idempotent
  ensures result is Ok implies caller == customer
{
  if caller == customer {
    return Ok(value: AuthedCustomer { id: customer })
  }
  return Err(error: Unknown(caller: caller))
}

module `app.contracts`

b3:5e9a934a233bb32e5f5e211459531261fd3d9ff5727966bde7afa52142174b07 · imports nothing · 0 proved · 0 assumed claims · 0 recover sites · 0 of 0 bodies opened

pub claim Idempotent "Calling twice with the same arguments has the same observable effect as calling once."

module `vendor.payments`

b3:b5846a32fec5efd85187b8fb322153b0f1f93501067cadc4f99eb7bbde1ddcfe · imports std.io, app.auth, app.contracts · 1 proved · 1 assumed claim · 0 recover sites · 0 of 1 bodies opened

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

effects io.net, alloc · claims Idempotent · 1 proved

assume Idempotent — Vendor API deduplicates on key for 24h; see contract §4.2 (/Users/jamesrandall/code/onus/examples/checkout/vendor/payments.onus:25:3)

{ ... } expand body (counted)

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"
  return Ok(value: Receipt { id: key ++ "/" ++ who.id, amount: amount })
}

Onus review · `checkout`

path `checkout` ok

Assumptions

Capabilities

Ledger (8 proved)

module `checkout`

module `app.auth`

module `app.contracts`

module `vendor.payments`

Ledger

Assumptions (3)

Recover sites (0)

Capability construction sites (1)

Diff

Diagnostics

in	claim	justification	at
`checkout.load_basket`	`Idempotent`	A select reads only; it has no observable effect.	`examples/checkout/checkout.onus:44:3`
`checkout.record_order`	`Idempotent`	The insert is `on conflict (receipt_id) do nothing`.	`examples/checkout/checkout.onus:61:3`
`vendor.payments.charge`	`Idempotent`	Vendor API deduplicates on key for 24h; see contract §4.2	`/Users/jamesrandall/code/onus/examples/checkout/vendor/payments.onus:25:3`

path checkout ok

Assumptions

Capabilities

Ledger (8 proved)

module checkout

module app.auth

module app.contracts

module vendor.payments

Ledger

Assumptions (3)

Recover sites (0)

Capability construction sites (1)

Diff

Diagnostics

path `checkout` ok

module `checkout`

module `app.auth`

module `app.contracts`

module `vendor.payments`