Verified Air

56. Accounting for paid services🔗

Requirement ONE-809. Of its 6 acceptance criteria, 3 are proven and 3 are open.

🔗rule
Rules.OneOrder.Accounting.bookStep (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (b : Rules.OneOrder.Accounting.ServiceBooks) : Rules.OneOrder.Accounting.BookEvent → Option Rules.OneOrder.Accounting.ServiceBooks
Rules.OneOrder.Accounting.bookStep (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (b : Rules.OneOrder.Accounting.ServiceBooks) : Rules.OneOrder.Accounting.BookEvent → Option Rules.OneOrder.Accounting.ServiceBooks

EARS: The system shall hold the amount paid for a service as a liability until the service reaches a final delivery status, and only then recognize it as revenue.

Story: As a revenue accountant, I want revenue recognized only when a service reaches a final status, and every payment accounted for, so that the books of each order balance.

Acceptance criteria:

  • ONE-809.1: While a paid service has not reached a final delivery status, the system shall hold the amount paid for it as a liability and recognize none of it as revenue.

  • ONE-809.2: When a paid service is DELIVERED, the system shall recognize the amount paid for it as revenue.

  • ONE-809.3: When a paid service reaches a final delivery status, the system shall hold none of the amount paid for it as a liability.

  • ONE-809.4: The system shall keep each order's payments equal to its refunds, plus the amount held as liability, plus the revenue recognized, plus the forfeited amounts.

  • ONE-809.5: The system shall never refund more for an order than was paid for it.

  • ONE-809.6: Where the airline checks the amounts of a cancellation, the system shall refuse a report whose refund, penalty and forfeited amount do not add up to the amount paid for the service.

The final statuses are those of ONE-103 (isFinal). Whether a final status other than DELIVERED earns revenue, refunds the amount paid or keeps it as a liability, and whether a penalty is recognized at cancellation, are a reading of the sources (RevenueReading). Payments for a service in a final status are refused, and a service is cancelled only before it reaches one. The sources send payments, refunds, penalties and forfeited amounts to accounting but state no balance, and do not say whether the amounts of a cancellation must add up to what was paid; that is a reading too (CancelCheck). The result is the books afterwards, or none when the event is refused.

56.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-809.1

Proven

Revenue recognized at final status, Delivered flight books

ONE-809.2

Proven

Delivered flight books, Delivered services earn revenue

ONE-809.3

Open

Cancel with penalty, No liability left at a final status, No show treatments

ONE-809.4

Open

Non refundable tax, Delivered flight books, Cancel with penalty, Goodwill refund, No show treatments, Money balance of an order, Cancel not adding up

ONE-809.5

Open

Non refundable tax, Refunds within payments, Cancel with penalty, Goodwill refund

ONE-809.6

Proven

Checking a cancellation's amounts, Goodwill refund, Cancel not adding up

56.2. Guarantees🔗

56.2.1. Revenue recognized at final status🔗

🔗guarantee
Rules.OneOrder.Accounting.liability_until_final (r : Rules.OneOrder.Accounting.RevenueReading) (b : Rules.OneOrder.Accounting.ServiceBooks) (h : Rules.OneOrder.Delivery.isFinal b.delivery = false) : Rules.OneOrder.Accounting.ServiceBooks.liability r b = b.paid ∧ Rules.OneOrder.Accounting.ServiceBooks.revenue r b = 0
Rules.OneOrder.Accounting.liability_until_final (r : Rules.OneOrder.Accounting.RevenueReading) (b : Rules.OneOrder.Accounting.ServiceBooks) (h : Rules.OneOrder.Delivery.isFinal b.delivery = false) : Rules.OneOrder.Accounting.ServiceBooks.liability r b = b.paid ∧ Rules.OneOrder.Accounting.ServiceBooks.revenue r b = 0

Until a service reaches a final delivery status, the whole amount paid for it is held as a liability and none of it is revenue, under every reading.

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

Checks acceptance criteria ONE-809.1.

56.2.2. Delivered services earn revenue🔗

🔗guarantee
Rules.OneOrder.Accounting.delivered_earns (r : Rules.OneOrder.Accounting.RevenueReading) (b : Rules.OneOrder.Accounting.ServiceBooks) (h : b.delivery = Rules.OneOrder.DeliveryStatus.delivered) : Rules.OneOrder.Accounting.ServiceBooks.revenue r b = b.paid
Rules.OneOrder.Accounting.delivered_earns (r : Rules.OneOrder.Accounting.RevenueReading) (b : Rules.OneOrder.Accounting.ServiceBooks) (h : b.delivery = Rules.OneOrder.DeliveryStatus.delivered) : Rules.OneOrder.Accounting.ServiceBooks.revenue r b = b.paid

The amount paid for a delivered service is revenue, under every reading.

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

Checks acceptance criteria ONE-809.2.

56.2.3. No liability left at a final status🔗

🔗guarantee
Rules.OneOrder.Accounting.final_status_no_liability (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (b b' : Rules.OneOrder.Accounting.ServiceBooks) (e : Rules.OneOrder.Accounting.BookEvent) (h : Rules.OneOrder.Accounting.bookStep r k b e = some b') (hf : Rules.OneOrder.Delivery.isFinal b'.delivery = true) : Rules.OneOrder.Accounting.ServiceBooks.liability r b' = 0
Rules.OneOrder.Accounting.final_status_no_liability (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (b b' : Rules.OneOrder.Accounting.ServiceBooks) (e : Rules.OneOrder.Accounting.BookEvent) (h : Rules.OneOrder.Accounting.bookStep r k b e = some b') (hf : Rules.OneOrder.Delivery.isFinal b'.delivery = true) : Rules.OneOrder.Accounting.ServiceBooks.liability r b' = 0

When a service reaches a final delivery status, none of the amount paid for it is held as a liability.

Open question for the business. The sources do not say which final statuses earn revenue. Under a reading that keeps the amount paid for a no-show as a liability, or that does not recognize a penalty when a cancellation is reported, money stays a liability on a service that will never change again. The examples noShowTreatments and cancelWithPenalty show it. For DELIVERED, NOT CLAIMED, EXPIRED and FAILED TO DELIVER, does the amount paid earn revenue, go back as a refund or stay a liability, and when is a penalty reported at cancellation recognized?

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

Checks acceptance criteria ONE-809.3.

56.2.4. Money balance of an order🔗

🔗guarantee
Rules.OneOrder.Accounting.order_books_balance (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (ids : List String) (es : List (String × Rules.OneOrder.Accounting.BookEvent)) : (Rules.OneOrder.Accounting.OrderBooks.totals r (Rules.OneOrder.Accounting.OrderBooks.run r k (List.map Rules.OneOrder.Accounting.ServiceBooks.new ids) es)).Balanced
Rules.OneOrder.Accounting.order_books_balance (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (ids : List String) (es : List (String × Rules.OneOrder.Accounting.BookEvent)) : (Rules.OneOrder.Accounting.OrderBooks.totals r (Rules.OneOrder.Accounting.OrderBooks.run r k (List.map Rules.OneOrder.Accounting.ServiceBooks.new ids) es)).Balanced

Whatever accounting is told about an order's services, its payments equal its refunds, plus the amount held as liability, plus the revenue recognized, plus the forfeited amounts.

Open question for the business. Under the reading where accounting records a cancellation as the airline sends it, a refund, penalty and forfeited amount that do not add up to what was paid break the balance. The examples goodwillRefund and cancelNotAddingUp show it: a goodwill refund of 120.00 on a 100.00 flight leaves 100.00 paid against 120.00 refunded. Where the airline checks the amounts, the balance holds (order_books_balance_of_checked). Must the amounts of a cancellation add up to what was paid, and if not, where does the difference go?

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

Checks acceptance criteria ONE-809.4.

56.2.5. Refunds within payments🔗

🔗guarantee
Rules.OneOrder.Accounting.refunds_within_payments (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (ids : List String) (es : List (String × Rules.OneOrder.Accounting.BookEvent)) : (Rules.OneOrder.Accounting.OrderBooks.totals r (Rules.OneOrder.Accounting.OrderBooks.run r k (List.map Rules.OneOrder.Accounting.ServiceBooks.new ids) es)).refunded ≤ (Rules.OneOrder.Accounting.OrderBooks.totals r (Rules.OneOrder.Accounting.OrderBooks.run r k (List.map Rules.OneOrder.Accounting.ServiceBooks.new ids) es)).paid
Rules.OneOrder.Accounting.refunds_within_payments (r : Rules.OneOrder.Accounting.RevenueReading) (k : Rules.OneOrder.Accounting.CancelCheck) (ids : List String) (es : List (String × Rules.OneOrder.Accounting.BookEvent)) : (Rules.OneOrder.Accounting.OrderBooks.totals r (Rules.OneOrder.Accounting.OrderBooks.run r k (List.map Rules.OneOrder.Accounting.ServiceBooks.new ids) es)).refunded ≤ (Rules.OneOrder.Accounting.OrderBooks.totals r (Rules.OneOrder.Accounting.OrderBooks.run r k (List.map Rules.OneOrder.Accounting.ServiceBooks.new ids) es)).paid

Whatever accounting is told about an order's services, it never refunds more than was paid.

Open question for the business. Under the reading where accounting records a cancellation as the airline sends it, nothing stops a refund larger than what was paid. The example goodwillRefund shows it: a goodwill refund of 120.00 on a flight paid at 100.00. Where the airline checks the amounts, a refund never exceeds what was paid (refunds_within_payments_of_checked). May a refund exceed what was paid, for example as goodwill, and how is the excess accounted for?

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

Checks acceptance criteria ONE-809.5.

56.2.6. Checking a cancellation's amounts🔗

🔗guarantee
Rules.OneOrder.Accounting.cancel_must_add_up (r : Rules.OneOrder.Accounting.RevenueReading) (b : Rules.OneOrder.Accounting.ServiceBooks) (rf pen forf : ℕ) (h : rf + pen + forf ≠ b.paid) : Rules.OneOrder.Accounting.bookStep r Rules.OneOrder.Accounting.CancelCheck.checked b (Rules.OneOrder.Accounting.BookEvent.cancel rf pen forf) = none
Rules.OneOrder.Accounting.cancel_must_add_up (r : Rules.OneOrder.Accounting.RevenueReading) (b : Rules.OneOrder.Accounting.ServiceBooks) (rf pen forf : ℕ) (h : rf + pen + forf ≠ b.paid) : Rules.OneOrder.Accounting.bookStep r Rules.OneOrder.Accounting.CancelCheck.checked b (Rules.OneOrder.Accounting.BookEvent.cancel rf pen forf) = none

Where the airline checks the amounts of a cancellation, a report whose refund, penalty and forfeited amount do not add up to the amount paid for the service is refused, under every reading of revenue.

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

Checks acceptance criteria ONE-809.6.

56.3. Examples🔗

56.3.1. Delivered flight books🔗

🔗example
Rules.OneOrder.Accounting.deliveredFlightBooks : Rules.OneOrder.Accounting.BookSteps
Rules.OneOrder.Accounting.deliveredFlightBooks : Rules.OneOrder.Accounting.BookSteps

Given an order with one flight paid at 100.00 EUR.

When the passenger flies and the flight is reported DELIVERED.

Then after the payment the 100.00 EUR is a liability. Once the flight is delivered it is revenue. At each step payments equal refunds, plus liability, plus revenue, plus forfeited amounts.

What Lean computed:

  • After payment: paid 10000, refunded 0, liability 10000, revenue 0, forfeited 0

  • At end: paid 10000, refunded 0, liability 0, revenue 10000, forfeited 0

Checks acceptance criteria ONE-809.1, ONE-809.2, ONE-809.4.

56.3.2. Cancel with penalty🔗

🔗example
Rules.OneOrder.Accounting.cancelWithPenalty : Rules.OneOrder.Accounting.PenaltyBooks
Rules.OneOrder.Accounting.cancelWithPenalty : Rules.OneOrder.Accounting.PenaltyBooks

Given an order with one flight paid at 100.00 EUR.

When the customer cancels with a penalty of 25.00 EUR, receives 75.00 EUR, and the flight is removed.

Then where the penalty is recognized at cancellation, it is 25.00 EUR of revenue. Where it is not, the 25.00 EUR stays a liability on a flight that can no longer change, since no delivery will ever recognize it. The books balance either way, and nothing is refunded beyond what was paid.

What Lean computed:

  • Penalty earned: paid 10000, refunded 7500, liability 0, revenue 2500, forfeited 0

  • Penalty not earned: paid 10000, refunded 7500, liability 2500, revenue 0, forfeited 0

Checks acceptance criteria ONE-809.3, ONE-809.4, ONE-809.5.

56.3.3. No show treatments🔗

🔗example
Rules.OneOrder.Accounting.noShowTreatments : Rules.OneOrder.Accounting.NoShowBooks
Rules.OneOrder.Accounting.noShowTreatments : Rules.OneOrder.Accounting.NoShowBooks

Given an order with one flight paid at 100.00 EUR.

When the passenger does not show and the flight is reported NOT CLAIMED.

Then depending on the reading, the 100.00 EUR is revenue, is refunded, or stays a liability on a flight that can no longer change. The books balance under all three.

What Lean computed:

  • Earn: paid 10000, refunded 0, liability 0, revenue 10000, forfeited 0

  • Refund: paid 10000, refunded 10000, liability 0, revenue 0, forfeited 0

  • Keep: paid 10000, refunded 0, liability 10000, revenue 0, forfeited 0

Checks acceptance criteria ONE-809.3, ONE-809.4.

56.3.4. Cancel not adding up🔗

🔗example
Rules.OneOrder.Accounting.cancelNotAddingUp : Rules.OneOrder.Accounting.CheckedOrAsSent
Rules.OneOrder.Accounting.cancelNotAddingUp : Rules.OneOrder.Accounting.CheckedOrAsSent

Given an order with one flight paid at 100.00 EUR.

When a cancellation is reported with a refund of 100.00 EUR and a penalty of 25.00 EUR, which add up to more than was paid.

Then where the airline checks the amounts, the report is refused and the flight is still a 100.00 EUR liability. Where accounting records it as sent, the books show 100.00 EUR paid against 100.00 EUR refunded and 25.00 EUR of revenue: they do not balance.

What Lean computed:

  • Checked: paid 10000, refunded 0, liability 10000, revenue 0, forfeited 0

  • As sent: paid 10000, refunded 10000, liability 0, revenue 2500, forfeited 0

Checks acceptance criteria ONE-809.4, ONE-809.6.

56.3.5. Goodwill refund🔗

🔗example
Rules.OneOrder.Accounting.goodwillRefund : Rules.OneOrder.Accounting.CheckedOrAsSent
Rules.OneOrder.Accounting.goodwillRefund : Rules.OneOrder.Accounting.CheckedOrAsSent

Given an order with one flight paid at 100.00 EUR.

When the airline cancels it and reports a goodwill refund of 120.00 EUR.

Then where the airline checks the amounts, the report is refused. Where accounting records it as sent, 120.00 EUR is refunded against 100.00 EUR paid: the refunds exceed the payments and the books do not balance.

What Lean computed:

  • Checked: paid 10000, refunded 0, liability 10000, revenue 0, forfeited 0

  • As sent: paid 10000, refunded 12000, liability 0, revenue 0, forfeited 0

Checks acceptance criteria ONE-809.4, ONE-809.5, ONE-809.6.

56.3.6. Non refundable tax🔗

🔗example
Rules.OneOrder.Accounting.nonRefundableTax : Rules.OneOrder.Accounting.OrderTotals
Rules.OneOrder.Accounting.nonRefundableTax : Rules.OneOrder.Accounting.OrderTotals

Given an order with one flight paid at 100.00 EUR, of which 10.00 EUR is a non-refundable tax.

When the customer cancels and receives 90.00 EUR.

Then the books record 90.00 EUR refunded and 10.00 EUR forfeited, and they balance: 100.00 EUR paid equals 90.00 EUR refunded plus 10.00 EUR forfeited.

What Lean computed:

  • Paid: 10000

  • Refunded: 9000

  • Liability: 0

  • Revenue: 0

  • Forfeited: 1000

Checks acceptance criteria ONE-809.4, ONE-809.5.

56.4. Open question🔗

The guarantee No liability left at a final status is open: the example Cancel with penalty, No show treatments shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

56.5. Open question🔗

The guarantee Money balance of an order is open: the example Delivered flight books, Cancel with penalty, No show treatments, Cancel not adding up, Goodwill refund, Non refundable tax shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

56.6. Open question🔗

The guarantee Refunds within payments is open: the example Cancel with penalty, Goodwill refund, Non refundable tax shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.