17. Money recorded on an order🔗

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

rule

Rules.OneOrder.Change.settle (l : Rules.OneOrder.Change.Ledger)
  (d : Rules.OneOrder.Change.PriceDifferential) :
  Rules.OneOrder.Change.Ledger
Rules.OneOrder.Change.settle
  (l : Rules.OneOrder.Change.Ledger)
  (d :
    Rules.OneOrder.Change.PriceDifferential) :
  Rules.OneOrder.Change.Ledger

EARS: When a seller settles a change or cancellation offer, the system shall record on the order what the customer paid, what the airline returned, the penalty and the forfeited amount.

Story: As a revenue accountant, I want every settled change recorded on the order, so that I can reconcile the order's items against its payments and refunds.

Acceptance criteria:

ONE-205.1: When a seller settles a change or cancellation offer, the system shall add the amount due to the airline to the order's payments and the amount due by the airline to its refunds.
ONE-205.2: When a seller settles a change or cancellation offer, the system shall add its penalty and forfeited amount to the totals recorded on the order and lower no total recorded before.
ONE-205.3: When a seller settles a paid change of an order item, the system shall keep the order's payments less refunds equal to the price of its live items plus the recorded penalties and forfeited amounts.

The penalties and forfeited amounts are kept at order level, as the guide records them from release 24.1, so they stay when the item they came from is replaced. The model keeps totals; the guide's individual records with their links to order items are not modelled.

17.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-205.1	Proven	Change balance, Settling adds to payments and refunds
ONE-205.2	Proven	Change balance, Settling records penalties and forfeits
ONE-205.3	Open	Change balance, Order balance after servicing

17.2. Guarantees🔗

17.2.1. Settling adds to payments and refunds🔗

guarantee

Rules.OneOrder.Change.settle_adds_payments
  (l : Rules.OneOrder.Change.Ledger)
  (d : Rules.OneOrder.Change.PriceDifferential) :
  (Rules.OneOrder.Change.settle l d).paid =
      l.paid + d.dueToAirline.amount ∧
    (Rules.OneOrder.Change.settle l d).refunded =
      l.refunded + d.dueByAirline.amount
Rules.OneOrder.Change.settle_adds_payments
  (l : Rules.OneOrder.Change.Ledger)
  (d :
    Rules.OneOrder.Change.PriceDifferential) :
  (Rules.OneOrder.Change.settle l
          d).paid =
      l.paid + d.dueToAirline.amount ∧
    (Rules.OneOrder.Change.settle l
          d).refunded =
      l.refunded + d.dueByAirline.amount

Settling an offer adds the amount due to the airline to the payments and the amount due by the airline to the refunds.

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

Checks acceptance criteria ONE-205.1.

17.2.2. Settling records penalties and forfeits🔗

guarantee

Rules.OneOrder.Change.settle_records_penalty
  (l : Rules.OneOrder.Change.Ledger)
  (d : Rules.OneOrder.Change.PriceDifferential) :
  (Rules.OneOrder.Change.settle l d).penalties =
      l.penalties + d.penalty.amount ∧
    (Rules.OneOrder.Change.settle l d).forfeited =
        l.forfeited + d.forfeited.amount ∧
      l.paid ≤ (Rules.OneOrder.Change.settle l d).paid ∧
        l.refunded ≤ (Rules.OneOrder.Change.settle l d).refunded ∧
          l.penalties ≤ (Rules.OneOrder.Change.settle l d).penalties ∧
            l.forfeited ≤ (Rules.OneOrder.Change.settle l d).forfeited
Rules.OneOrder.Change.settle_records_penalty
  (l : Rules.OneOrder.Change.Ledger)
  (d :
    Rules.OneOrder.Change.PriceDifferential) :
  (Rules.OneOrder.Change.settle l
          d).penalties =
      l.penalties + d.penalty.amount ∧
    (Rules.OneOrder.Change.settle l
            d).forfeited =
        l.forfeited + d.forfeited.amount ∧
      l.paid ≤
          (Rules.OneOrder.Change.settle l
              d).paid ∧
        l.refunded ≤
            (Rules.OneOrder.Change.settle
                l d).refunded ∧
          l.penalties ≤
              (Rules.OneOrder.Change.settle
                  l d).penalties ∧
            l.forfeited ≤
              (Rules.OneOrder.Change.settle
                  l d).forfeited

Settling an offer adds its penalty and forfeited amount to those recorded, and never lowers an amount recorded before.

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

Checks acceptance criteria ONE-205.2.

17.2.3. Order balance after servicing🔗

guarantee

Rules.OneOrder.Change.change_keeps_balance
  (m : Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (r : Rules.OneOrder.Change.ExcessPenalty)
  (o o' : Rules.OneOrder.Order) (c : Rules.OneOrder.Change.ItemChange)
  (old : Rules.OneOrder.OrderItem)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (d : Rules.OneOrder.Change.PriceDifferential)
  (l : Rules.OneOrder.Change.Ledger)
  (hbal : Rules.OneOrder.Change.Ledger.Balanced v o l)
  (hold :
    List.find? (fun x ↦ decide (x.id = c.item)) o.items = some old)
  (hc : Rules.OneOrder.Change.changeItem m o c = Except.ok o')
  (hprices : q.oldPrice = old.price ∧ q.newPrice = c.newPrice)
  (hd : Rules.OneOrder.Change.priceDifferential r q = Except.ok d) :
  Rules.OneOrder.Change.Ledger.Balanced v o'
    (Rules.OneOrder.Change.settle l d)
Rules.OneOrder.Change.change_keeps_balance
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (o o' : Rules.OneOrder.Order)
  (c : Rules.OneOrder.Change.ItemChange)
  (old : Rules.OneOrder.OrderItem)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (d :
    Rules.OneOrder.Change.PriceDifferential)
  (l : Rules.OneOrder.Change.Ledger)
  (hbal :
    Rules.OneOrder.Change.Ledger.Balanced
      v o l)
  (hold :
    List.find?
        (fun x ↦ decide (x.id = c.item))
        o.items =
      some old)
  (hc :
    Rules.OneOrder.Change.changeItem m o
        c =
      Except.ok o')
  (hprices :
    q.oldPrice = old.price ∧
      q.newPrice = c.newPrice)
  (hd :
    Rules.OneOrder.Change.priceDifferential
        r q =
      Except.ok d) :
  Rules.OneOrder.Change.Ledger.Balanced v
    o' (Rules.OneOrder.Change.settle l d)

A balanced order stays balanced when a paid change of one of its items is made and its price differential settled, under every reading of the guide.

Open question for the business. After a change that keeps a service, the original item still holds value (see ONE-204.5), so its price still counts as live next to the new item's price. The example changeBalance shows it: a 1,000.00 trip changed to a 900.00 trip keeping the outbound flight, with a 40.00 penalty and 120.00 forfeited, leaves 1,060.00 paid against 1,900.00 of live items plus 160.00 recorded. The same change with nothing kept balances. A request to keep value for later use, or a waived penalty above the refundable value, breaks it too, for the reasons given under ONE-201.5. Should the original item stop counting once the change is paid, and how does a change accepted but not yet paid enter the balance?

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

Checks acceptance criteria ONE-205.3.

17.3. Examples🔗

17.3.1. Change balance🔗

example

Rules.OneOrder.Change.changeBalance :
  List Rules.OneOrder.Change.BalanceRow
Rules.OneOrder.Change.changeBalance :
  List Rules.OneOrder.Change.BalanceRow

Given the trip order, paid 1,000.00 EUR and ready to proceed, with nothing refunded and nothing recorded. It is balanced.

When the seller accepts and pays a change to a 900.00 EUR trip with a 40.00 EUR penalty and 120.00 EUR forfeited, the figures of worked example EXM_ORD_003C. The change keeps the outbound flight, or keeps nothing.

Then the customer pays 60.00 EUR more either way. With nothing kept, the order balances: 1,060.00 EUR paid equals 900.00 EUR of live items plus 160.00 EUR recorded. With the outbound flight kept, the original item still counts as live, and the order does not balance.

What Lean computed:

Stage	Paid	Live items	Penalties	Forfeited	Balanced
before the change	1000.00 EUR	1000.00 EUR	0.00 EUR	0.00 EUR	yes
after a change keeping the outbound flight	1060.00 EUR	1900.00 EUR	40.00 EUR	120.00 EUR	no
after a change keeping nothing	1060.00 EUR	900.00 EUR	40.00 EUR	120.00 EUR	yes

Checks acceptance criteria ONE-205.1, ONE-205.2, ONE-205.3.

17.4. Open question🔗

The guarantee Order balance after servicing is open: the example Change balance shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.