19. Paid order item🔗

Requirement ONE-302. Of its 3 acceptance criteria, 3 are proven.

rule

Rules.OneOrder.Payment.isPaid
  (payments : List Rules.OneOrder.Payment.Transaction) (ref : String) :
  Bool
Rules.OneOrder.Payment.isPaid
  (payments :
    List
      Rules.OneOrder.Payment.Transaction)
  (ref : String) : Bool

EARS: The system shall count an order item paid once a SUCCESSFUL payment covers it.

Story: As an airline, I want an order item counted as paid only when a payment for it has succeeded, so that I release nothing on money I may not collect.

Acceptance criteria:

ONE-302.1: When a SUCCESSFUL payment covers an order item, the system shall count the item paid.
ONE-302.2: If every payment covering an order item is PENDING or FAILED, then the system shall not count the item paid.
ONE-302.3: If the transaction of any payment method in a payment fails, then the system shall count none of the order items it covers as paid by that payment and shall leave their services unchanged.

The amounts are checked when the payment is accepted: the requested amounts of a payment add up to the price of the items it covers. Value carried over from an item that a change replaced is not modelled.

19.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-302.1	Proven	Two payments one declined, Only successful payments pay
ONE-302.2	Proven	Payment without method, Two payments one declined, Only successful payments pay, Pending redirect
ONE-302.3	Proven	Failed payment leaves items unpaid, Declined card for bag

19.2. Guarantees🔗

19.2.1. Only successful payments pay🔗

guarantee

Rules.OneOrder.Payment.isPaid_iff
  (ps : List Rules.OneOrder.Payment.Transaction) (ref : String) :
  Rules.OneOrder.Payment.isPaid ps ref = true ↔
    ∃ p ∈ ps,
      p.status = Rules.OneOrder.Payment.PaymentStatus.successful ∧
        ref ∈ p.covers
Rules.OneOrder.Payment.isPaid_iff
  (ps :
    List
      Rules.OneOrder.Payment.Transaction)
  (ref : String) :
  Rules.OneOrder.Payment.isPaid ps ref =
      true ↔
    ∃ p ∈ ps,
      p.status =
          Rules.OneOrder.Payment.PaymentStatus.successful ∧
        ref ∈ p.covers

An order item is counted paid exactly when a SUCCESSFUL payment covers it: PENDING and FAILED payments never count.

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

Checks acceptance criteria ONE-302.1, ONE-302.2.

19.2.2. Failed payment leaves items unpaid🔗

guarantee

Rules.OneOrder.Payment.failed_method_pays_nothing
  (p : Rules.OneOrder.Payment.Transaction)
  (items : List Rules.OneOrder.Payment.PayableItem)
  (h :
    ∃ m ∈ p.parts,
      m.status = Rules.OneOrder.Payment.PaymentStatus.failed) :
  (∀ (ref : String), p.pays ref = false) ∧
    Rules.OneOrder.Payment.applyOutcome p items = items
Rules.OneOrder.Payment.failed_method_pays_nothing
  (p : Rules.OneOrder.Payment.Transaction)
  (items :
    List
      Rules.OneOrder.Payment.PayableItem)
  (h :
    ∃ m ∈ p.parts,
      m.status =
        Rules.OneOrder.Payment.PaymentStatus.failed) :
  (∀ (ref : String), p.pays ref = false) ∧
    Rules.OneOrder.Payment.applyOutcome p
        items =
      items

A payment with a failed method pays for none of the order items it covers, and its outcome leaves their services and payment time limits as they were. A seller who wants one item paid even if the method for another is declined must send two payments.

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

Checks acceptance criteria ONE-302.3.

19.3. Examples🔗

19.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.

19.3.2. 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.

19.3.3. Two payments one declined🔗

example

Rules.OneOrder.Payment.twoPaymentsOneDeclined :
  Rules.OneOrder.Payment.OrderView
Rules.OneOrder.Payment.twoPaymentsOneDeclined :
  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 them in two payments: the trip by settlement plan, which succeeds, and the bag by card, which is declined.

Then the trip is paid: its flights are ready to proceed and it has no payment time limit. The bag is not paid and is unchanged.

What Lean computed:

Payments: successful, failed
Items: see the table below.

Items:

Item	Paid	Delivery	Time limit
TRIP	yes	ready to proceed, ready to proceed	none
BAG	no	confirmed	2026-10-27 12:00 UTC

Checks acceptance criteria ONE-302.1, ONE-302.2, ONE-305.1, ONE-305.2, ONE-305.3, ONE-305.5.

19.3.4. Pending redirect🔗

example

Rules.OneOrder.Payment.pendingRedirect :
  Rules.OneOrder.Payment.OrderView
Rules.OneOrder.Payment.pendingRedirect :
  Rules.OneOrder.Payment.OrderView

Given the trip at 100.00 EUR, unpaid.

When the customer starts a redirected card payment for it and has not yet completed it.

Then the payment is pending, the trip is not paid, and its flights stay confirmed with their payment time limit.

What Lean computed:

Payments: pending
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-302.2, ONE-305.4.