20. Payment status and its moves🔗

Requirement ONE-303. Of its 3 acceptance criteria, 2 are proven and 1 is open.

rule

Rules.OneOrder.Payment.recordOutcome
  (r : Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction) (ref : String)
  (s : Rules.OneOrder.Payment.PaymentStatus) :
  Rules.OneOrder.Payment.Transaction
Rules.OneOrder.Payment.recordOutcome
  (r :
    Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction)
  (ref : String)
  (s :
    Rules.OneOrder.Payment.PaymentStatus) :
  Rules.OneOrder.Payment.Transaction

EARS: When the airline reports the outcome of a payment method's transaction, the system shall record it as the transaction's status if the move from the recorded status is allowed.

Story: As an airline, I want the outcome of each payment method's transaction recorded as it arrives, so that a payment's status follows what I know about its funds.

Acceptance criteria:

ONE-303.1: When the airline reports a SUCCESSFUL or FAILED outcome for a payment method's transaction that is still PENDING, the system shall record the outcome.
ONE-303.2: When the airline reports the outcome of one payment method's transaction, the system shall leave the transactions of the payment's other methods unchanged.
ONE-303.3: The system shall never change the status of a payment that is SUCCESSFUL or FAILED.

Which moves are allowed besides those out of PENDING is a reading of the guide (see OutcomeReading).

20.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
ONE-303.1	Proven	Outcomes of pending transactions are recorded, Redirect completes
ONE-303.2	Proven	Redirect completes, Other methods keep their outcomes
ONE-303.3	Open	Chargeback, Late redirect capture, Settled payments keep their status

20.2. Guarantees🔗

20.2.1. Outcomes of pending transactions are recorded🔗

guarantee

Rules.OneOrder.Payment.recordOutcome_pending
  (r : Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction) (ref : String)
  (s : Rules.OneOrder.Payment.PaymentStatus)
  (hs : s ≠ Rules.OneOrder.Payment.PaymentStatus.pending)
  (m : Rules.OneOrder.Payment.MethodPart) (hm : m ∈ p.parts)
  (hid : m.id = ref)
  (hp : m.status = Rules.OneOrder.Payment.PaymentStatus.pending) :
  { id := m.id, method := m.method, requested := m.requested,
      surcharge := m.surcharge, status := s } ∈
    (Rules.OneOrder.Payment.recordOutcome r p ref s).parts
Rules.OneOrder.Payment.recordOutcome_pending
  (r :
    Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction)
  (ref : String)
  (s :
    Rules.OneOrder.Payment.PaymentStatus)
  (hs :
    s ≠
      Rules.OneOrder.Payment.PaymentStatus.pending)
  (m : Rules.OneOrder.Payment.MethodPart)
  (hm : m ∈ p.parts) (hid : m.id = ref)
  (hp :
    m.status =
      Rules.OneOrder.Payment.PaymentStatus.pending) :
  { id := m.id, method := m.method,
      requested := m.requested,
      surcharge := m.surcharge,
      status := s } ∈
    (Rules.OneOrder.Payment.recordOutcome
        r p ref s).parts

When the airline reports that a method's pending transaction succeeded or failed, the outcome is recorded, under every reading of the guide.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-303.1.

20.2.2. Other methods keep their outcomes🔗

guarantee

Rules.OneOrder.Payment.recordOutcome_other_methods
  (r : Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction) (ref : String)
  (s : Rules.OneOrder.Payment.PaymentStatus)
  (m : Rules.OneOrder.Payment.MethodPart) (hm : m ∈ p.parts)
  (hid : m.id ≠ ref) :
  m ∈ (Rules.OneOrder.Payment.recordOutcome r p ref s).parts
Rules.OneOrder.Payment.recordOutcome_other_methods
  (r :
    Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction)
  (ref : String)
  (s :
    Rules.OneOrder.Payment.PaymentStatus)
  (m : Rules.OneOrder.Payment.MethodPart)
  (hm : m ∈ p.parts) (hid : m.id ≠ ref) :
  m ∈
    (Rules.OneOrder.Payment.recordOutcome
        r p ref s).parts

Reporting the outcome of one method's transaction leaves the transactions of the payment's other methods as they were.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-303.2.

20.2.3. Settled payments keep their status🔗

guarantee

Rules.OneOrder.Payment.recordOutcome_settled_final
  (r : Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction) (ref : String)
  (s : Rules.OneOrder.Payment.PaymentStatus)
  (h :
    p.status = Rules.OneOrder.Payment.PaymentStatus.successful ∨
      p.status = Rules.OneOrder.Payment.PaymentStatus.failed) :
  (Rules.OneOrder.Payment.recordOutcome r p ref s).status = p.status
Rules.OneOrder.Payment.recordOutcome_settled_final
  (r :
    Rules.OneOrder.Payment.OutcomeReading)
  (p : Rules.OneOrder.Payment.Transaction)
  (ref : String)
  (s :
    Rules.OneOrder.Payment.PaymentStatus)
  (h :
    p.status =
        Rules.OneOrder.Payment.PaymentStatus.successful ∨
      p.status =
        Rules.OneOrder.Payment.PaymentStatus.failed) :
  (Rules.OneOrder.Payment.recordOutcome r
        p ref s).status =
    p.status

A SUCCESSFUL or FAILED payment keeps its status whatever outcome the airline later reports for one of its methods.

Open question for the business. The guide says a PENDING payment moves to SUCCESSFUL or FAILED and does not say whether either is final. Under a reading where a card chargeback turns a successful transaction into a failed one, a SUCCESSFUL payment becomes FAILED; the example chargeback shows it. Under a reading where a redirected payment completed after the airline marked it failed is recorded, a FAILED payment becomes SUCCESSFUL; the example lateRedirectCapture shows it. Can a SUCCESSFUL payment later fail, can a FAILED payment later succeed, and what then happens to the order items it covers?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-303.3.

20.3. Examples🔗

20.3.1. Redirect completes🔗

example

Rules.OneOrder.Payment.redirectCompletes :
  Rules.OneOrder.Payment.Recorded
Rules.OneOrder.Payment.redirectCompletes :
  Rules.OneOrder.Payment.Recorded

Given the trip payment: 20.00 EUR by settlement plan, already successful, and 80.00 EUR by card through a redirect, still pending.

When the customer completes the redirect and the airline reports the card transaction successful.

Then the card transaction is recorded as successful, the settlement plan transaction is unchanged, and the payment becomes successful.

What Lean computed:

Methods: see the table below.
Payment before: pending
Payment after: successful

Methods:

Transaction	Method	Before	After
TX-1	settlement plan	successful	successful
TX-2	card	pending	successful

Checks acceptance criteria ONE-303.1, ONE-303.2.

20.3.2. Chargeback🔗

example

Rules.OneOrder.Payment.chargeback : Rules.OneOrder.Payment.Readings
Rules.OneOrder.Payment.chargeback :
  Rules.OneOrder.Payment.Readings

Given the trip paid by card, with a successful payment.

When the card holder disputes the charge and the airline reports the card transaction failed.

Then under the final reading the payment stays successful. Under the chargeback reading, where a successful transaction may later fail, the payment becomes failed.

What Lean computed:

Before: successful
Under final reading: successful
Under other reading: failed

Checks acceptance criteria ONE-303.3.

20.3.3. Late redirect capture🔗

example

Rules.OneOrder.Payment.lateRedirectCapture :
  Rules.OneOrder.Payment.LateCapture
Rules.OneOrder.Payment.lateRedirectCapture :
  Rules.OneOrder.Payment.LateCapture

Given the trip at 100.00 EUR, unpaid, with a redirected card payment for it still pending.

When the payment time limit passes, and one minute later the customer completes the redirect and the airline reports the card transaction successful.

Then at the limit the trip is removed and the payment fails. Under the final reading the late report changes nothing. Under the late capture reading the payment becomes successful, but the trip's flights stay removed: the customer has paid for nothing.

What Lean computed:

Payment at limit: failed
Trip at limit: removed, removed
Under final reading: failed
Under late capture reading: successful
Trip after capture: removed, removed

Checks acceptance criteria ONE-303.3, ONE-306.1, ONE-306.2.

20.4. Open question🔗

The guarantee Settled payments keep their status is open: the example Chargeback, Late redirect capture shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.