Verified Air

21. Accepting a payment🔗

Requirement ONE-304. Of its 7 acceptance criteria, 7 are proven.

🔗rule
Rules.OneOrder.Payment.acceptPayment
  (o : Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction) (now : Rules.Core.Instant) :
  Except Rules.OneOrder.Payment.PaymentRejection (List Rules.Core.Money)
Rules.OneOrder.Payment.acceptPayment
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction)
  (now : Rules.Core.Instant) :
  Except
    Rules.OneOrder.Payment.PaymentRejection
    (List Rules.Core.Money)

EARS: When a seller pays for order items, the system shall accept the payment only if it is made before the items' payment time limits and its requested amounts add up to their price, and shall charge each payment method its requested amount plus its surcharge.

Story: As an airline, I want each payment checked against the items it pays for, so that items are paid in full and on time, and each method is charged its amount plus its surcharge.

Acceptance criteria:

  • ONE-304.1: When the airline accepts a payment, the system shall charge each payment method its requested amount plus its surcharge.

  • ONE-304.2: If the requested amounts of a payment do not add up to the price of the order items it covers, then the system shall reject the payment.

  • ONE-304.3: When the airline accepts a payment, the system shall charge in total the price of the order items it covers plus the surcharges of its payment methods.

  • ONE-304.4: If a payment is made at or after the payment time limit of an order item it covers, then the system shall reject the payment.

  • ONE-304.5: If a payment uses the commitment method with an amount other than zero, then the system shall reject the payment.

  • ONE-304.6: If a payment uses the commitment method for order items with an amount to pay, then the system shall reject the payment.

  • ONE-304.7: If a payment has no payment method, then the system shall reject the payment.

The checks run in this order: payment time limits, a payment method present, currencies, commitment amounts, commitments for items with an amount to pay, and the requested total. The result is the amount charged to each method, in the order of the methods.

21.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-304.1

Proven

Split payment charges, Each method is charged its amount plus its surcharge

ONE-304.2

Proven

Surcharge counted as price, Requested amounts add up to the price

ONE-304.3

Proven

Amount charged across methods, Split payment charges

ONE-304.4

Proven

Payment after time limit, No payment at or after the time limit

ONE-304.5

Proven

Commitment for free seat, Commitment only when nothing due

ONE-304.6

Proven

Commitment for free seat, Commitment beside card, Commitment only when nothing due

ONE-304.7

Proven

Accept payment rejects without method

21.2. Guarantees🔗

21.2.1. Each method is charged its amount plus its surcharge🔗

🔗guarantee
Rules.OneOrder.Payment.acceptPayment_charges
  (o : Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction) (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h : Rules.OneOrder.Payment.acceptPayment o p now = Except.ok cs) :
  List.map some cs =
    List.map (fun m ↦ m.requested.add m.surcharge) p.parts
Rules.OneOrder.Payment.acceptPayment_charges
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction)
  (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h :
    Rules.OneOrder.Payment.acceptPayment o
        p now =
      Except.ok cs) :
  List.map some cs =
    List.map
      (fun m ↦
        m.requested.add m.surcharge)
      p.parts

An accepted payment charges each payment method its requested amount plus its surcharge: the two amounts added as money, in one currency, for every method in turn.

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

Checks acceptance criteria ONE-304.1.

21.2.2. Requested amounts add up to the price🔗

🔗guarantee
Rules.OneOrder.Payment.acceptPayment_requested_eq_price
  (o : Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction) (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h : Rules.OneOrder.Payment.acceptPayment o p now = Except.ok cs) :
  p.requestedTotal = Rules.OneOrder.Payment.priceTotal (o.coveredBy p)
Rules.OneOrder.Payment.acceptPayment_requested_eq_price
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction)
  (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h :
    Rules.OneOrder.Payment.acceptPayment o
        p now =
      Except.ok cs) :
  p.requestedTotal =
    Rules.OneOrder.Payment.priceTotal
      (o.coveredBy p)

An accepted payment's requested amounts add up to the price of the order items it covers.

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

Checks acceptance criteria ONE-304.2.

21.2.3. Amount charged across methods🔗

🔗guarantee
Rules.OneOrder.Payment.acceptPayment_total
  (o : Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction) (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h : Rules.OneOrder.Payment.acceptPayment o p now = Except.ok cs) :
  (List.map (fun x ↦ x.amount) cs).sum =
    Rules.OneOrder.Payment.priceTotal (o.coveredBy p) + p.surchargeTotal
Rules.OneOrder.Payment.acceptPayment_total
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction)
  (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h :
    Rules.OneOrder.Payment.acceptPayment o
        p now =
      Except.ok cs) :
  (List.map (fun x ↦ x.amount) cs).sum =
    Rules.OneOrder.Payment.priceTotal
        (o.coveredBy p) +
      p.surchargeTotal

An accepted payment charges in total the price of the order items it covers plus the surcharges of its payment methods.

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

Checks acceptance criteria ONE-304.3.

21.2.4. No payment at or after the time limit🔗

🔗guarantee
Rules.OneOrder.Payment.acceptPayment_rejects_after_time_limit
  (o : Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction) (now : Rules.Core.Instant)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.coveredBy p)
  (t : Rules.Core.Instant) (ht : pi.timeLimit = some t)
  (hle : now ≥ t) :
  Rules.OneOrder.Payment.acceptPayment o p now =
    Except.error Rules.OneOrder.Payment.PaymentRejection.timeLimitPassed
Rules.OneOrder.Payment.acceptPayment_rejects_after_time_limit
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction)
  (now : Rules.Core.Instant)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ o.coveredBy p)
  (t : Rules.Core.Instant)
  (ht : pi.timeLimit = some t)
  (hle : now ≥ t) :
  Rules.OneOrder.Payment.acceptPayment o p
      now =
    Except.error
      Rules.OneOrder.Payment.PaymentRejection.timeLimitPassed

A payment made at or after the payment time limit of an order item it covers is rejected.

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

Checks acceptance criteria ONE-304.4.

21.2.5. Commitment only when nothing due🔗

🔗guarantee
Rules.OneOrder.Payment.acceptPayment_commitment_zero
  (o : Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction) (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h : Rules.OneOrder.Payment.acceptPayment o p now = Except.ok cs)
  (m : Rules.OneOrder.Payment.MethodPart) (hm : m ∈ p.parts)
  (hc : m.method = Rules.OneOrder.Payment.Method.commitment) :
  m.requested.amount = 0 ∧
    m.surcharge.amount = 0 ∧
      ∀ pi ∈ o.coveredBy p, pi.item.price.amount = 0
Rules.OneOrder.Payment.acceptPayment_commitment_zero
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction)
  (now : Rules.Core.Instant)
  (cs : List Rules.Core.Money)
  (h :
    Rules.OneOrder.Payment.acceptPayment o
        p now =
      Except.ok cs)
  (m : Rules.OneOrder.Payment.MethodPart)
  (hm : m ∈ p.parts)
  (hc :
    m.method =
      Rules.OneOrder.Payment.Method.commitment) :
  m.requested.amount = 0 ∧
    m.surcharge.amount = 0 ∧
      ∀ pi ∈ o.coveredBy p,
        pi.item.price.amount = 0

In an accepted payment, a commitment method carries an amount and a surcharge of zero, and every order item the payment covers has nothing to pay.

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

Checks acceptance criteria ONE-304.5, ONE-304.6.

21.2.6. Accept payment rejects without method🔗

🔗guarantee
Rules.OneOrder.Payment.acceptPayment_rejects_without_method
  (o : Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction) (now : Rules.Core.Instant)
  (h : p.parts = []) (cs : List Rules.Core.Money) :
  Rules.OneOrder.Payment.acceptPayment o p now ≠ Except.ok cs
Rules.OneOrder.Payment.acceptPayment_rejects_without_method
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (p : Rules.OneOrder.Payment.Transaction)
  (now : Rules.Core.Instant)
  (h : p.parts = [])
  (cs : List Rules.Core.Money) :
  Rules.OneOrder.Payment.acceptPayment o p
      now ≠
    Except.ok cs

A payment with no payment method is never accepted.

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

Checks acceptance criteria ONE-304.7.

21.3. Examples🔗

21.3.1. Split payment charges🔗

🔗example
Rules.OneOrder.Payment.splitPaymentCharges :
  Except Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges
Rules.OneOrder.Payment.splitPaymentCharges :
  Except
    Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges

Given the trip at 100.00 EUR, unpaid, with its payment time limit an hour away.

When the seller pays 20.00 EUR by settlement plan and 80.00 EUR by card, on which the airline adds a 2.00 EUR surcharge.

Then the payment is accepted. The settlement plan is charged 20.00 EUR and the card 82.00 EUR, 102.00 EUR in all: the price plus the surcharge.

What Lean computed:

Accepted. The result:

  • Methods: see the table below.

  • Total: 102.00 EUR

Methods:

Method

Requested

Surcharge

Charged

settlement plan

20.00 EUR

0.00 EUR

20.00 EUR

card

80.00 EUR

2.00 EUR

82.00 EUR

Checks acceptance criteria ONE-304.1, ONE-304.3.

21.3.2. Surcharge counted as price🔗

🔗example
Rules.OneOrder.Payment.surchargeCountedAsPrice :
  Except Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges
Rules.OneOrder.Payment.surchargeCountedAsPrice :
  Except
    Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges

Given the trip at 100.00 EUR, unpaid, with its payment time limit an hour away.

When the seller requests 20.00 EUR from the settlement plan and 82.00 EUR from the card, counting the card's 2.00 EUR surcharge toward the price.

Then the payment is rejected: the requested amounts add up to 102.00 EUR, and the trip costs 100.00 EUR.

What Lean computed:

Rejected: amount mismatch.

Checks acceptance criteria ONE-304.2.

21.3.3. Payment after time limit🔗

🔗example
Rules.OneOrder.Payment.paymentAfterTimeLimit :
  Except Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges
Rules.OneOrder.Payment.paymentAfterTimeLimit :
  Except
    Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges

Given the trip at 100.00 EUR, unpaid, with a payment time limit of 2026-10-27 12:00 UTC.

When the seller pays for it in full at 12:01 UTC.

Then the payment is rejected because the time limit has passed.

What Lean computed:

Rejected: time limit passed.

Checks acceptance criteria ONE-304.4.

21.3.4. Commitment for free seat🔗

🔗example
Rules.OneOrder.Payment.commitmentForFreeSeat :
  Except Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges
Rules.OneOrder.Payment.commitmentForFreeSeat :
  Except
    Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges

Given the free seat, unpaid, with its payment time limit an hour away.

When the seller commits to pay for it with the commitment method and an amount of zero.

Then the payment is accepted, and nothing is charged.

What Lean computed:

Accepted. The result:

  • Methods: see the table below.

  • Total: 0.00 EUR

Methods:

Method

Requested

Surcharge

Charged

commitment

0.00 EUR

0.00 EUR

0.00 EUR

Checks acceptance criteria ONE-304.5, ONE-304.6.

21.3.5. Commitment beside card🔗

🔗example
Rules.OneOrder.Payment.commitmentBesideCard :
  Except Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges
Rules.OneOrder.Payment.commitmentBesideCard :
  Except
    Rules.OneOrder.Payment.PaymentRejection
    Rules.OneOrder.Payment.Charges

Given the bag at 40.00 EUR and the free seat, both unpaid, with their payment time limit an hour away.

When the seller pays for both in one payment: 40.00 EUR by card and a commitment of zero for the seat.

Then the payment is rejected: the commitment method may only cover items with nothing to pay, and the bag costs 40.00 EUR. A card payment of 40.00 EUR alone may cover both.

What Lean computed:

Rejected: commitment with amount due.

Checks acceptance criteria ONE-304.6.