Understanding the Concierge

What the concierge is

The concierge is poly's release example and the agent of the live demo. A small shop answers its customers on WhatsApp. A customer asks where an order is, or asks for money back. Staff follow along on Slack. Refunds go through the shop's Stripe account under a delegated credential.

The program is about 490 lines of poly and a 30-line policy. In the demo, Stripe is a local stand-in and the shop and its customers are made up. The companion pages are Understanding Poly for the language and the refund demo’s records in the repository for the three acts and how to run them.

How it is built

A message travels from the customer to the Desk, through the model's typed answers, to the gate. Only what the gate allows reaches the refund handler, and only what the handler checks reaches Stripe.

The dashed arrow to the staff is a notice; the solid one back is a signed approval or resolve. A Slack message cannot approve.

The Desk machine

Each customer has a Desk. It holds what the conversation is doing, who the customer is, and whether a refund is already issued or still uncertain. It answers one message at a time.

enum Ledger { None, Unknown, Issued }
type Amount = { value: 0..500 }

service machine Desk {
  state {
    phase    : Phase     = Idle
    customer : Principal = none
    question : Content   = none
    refund   : Ledger    = None
    // ... four more fields
  }
  never no-reissue: emit refund while refund != None
}

The amount is a type with a strict domain. A model answer outside 0..500 is refused before it becomes a step.

How a refund is decided

The model reads the message and the customer's own orders, and must answer with a whole number and the one order it is about. Four guards stand between that answer and an emitted refund.

decision amount(text: Content, context: Items) -> Amount {
  provider "small"
  labels { egress:external, read:private }
  cites context
  ok(r) -> Amounted(value: r.answer.value, conf: r.conf.value, cites: r.cites)
  failed -> Unextracted()
}

on Amounted(value, conf, cites) {
  require phase == Extracting else reject "not-extracting"
  if conf >= 0.8 {
    if cites.count == 1 {
      if refund == None {
        phase' = Refunding
        large' = value > 100
        refund' = Unknown
        emit refund(amount: value, customer: customer, order: cites)
      } else { // reply "being checked" or "already processed" }
    } else { // reply Unsure }
  } else { // reply Unsure }
}

1. The type. The amount is 0..500. "Refund me 5,000" is refused at dispatch and journaled; the handler never sees it.
2. The confidence. Below 0.8, the guest is told the request is unclear. The amount is a vote of five asks, so the confidence is the share that agreed.
3. The citation. The answer must cite exactly one of the customer's own orders. Two orders, or none, gets an "unsure" reply.
4. The ledger. A refund already issued or still uncertain in this conversation blocks a new one.

The refund itself is declared as an irreversible effect with a key. The runtime attaches the same key to every attempt of one intent, so a lost answer and a retry give one refund.

effect refund(amount: 0..500, customer: Principal, order: Items) {
  kind "payments.refund"
  targets { egress: ["https://api.stripe.com/v1/refunds", "https://api.stripe.com/v1/charges/"] }
  uses payments { read_write }
  one order
  class irreversible
  idempotent header "Idempotency-Key" window 24h
  ok -> Refunded()
  failed -> RefundFailed()
  exhausted -> RefundUnknown()
}

Three outcomes, three meanings: it happened, it definitely did not, or nobody knows. Only the last needs a person.

Who may say yes

The policy is a separate file a person signs. It holds three obligations, and the gate applies them to every effect against the state that emitted it.

policy refunds {
  scope "concierge"
  obligation large-refund-reviewed "A refund above 100 is issued only after a person approves it." rule {
    when effect.kind == "payments.refund" && machine("concierge.Desk").large
    require false else escalate
  }
  obligation customer-decisions "A model answering a customer is given nothing above the customer audience." ...
  obligation staff-decisions "A model answering the staff is given nothing above the staff audience." ...
}

Each attack, each layer

In the live demo the audience attacks the concierge over a real model. Each attack is stopped by a different part of the program, and each part is either checked or enforced at run time.

What is checked

The demo copy is checked and admitted on every launch, CLEAN, over an instance of 5762 Desk states and the machines it talks to. The check covers every answer each decision could give, including the worst.

• No second refund in a conversation. no-reissue: no refund intent while one is issued or uncertain.
• Retries are safe. The refund is irreversible with up to five attempts, so it must declare a key; without one the check reports PL4003 and the build is not admitted.
• No guest reaches another's order. Every body carries its owner as taint, and the flow rules are checked on every path.
• Every model call crosses the gate. A decision whose inputs are above its audience is denied.
• Spending stays under the cap. Each call's worst case is reserved before it is sent.

At run time the same rules are enforced again, every step is journaled, and the journal replays with no divergence in the recorded end-to-end test.

What it does not cover

• One refund per conversation, not per order. A cited order has no readable identity in the program, so a guest with two orders cannot refund the second in the same thread. A per-order rule waits for a data layer.
• The handler is host code. The check that a refund is no more than what was paid lives in the handler, held by capabilities and tests, not by the checker.
• The provider honours the key. That Stripe returns the first answer for a repeated key is an assumption, stated in the certificate.
• The same reply to two guests. A reply text carries its recipient as taint by its digest; the same text for a second guest is refused. Refund attacks run one guest at a time.
• An escalation nobody approves leaves the guest with no reply.
• Calibration. The confidence maps are stand-ins until a calibration run fits them to the models in use.

Conclusion

The concierge puts a model in front of customers and money, and keeps the model out of every decision that matters. The model classifies, extracts and writes; the program decides, through a typed amount, a cited order, a ledger and a policy a person signed. Each attack in the demo is stopped by a named part, and most of those parts are checked over every answer the model could give. What is left to host code and to assumptions is listed, so the guarantee can be read for exactly what it covers.

Glossary

Desk

The machine that holds one customer's conversation and refund ledger.

Decision

A model call whose answer is a finite typed value, explored by the checker.

Citation

The order a decision's answer is about, chosen from the customer's own orders.

Ledger

The Desk's record of its refund: None, Unknown or Issued.

Gate

The runtime component that allows, denies or escalates each effect against the policy.

Escalation

A refund held for a person's signed approval.

Resolve

A person's signed decision that settles an uncertain refund as done or not done.

Idempotency key

The id the runtime attaches to every attempt of one refund intent, so the provider runs it once.

Taint

The owner and audience a body carries, followed on every path.

Journal

The hash-chained, signed record of every step and verdict, which replays exactly.