22. Applying a payment outcome🔗

Requirement ONE-305. Of its 5 acceptance criteria, 5 are proven.

rule

Rules.OneOrder.Payment.applyOutcome
  (p : Rules.OneOrder.Payment.Transaction)
  (items : List Rules.OneOrder.Payment.PayableItem) :
  List Rules.OneOrder.Payment.PayableItem
Rules.OneOrder.Payment.applyOutcome
  (p : Rules.OneOrder.Payment.Transaction)
  (items :
    List
      Rules.OneOrder.Payment.PayableItem) :
  List Rules.OneOrder.Payment.PayableItem

EARS: When a payment becomes SUCCESSFUL, the system shall move every CONFIRMED service of the order items it covers to READY TO PROCEED and remove their payment time limits.

Story: As an airline, I want a successful payment to release the order items it paid for, so that their services can be delivered and are no longer at risk of removal.

Acceptance criteria:

ONE-305.1: When a payment is SUCCESSFUL, the system shall move every CONFIRMED service of the order items it covers to READY TO PROCEED.
ONE-305.2: When a payment is SUCCESSFUL, the system shall remove the payment time limits of the order items it covers.
ONE-305.3: If a payment is FAILED, then the system shall leave the services and payment time limits of the order items it covers unchanged.
ONE-305.4: While a payment is PENDING, the system shall leave the services and payment time limits of the order items it covers unchanged.
ONE-305.5: The system shall leave the order items a payment does not cover unchanged.

The guide states these effects for redirected payments. The model applies them to a payment of any method.

22.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-305.1	Proven	Two payments one declined, Effects of a payment outcome
ONE-305.2	Proven	Two payments one declined, Paid items lose their payment time limits
ONE-305.3	Proven	Two payments one declined, Failed and pending payments change nothing, Declined card for bag
ONE-305.4	Proven	Failed and pending payments change nothing, Pending redirect
ONE-305.5	Proven	Two payments one declined, Items a payment does not cover are unchanged

22.2. Guarantees🔗

22.2.1. Effects of a payment outcome🔗

guarantee

Rules.OneOrder.Payment.applyOutcome_ready
  (p : Rules.OneOrder.Payment.Transaction)
  (items : List Rules.OneOrder.Payment.PayableItem)
  (h : p.status = Rules.OneOrder.Payment.PaymentStatus.successful)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ items)
  (hc : pi.item.id ∈ p.covers) (s : Rules.OneOrder.Service)
  (hs : s ∈ pi.item.services)
  (hconf : s.delivery = Rules.OneOrder.DeliveryStatus.confirmed) :
  ∃ pi' ∈ Rules.OneOrder.Payment.applyOutcome p items,
    pi'.item.id = pi.item.id ∧
      { id := s.id, passenger := s.passenger, segment := s.segment,
          status := s.status,
          delivery := Rules.OneOrder.DeliveryStatus.readyToProceed } ∈
        pi'.item.services
Rules.OneOrder.Payment.applyOutcome_ready
  (p : Rules.OneOrder.Payment.Transaction)
  (items :
    List
      Rules.OneOrder.Payment.PayableItem)
  (h :
    p.status =
      Rules.OneOrder.Payment.PaymentStatus.successful)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ items)
  (hc : pi.item.id ∈ p.covers)
  (s : Rules.OneOrder.Service)
  (hs : s ∈ pi.item.services)
  (hconf :
    s.delivery =
      Rules.OneOrder.DeliveryStatus.confirmed) :
  ∃
    pi' ∈
      Rules.OneOrder.Payment.applyOutcome
        p items,
    pi'.item.id = pi.item.id ∧
      { id := s.id,
          passenger := s.passenger,
          segment := s.segment,
          status := s.status,
          delivery :=
            Rules.OneOrder.DeliveryStatus.readyToProceed } ∈
        pi'.item.services

When a payment is SUCCESSFUL, each CONFIRMED service of an order item it covers is READY TO PROCEED afterwards.

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

Checks acceptance criteria ONE-305.1.

22.2.2. Paid items lose their payment time limits🔗

guarantee

Rules.OneOrder.Payment.applyOutcome_no_time_limit
  (p : Rules.OneOrder.Payment.Transaction)
  (items : List Rules.OneOrder.Payment.PayableItem)
  (h : p.status = Rules.OneOrder.Payment.PaymentStatus.successful)
  (pi : Rules.OneOrder.Payment.PayableItem) :
  pi ∈ Rules.OneOrder.Payment.applyOutcome p items →
    pi.item.id ∈ p.covers → pi.timeLimit = none
Rules.OneOrder.Payment.applyOutcome_no_time_limit
  (p : Rules.OneOrder.Payment.Transaction)
  (items :
    List
      Rules.OneOrder.Payment.PayableItem)
  (h :
    p.status =
      Rules.OneOrder.Payment.PaymentStatus.successful)
  (pi :
    Rules.OneOrder.Payment.PayableItem) :
  pi ∈
      Rules.OneOrder.Payment.applyOutcome
        p items →
    pi.item.id ∈ p.covers →
      pi.timeLimit = none

When a payment is SUCCESSFUL, no order item it covers has a payment time limit afterwards.

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

Checks acceptance criteria ONE-305.2.

22.2.3. Failed and pending payments change nothing🔗

guarantee

Rules.OneOrder.Payment.applyOutcome_unsuccessful
  (p : Rules.OneOrder.Payment.Transaction)
  (items : List Rules.OneOrder.Payment.PayableItem)
  (h : p.status ≠ Rules.OneOrder.Payment.PaymentStatus.successful) :
  Rules.OneOrder.Payment.applyOutcome p items = items
Rules.OneOrder.Payment.applyOutcome_unsuccessful
  (p : Rules.OneOrder.Payment.Transaction)
  (items :
    List
      Rules.OneOrder.Payment.PayableItem)
  (h :
    p.status ≠
      Rules.OneOrder.Payment.PaymentStatus.successful) :
  Rules.OneOrder.Payment.applyOutcome p
      items =
    items

A payment that is not SUCCESSFUL, whether FAILED or PENDING, leaves every order item as it was.

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

Checks acceptance criteria ONE-305.3, ONE-305.4.

22.2.4. Items a payment does not cover are unchanged🔗

guarantee

Rules.OneOrder.Payment.applyOutcome_uncovered
  (p : Rules.OneOrder.Payment.Transaction)
  (items : List Rules.OneOrder.Payment.PayableItem) :
  List.filter (fun pi ↦ decide (pi.item.id ∉ p.covers))
      (Rules.OneOrder.Payment.applyOutcome p items) =
    List.filter (fun pi ↦ decide (pi.item.id ∉ p.covers)) items
Rules.OneOrder.Payment.applyOutcome_uncovered
  (p : Rules.OneOrder.Payment.Transaction)
  (items :
    List
      Rules.OneOrder.Payment.PayableItem) :
  List.filter
      (fun pi ↦
        decide (pi.item.id ∉ p.covers))
      (Rules.OneOrder.Payment.applyOutcome
        p items) =
    List.filter
      (fun pi ↦
        decide (pi.item.id ∉ p.covers))
      items

A payment's outcome leaves the order items it does not cover as they were.

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

Checks acceptance criteria ONE-305.5.

22.3. Examples🔗

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

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

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