payments: the reply that never comes, and the idempotency key

README.md

@@ -56,6 +56,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding
 | [`expense-approval/`](expense-approval/) | Can a large expense be paid without two independent approvals? | Yes, when one person holds both roles: "two signatures" counted boxes, not people. |
 | [`agent-guardrails/`](agent-guardrails/) | Can an AI agent's secret leave the machine with no human saying yes? | Not under v1. Add a "read-only" web-fetch and it can, in three moves, none of them human's. |
 | [`deployment/`](deployment/) | Is production ever dark mid-rollout, and can the fleet always roll back? | Never dark behind a health gate; but after the migration, the runbook's rollback is unreachable for good. |
+| [`payments/`](payments/) | Can a lost reply and a retry charge a customer twice? | Without an idempotency key, in six steps, each correct where it stood. The key also stops a late capture beating a cancellation. |
 | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. |
 
 **Design, judgement and change**

docker-compose.yml

@@ -95,6 +95,12 @@ services:
     image: writ-problems
     command: ["deployment"]
 
+  # Payments: a lost reply, a retry, and the idempotency key.
+  payments:
+    build: .
+    image: writ-problems
+    command: ["payments"]
+
   # A timetable CP-SAT decided, audited: one state, two broken school rules,
   # two questions the curriculum never answered.
   timetable:

modality-cross-check.sh

@@ -34,7 +34,7 @@ set -u
 here=$(cd "$(dirname "$0")" && pwd)
 WRIT=${WRIT:-writ}
 
-scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment"
+scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver expense-approval agent-guardrails deployment payments"
 
 considered=0
 compared=0

payments/README.md

@@ -0,0 +1,170 @@
+# Payments: the reply that never comes
+
+A shop takes payment in two steps: **authorize** the card, which reserves the
+money, then **capture**, which takes it. The capture is a request to a payment
+processor, and the processor's reply can be lost: a timeout, a dropped
+connection, a load balancer restart. The shop then does not know whether the
+money was taken, so it does what every integration does. It waits, and it
+asks again.
+
+If the first request did land, the retry is a second capture. The customer is
+charged twice, and nothing on the shop's side looks wrong: it received one
+reply, recorded one capture, and shipped one order. The usual cure is an
+**idempotency key**: every request carries a key, and the processor answers a
+repeated key with the original reply instead of acting again.
+
+## The model
+
+[`payments.writ`](payments.writ) follows one order:
+
+- the shop's view, `o`: its `stage` (`placed`, `authorized`, `captured`,
+  `settled`, `refunded`, `cancelled`) and whether it has shipped;
+- the wire, `net`: a capture `request` on its way out, a `reply` on its way
+  back, and a `void` (more below);
+- the processor's view, `proc`: how many times it has taken the money
+  (`none`, `one`, `two`), whether it has refunded, and the keys it has
+  already honoured (`seen`).
+
+The processor counts captures, not money. The questions are about how many
+times the money was taken, so a three-member type is the honest size, and
+`two` is the bug. A refund question that needed partial amounts would add a
+band (`none`, `partial`, `full`), still not a number.
+
+The shop's moves are `authorize`, `send-capture`, `receive-reply`, `settle`,
+`ship`, `refund` and `cancel`. `send-capture` is the first attempt and every
+retry: whenever the shop is waiting on a capture, with nothing out and
+nothing back, it sends one. The network's move is `lose-reply`.
+
+The processor's moves are where the two files differ. With the key
+(`payments.writ`), `capture` records `k1`, and a request carrying a seen key
+gets `replay-reply`: the original answer, no second capture.
+[`payments-shortcut.writ`](payments-shortcut.writ) sends no key, so the
+processor has nothing to record or check, and `capture-again` takes the money
+a second time.
+
+## What writ answers
+
+The questions are in [`payments.claims`](payments.claims). With the key,
+exit 0:
+
+```
+holds  settles
+  "a payment can settle"
+holds  never-double
+  "the customer is never charged twice"
+holds  never-charged-for-nothing
+  "once the wire is quiet, a cancelled order never leaves the customer charged"
+holds  always-terminal
+  "from everywhere, the order can still reach an end"
+certified: every answer re-derived from the model (writ-cert)
+```
+
+Without it, exit 1:
+
+```
+fails  never-double
+  "the customer is never charged twice"
+  witness:  1. authorize       → #1   o.stage: placed → authorized
+            2. send-capture    → #3   net.request: no → yes
+            3. capture         → #5   net.request: yes → no, net.reply: no → yes, proc.captures: none → one
+            4. lose-reply      → #8   net.reply: yes → no
+            5. send-capture    → #13   net.request: no → yes
+            6. capture-again   → #16   net.request: yes → no, net.reply: no → yes, proc.captures: one → two
+```
+
+Read it as the support ticket it becomes. The shop asked for the money, the
+processor took it, the answer got lost, the shop asked again, and the
+processor took it again. Every step is correct from where it stands. No
+single component misbehaved.
+
+[`payments.rules`](payments.rules) shows where those double charges end up,
+as the shop sees the order:
+
+```sh
+writ derive payments-shortcut.writ payments.rules double-charged
+```
+
+```
+double-charged  (13 rows)
+  22  authorized  no
+  …
+  29  settled  no
+  30  captured  yes
+  31  refunded  no
+  …
+  34  settled  yes
+  35  cancelled  no
+```
+
+Settled and shipped, refunded (one capture given back, one kept), cancelled:
+the double charge appears in every stage the shop has, and nothing marks it.
+It reaches support as a complaint, not as an alert.
+
+## The cancellation that loses the race
+
+The shortcut fails a second question:
+
+```
+fails  never-charged-for-nothing
+  "once the wire is quiet, a cancelled order never leaves the customer charged"
+  witness:  1. authorize            → #1   o.stage: placed → authorized
+            2. send-capture         → #3   net.request: no → yes
+            3. cancel               → #5   o.stage: authorized → cancelled, net.void: no → yes
+            4. void-uncaptured      → #8   net.void: yes → no
+            5. capture              → #13   net.request: yes → no, net.reply: no → yes, proc.captures: none → one
+            6. discard-late-reply   → #19   net.reply: yes → no
+```
+
+The shop cancels while its capture request is still on the wire, and sends a
+void. The void arrives first, finds nothing to refund, and is done. Then the
+capture lands. With a key, the void marks `k1` as used, so the late capture is
+answered with a replay and takes nothing. Without a key there is nothing to
+mark. The key is not only a retry mechanism: it is what lets a cancellation
+refer to a request that has not arrived yet.
+
+"Once the wire is quiet" is part of the question on purpose. While a request
+or a void is still in flight, the charge is unresolved, not wrong. The
+property asks about the situations where nothing more will arrive.
+
+## What writ found while this was being written
+
+The first draft of the safe file had no void. `cancel` was allowed whenever
+the shop had not captured, because from its own records no money had moved.
+writ failed it, key and all (change columns trimmed):
+
+```
+fails  never-charged-for-nothing
+  witness:  1. authorize
+            2. send-capture
+            3. cancel
+            4. capture
+```
+
+The shop's record says "not captured" in two different situations: nothing
+was sent, or something was sent and nothing came back. Only the first is safe
+to cancel on. The fix, in both files, is that cancelling also voids at the
+processor. With the key the void is enough; without it, as above, it is not.
+
+## What to take away
+
+At-least-once delivery plus a non-idempotent operation means sometimes
+twice, and testing rarely shows it, because the lost reply is rare and the
+double charge looks like a normal order. The question that catches it,
+"never two captures", is about the processor's state, which the shop never
+sees. That is why it belongs in a model.
+
+The shortcut still settles and still reaches an end. Unlike the migration
+problems, it is not even faster. It skips no wait. It just leaves out one
+field on the request.
+
+## Run it
+
+```sh
+writ check payments.writ --claims payments.claims           # exit 0
+writ check payments-shortcut.writ --claims payments.claims  # exit 1
+writ compare payments.writ payments-shortcut.writ           # exit 1: both guarantees LOST
+```
+
+`../modality-cross-check.sh` checks the `.rules` encoding against `writ check`.
+`../two-phase-commit/` has the same lossy-wire idiom, applied to agreement
+rather than money.

payments/payments-shortcut.writ

@@ -0,0 +1,132 @@
+; The same lifecycle, with NO IDEMPOTENCY KEY: the retry is a brand new
+; request as far as the processor can tell.
+;
+; Every step is correct from where it stands. The shop did not get a reply, so
+; it asked again. The processor got a request, so it captured.
+;
+; `writ check` exits 1 on this file.
+
+(load "stdlib.writ")
+(load "payments.lib.writ")
+
+(schema payments
+
+  (type yn (no yes))
+
+  ; The shop's view of the order.
+  (type stage-t (placed authorized captured settled refunded cancelled))
+  (type order
+    (arrow stage    (to stage-t))
+    (arrow shipment (to yn)))
+
+  ; The wire: a capture request on its way to the processor, and the
+  ; processor's reply on its way back. Either may be in flight; the reply can
+  ; be lost.
+  (type wire
+    (arrow request (to yn))
+    (arrow reply   (to yn))
+    (arrow void    (to yn)))
+
+  ; The processor's view. How many times it has taken the money, not how much:
+  ; none, one, or two, and two is the bug. Whether it has refunded. And the
+  ; idempotency keys it has already honoured.
+  (type count (none one two))
+  (type key-t (k1))
+  (type processor
+    (arrow captures (to count))
+    (arrow refunded (to yn))
+    (maybe seen key-t))
+
+  ; ---- the rules ----
+
+  ; The customer is charged at most once.
+  (equation one-capture (not (is processor.captures two)))
+
+  ; A cancelled order never ships.
+  (equation cancelled-never-ships
+    (not (and (is order.stage cancelled) (is order.shipment yes)))))
+
+(instance start payments
+  (order o (stage placed) (shipment no))
+  (wire net (request no) (reply no) (void no))
+  (processor proc (captures none) (refunded no) (seen vacant)))
+
+(use payments)
+(initial start)
+
+; ---- the shop ----
+
+(transition authorize
+  (when (is o.stage placed))
+  (do (set o.stage authorized)))
+
+; Ask the processor to capture. The same move is the first attempt and every
+; retry: whenever the shop is waiting on a capture and has no request out and
+; no reply in, it sends one. That is what a timeout-and-retry loop does.
+(transition send-capture
+  (when (and (is o.stage authorized) (is net.request no) (is net.reply no)))
+  (do (set net.request yes)))
+
+(transition receive-reply
+  (when (and (is net.reply yes) (is o.stage authorized)))
+  (do (set net.reply no) (set o.stage captured)))
+
+; A reply for an order the shop has already cancelled is dropped.
+(transition discard-late-reply
+  (when (and (is net.reply yes) (is o.stage cancelled)))
+  (do (set net.reply no)))
+
+(transition settle
+  (when (is o.stage captured))
+  (do (set o.stage settled)))
+
+(transition ship
+  (when (and (or (is o.stage captured) (is o.stage settled)) (is o.shipment no)))
+  (do (set o.shipment yes)))
+
+(transition refund
+  (when (and (or (is o.stage captured) (is o.stage settled)) (is o.shipment no)))
+  (do (set o.stage refunded) (set proc.refunded yes)))
+
+; Cancel an order the shop has not captured. From its own view no money
+; moved, but a capture request may be out, or may have landed and lost its
+; reply. So cancelling also tells the processor to void the payment.
+;
+; The first draft of this file cancelled without the void, and writ found it:
+; authorize, send the capture, cancel, and the capture lands after the
+; cancellation. See the README.
+(transition cancel
+  (when (and (or (is o.stage placed) (is o.stage authorized)) (is o.shipment no)))
+  (do (set o.stage cancelled) (set net.void yes)))
+
+; ---- the network ----
+
+; The processor's reply never arrives: a timeout, a dropped connection, a
+; load balancer restart. The capture itself happened.
+(transition lose-reply
+  (when (is net.reply yes))
+  (do (set net.reply no)))
+
+; ---- the processor ----
+
+; No idempotency key: the request carries nothing the processor could
+; recognise, so it records nothing and checks nothing. Every request that
+; arrives is a capture.
+(transition capture
+  (when (and (is net.request yes) (is proc.captures none)))      ; <- key check, gone
+  (do (set net.request no) (set proc.captures one) (set net.reply yes)))  ; <- key record, gone
+(transition capture-again
+  (when (and (is net.request yes) (is proc.captures one)))       ; <- key check, gone
+  (do (set net.request no) (set proc.captures two) (set net.reply yes)))
+; A void: refund a capture already made. With no key, there is nothing to
+; mark, so a capture request still on the wire is honoured when it lands.
+(transition void-captured
+  (when (and (is net.void yes) (is proc.captures one)))
+  (do (set net.void no) (set proc.refunded yes)))         ; <- key record, gone
+(transition void-uncaptured
+  (when (and (is net.void yes) (is proc.captures none)))
+  (do (set net.void no)))                                 ; <- key record, gone
+(transition replay-reply
+  (when (and (is net.request yes) (is proc.seen k1)))
+  (do (set net.request no) (set net.reply yes)))
+

payments/payments.claims

@@ -0,0 +1,29 @@
+; The questions, put to both integrations.
+
+(load "payments.lib.writ")
+
+(property settles
+  "a payment can settle"
+  (possible (is o.stage settled)))
+
+(property never-double
+  "the customer is never charged twice"
+  (never (is proc.captures two)))
+
+(property never-charged-for-nothing
+  "once the wire is quiet, a cancelled order never leaves the customer charged"
+  (never (and charged-for-nothing quiet)))
+
+(property always-terminal
+  "from everywhere, the order can still reach an end"
+  (live terminal))
+
+; ---- ownership ----
+(accept capture       one-capture)
+(accept capture-again one-capture)
+(accept authorize     cancelled-never-ships)
+(accept receive-reply cancelled-never-ships)
+(accept settle        cancelled-never-ships)
+(accept ship          cancelled-never-ships)
+(accept refund        cancelled-never-ships)
+(accept cancel        cancelled-never-ships)

payments/payments.lib.writ

@@ -0,0 +1,17 @@
+; Shared by the models and the questions, because a questions file has its own
+; form scope and there is no implicit prelude.
+(load "stdlib.writ")
+
+; The order has reached an end: settled, refunded or cancelled.
+(form terminal
+  (or (is o.stage settled) (is o.stage refunded) (is o.stage cancelled)))
+
+; The customer has paid for an order they will not get: it was cancelled, and
+; the processor holds a capture nobody refunded.
+(form charged-for-nothing
+  (and (is o.stage cancelled) (not (is proc.captures none)) (is proc.refunded no)))
+
+; Nothing on the wire: no request, reply or void still to land. Until then the
+; charge is unresolved, not wrong.
+(form quiet
+  (and (is net.request no) (is net.reply no) (is net.void no)))