18. Paying with several methods🔗

Requirement ONE-301. Of its 4 acceptance criteria, 4 are proven.

rule

Rules.OneOrder.Payment.Transaction.status
  (p : Rules.OneOrder.Payment.Transaction) :
  Rules.OneOrder.Payment.PaymentStatus
Rules.OneOrder.Payment.Transaction.status
  (p :
    Rules.OneOrder.Payment.Transaction) :
  Rules.OneOrder.Payment.PaymentStatus

EARS: The system shall give a payment the status FAILED if it has no payment method or the transaction of any of its payment methods failed, SUCCESSFUL if all of them succeeded, and PENDING otherwise.

Story: As an airline, I want a payment made with several methods to succeed only when every method succeeds, so that I never treat an order item as paid when part of its money will not arrive.

Acceptance criteria:

ONE-301.1: If the transaction of any payment method in a payment fails, then the system shall mark the whole payment FAILED.
ONE-301.2: When a payment has at least one payment method and the transactions of all its payment methods succeed, the system shall mark the payment SUCCESSFUL.
ONE-301.3: While no payment method's transaction in a payment has failed and at least one is still pending, the system shall mark the payment PENDING.
ONE-301.4: If a payment has no payment method, then the system shall mark it FAILED.

The guide describes a payment as made with one or more payment methods. A payment with none collects nothing, so it is FAILED. Without that case, every method of an empty payment would count as succeeded, and the payment with them.

18.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-301.1	Proven	Status from methods, A failed method fails the payment, Declined card for bag
ONE-301.2	Proven	Status from methods, A payment succeeds when every method succeeds
ONE-301.3	Proven	Status from methods, A payment is pending while a method is pending
ONE-301.4	Proven	Payment without method, Status without method

18.2. Guarantees🔗

18.2.1. A failed method fails the payment🔗

guarantee

Rules.OneOrder.Payment.status_failed_iff
  (p : Rules.OneOrder.Payment.Transaction) :
  p.status = Rules.OneOrder.Payment.PaymentStatus.failed ↔
    p.parts = [] ∨
      ∃ m ∈ p.parts,
        m.status = Rules.OneOrder.Payment.PaymentStatus.failed
Rules.OneOrder.Payment.status_failed_iff
  (p :
    Rules.OneOrder.Payment.Transaction) :
  p.status =
      Rules.OneOrder.Payment.PaymentStatus.failed ↔
    p.parts = [] ∨
      ∃ m ∈ p.parts,
        m.status =
          Rules.OneOrder.Payment.PaymentStatus.failed

A payment is FAILED exactly when it has no payment method or the transaction of at least one of its payment methods failed.

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

Checks acceptance criteria ONE-301.1.

18.2.2. A payment succeeds when every method succeeds🔗

guarantee

Rules.OneOrder.Payment.status_successful_iff
  (p : Rules.OneOrder.Payment.Transaction) :
  p.status = Rules.OneOrder.Payment.PaymentStatus.successful ↔
    p.parts ≠ [] ∧
      ∀ m ∈ p.parts,
        m.status = Rules.OneOrder.Payment.PaymentStatus.successful
Rules.OneOrder.Payment.status_successful_iff
  (p :
    Rules.OneOrder.Payment.Transaction) :
  p.status =
      Rules.OneOrder.Payment.PaymentStatus.successful ↔
    p.parts ≠ [] ∧
      ∀ m ∈ p.parts,
        m.status =
          Rules.OneOrder.Payment.PaymentStatus.successful

A payment is SUCCESSFUL exactly when it has at least one payment method and the transactions of all its payment methods succeeded.

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

Checks acceptance criteria ONE-301.2.

18.2.3. A payment is pending while a method is pending🔗

guarantee

Rules.OneOrder.Payment.status_pending_iff
  (p : Rules.OneOrder.Payment.Transaction) :
  p.status = Rules.OneOrder.Payment.PaymentStatus.pending ↔
    (∀ m ∈ p.parts,
        m.status ≠ Rules.OneOrder.Payment.PaymentStatus.failed) ∧
      ∃ m ∈ p.parts,
        m.status = Rules.OneOrder.Payment.PaymentStatus.pending
Rules.OneOrder.Payment.status_pending_iff
  (p :
    Rules.OneOrder.Payment.Transaction) :
  p.status =
      Rules.OneOrder.Payment.PaymentStatus.pending ↔
    (∀ m ∈ p.parts,
        m.status ≠
          Rules.OneOrder.Payment.PaymentStatus.failed) ∧
      ∃ m ∈ p.parts,
        m.status =
          Rules.OneOrder.Payment.PaymentStatus.pending

A payment is PENDING exactly when no method's transaction failed and at least one is still pending.

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

Checks acceptance criteria ONE-301.3.

18.2.4. Status without method🔗

guarantee

Rules.OneOrder.Payment.status_without_method
  (p : Rules.OneOrder.Payment.Transaction) (h : p.parts = []) :
  p.status = Rules.OneOrder.Payment.PaymentStatus.failed
Rules.OneOrder.Payment.status_without_method
  (p : Rules.OneOrder.Payment.Transaction)
  (h : p.parts = []) :
  p.status =
    Rules.OneOrder.Payment.PaymentStatus.failed

A payment with no payment method is FAILED, so it never counts an order item as paid.

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

Checks acceptance criteria ONE-301.4.

18.3. Examples🔗

18.3.1. Declined card for bag🔗

example

Rules.OneOrder.Payment.declinedCardForBag :
  Rules.OneOrder.Payment.OrderView
Rules.OneOrder.Payment.declinedCardForBag :
  Rules.OneOrder.Payment.OrderView

Given the trip at 100.00 EUR and the bag at 40.00 EUR, both unpaid.

When the seller pays for both in one payment: 100.00 EUR by settlement plan, which succeeds, and 40.00 EUR by card, which is declined.

Then the whole payment fails. Neither item is paid, and their services stay confirmed with their payment time limits.

What Lean computed:

Payments: failed
Items: see the table below.

Items:

Item	Paid	Delivery	Time limit
TRIP	no	confirmed, confirmed	2026-10-27 12:00 UTC
BAG	no	confirmed	2026-10-27 12:00 UTC

Checks acceptance criteria ONE-301.1, ONE-302.3, ONE-305.3.

18.3.2. Status from methods🔗

example

Rules.OneOrder.Payment.statusFromMethods :
  List Rules.OneOrder.Payment.StatusRow
Rules.OneOrder.Payment.statusFromMethods :
  List Rules.OneOrder.Payment.StatusRow

Given the 100.00 EUR trip, paid with 20.00 EUR by settlement plan and 80.00 EUR by card in one payment.

When the two transactions have different outcomes.

Then the payment succeeds only when both succeed. It is pending while the card is still pending, and it fails as soon as either method fails.

What Lean computed:

Settlement plan	Card	Payment
successful	successful	successful
successful	pending	pending
pending	failed	failed
successful	failed	failed

Checks acceptance criteria ONE-301.1, ONE-301.2, ONE-301.3.

18.3.3. Payment without method🔗

example

Rules.OneOrder.Payment.paymentWithoutMethod :
  Rules.OneOrder.Payment.OrderView
Rules.OneOrder.Payment.paymentWithoutMethod :
  Rules.OneOrder.Payment.OrderView

Given the trip at 100.00 EUR, unpaid.

When a payment for the trip arrives that names no payment method.

Then the payment fails, because it collects nothing. The trip is not paid, and its flights stay confirmed with their payment time limit.

What Lean computed:

Payments: failed
Items: see the table below.

Items:

Item	Paid	Delivery	Time limit
TRIP	no	confirmed, confirmed	2026-10-27 12:00 UTC
BAG	no	confirmed	2026-10-27 12:00 UTC

Checks acceptance criteria ONE-301.4, ONE-302.2.