From c50a1efa9c75382a95791f87d81b9997fc8ce396 Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 20:30:53 +0300 Subject: [PATCH] payments: the reply that never comes, and the idempotency key One order: authorize, capture over a wire that loses replies, settle, ship, refund, cancel. Without a key, a lost reply and a retry charge twice in six steps; derive double-charged shows the order looking normal in every stage. The shortcut also charges for a cancelled order: the void overtakes the capture, finds nothing, and the capture lands after it. Writing it, writ failed the first draft of the SAFE file, key and all: cancel was allowed whenever the shop had not captured, so a capture still on the wire landed after the cancellation. cancel now voids at the processor, under the same key. Cross-check 52 -> 56 properties (54 compared); 314 checks. Co-Authored-By: Claude Opus 5.5 --- README.md | 1 + docker-compose.yml | 6 ++ modality-cross-check.sh | 2 +- payments/README.md | 170 ++++++++++++++++++++++++++++++++ payments/payments-shortcut.writ | 132 +++++++++++++++++++++++++ payments/payments.claims | 29 ++++++ payments/payments.lib.writ | 17 ++++ payments/payments.rules | 32 ++++++ payments/payments.writ | 133 +++++++++++++++++++++++++ run-tests.sh | 50 ++++++++-- 10 files changed, 561 insertions(+), 11 deletions(-) create mode 100644 payments/README.md create mode 100644 payments/payments-shortcut.writ create mode 100644 payments/payments.claims create mode 100644 payments/payments.lib.writ create mode 100644 payments/payments.rules create mode 100644 payments/payments.writ diff --git a/README.md b/README.md index aabf38c..c964a0e 100644 --- a/README.md +++ b/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** diff --git a/docker-compose.yml b/docker-compose.yml index 8488cdc..c5c14eb 100644 --- a/docker-compose.yml +++ b/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: diff --git a/modality-cross-check.sh b/modality-cross-check.sh index 88c96aa..ce0471d 100755 --- a/modality-cross-check.sh +++ b/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 diff --git a/payments/README.md b/payments/README.md new file mode 100644 index 0000000..3d6f671 --- /dev/null +++ b/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. diff --git a/payments/payments-shortcut.writ b/payments/payments-shortcut.writ new file mode 100644 index 0000000..194f63a --- /dev/null +++ b/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))) + diff --git a/payments/payments.claims b/payments/payments.claims new file mode 100644 index 0000000..3b5389f --- /dev/null +++ b/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) diff --git a/payments/payments.lib.writ b/payments/payments.lib.writ new file mode 100644 index 0000000..c1e520f --- /dev/null +++ b/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))) diff --git a/payments/payments.rules b/payments/payments.rules new file mode 100644 index 0000000..19d17ec --- /dev/null +++ b/payments/payments.rules @@ -0,0 +1,32 @@ +; The same four questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "payments.lib.writ") + +(satisfies settles (is o.stage settled)) + +(satisfies never-double (is proc.captures two)) + +(satisfies never-charged-for-nothing (and charged-for-nothing quiet)) + +(satisfies ended terminal) +(can-reach can-end ended) +(trapped always-terminal can-end) + +; ---- the explanation ---- +; Where the double charge leaves the order, as the shop sees it: its stage, +; and whether it shipped. The rows cover every stage there is: settled and +; shipped, refunded (one capture given back, one kept), cancelled. Nothing on +; the shop's side marks them, which is why this reaches support as a customer +; complaint and not as an alert. +(relation double-charged (Situation stage-t yn)) +(rule (double-charged S G Y) + (situation S) + (holds S (is proc.captures two)) + (holds S (is o.stage G)) + (holds S (is o.shipment Y))) diff --git a/payments/payments.writ b/payments/payments.writ new file mode 100644 index 0000000..feb95ce --- /dev/null +++ b/payments/payments.writ @@ -0,0 +1,133 @@ +; A payment's lifecycle, over a network that loses replies. +; +; The shop authorizes the customer's card, asks the processor to capture the +; money, and settles. It can ship, refund, or cancel. The processor's reply can +; be lost; the shop then retries, as every payment integration does. The +; retry carries an idempotency key, so the processor recognises it. +; +; `writ check` exits 0 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 ---- + +; Every request carries the idempotency key k1. A key the processor has not +; seen is a capture; a key it has seen gets the original reply again, and no +; second capture. +(transition capture + (when (and (is net.request yes) (is proc.captures none) (not (is proc.seen k1)))) + (do (set net.request no) (set proc.captures one) (set proc.seen k1) (set net.reply yes))) +(transition capture-again + (when (and (is net.request yes) (is proc.captures one) (not (is proc.seen k1)))) + (do (set net.request no) (set proc.captures two) (set net.reply yes))) +; A void under the same key: refund a capture already made, and mark the key +; used, so a capture request still on the wire is replayed, not honoured. +(transition void-captured + (when (and (is net.void yes) (is proc.captures one))) + (do (set net.void no) (set proc.refunded yes) (set proc.seen k1))) +(transition void-uncaptured + (when (and (is net.void yes) (is proc.captures none))) + (do (set net.void no) (set proc.seen k1))) +(transition replay-reply + (when (and (is net.request yes) (is proc.seen k1))) + (do (set net.request no) (set net.reply yes))) + diff --git a/run-tests.sh b/run-tests.sh index 24f0937..f90d174 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,18 +431,18 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The nineteen scenarios this script walks by convention, and their 52 + # The twenty scenarios this script walks by convention, and their 56 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the nineteen fails this line, which is the point of it — + # property to any of the twenty fails this line, which is the point of it — # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, # 26 -> 31 with two-phase-commit, 31 -> 41 with the three # entitlement-problems (3 + 3 + 4), 41 -> 45 with expense-approval, and - # 45 -> 49 with agent-guardrails, 49 -> 52 with deployment, and this line is - # where each of those had to be said out loud. - has "cross-check: all 52 properties of the nineteen scenarios were considered" \ - "$out" "considered 52 properties: 50 compared, 2 not compared" - # Two of the 52 are not compared, and the count above is the only place that + # 45 -> 49 with agent-guardrails, 49 -> 52 with deployment, 52 -> 56 with + # payments, and this line is where each of those had to be said out loud. + has "cross-check: all 56 properties of the twenty scenarios were considered" \ + "$out" "considered 56 properties: 54 compared, 2 not compared" + # Two of the 56 are not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit and expense-approval # each ask one property under a fairness assumption, which ct.rules §8 does # not encode. @@ -459,9 +459,9 @@ crosscheck() { # measured. If it ever reads "unexercised" again, a scenario went missing. # two-phase-commit's atomicity is the third; the entitlement problems bring # four more, since "nobody ever holds X" is how an access rule is said, and - # expense-approval, agent-guardrails and deployment one each. + # expense-approval, agent-guardrails and deployment one each, payments two. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 10 properties compared" + "never: 12 properties compared" # And `inevitable`, two of whose three are two-phase-commit's — the newest # modality, and the one whose second implementation is newest, so the line # that says it is being compared at all is worth having. The third is @@ -810,9 +810,39 @@ deployment() { has "deployment: the migration" "$dv" " migrate" } +payments() { + d="$here/payments" + c="$d/payments.claims" + echo "== Payments — the reply that never comes, and the retry ==" + echo " Q: can a lost reply and a retry charge the customer twice?" + out=$("$WRIT" check "$d/payments.writ" --claims "$c" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "payments: with an idempotency key, the integration is clean" "$st" 0 + has "payments: A. a payment can settle" "$out" "holds settles" + has "payments: B. never charged twice" "$out" "holds never-double" + has "payments: C. a cancelled order is never left charged" "$out" "holds never-charged-for-nothing" + has "payments: and every order can still reach an end" "$out" "holds always-terminal" + lacks "payments: nothing is violated" "$out" "violated in" + + sc=$("$WRIT" check "$d/payments-shortcut.writ" --claims "$c" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "payments: without the key, the integration is refused" "$sst" 1 + has "payments: D. a lost reply and a retry charge twice" "$sc" \ + "violated in 13 reachable situations witness: 1. authorize 2. send-capture 3. capture 4. lose-reply 5. send-capture 6. capture-again" + has "payments: E. and a void that overtakes the capture charges for a cancelled order" "$sc" "fails never-charged-for-nothing" + near "payments: the void lands first, with nothing to refund" "$sc" "fails never-charged-for-nothing" "4. void-uncaptured" + near "payments: then the capture" "$sc" "fails never-charged-for-nothing" "5. capture" + has "payments: F. yet it still settles" "$sc" "holds settles" + + dv=$("$WRIT" derive "$d/payments-shortcut.writ" "$d/payments.rules" double-charged 2>&1) + has "payments: G. double charges hide in orders that settled and shipped" "$dv" "settled yes" +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver expense_approval agent_guardrails deployment payments control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):"