Verified Air

54. Allocating a short remittance🔗

Requirement ONE-807. Of its 6 acceptance criteria, 4 are proven and 2 are open.

🔗rule
Rules.OneOrder.Accounting.allocate
  (a : Rules.OneOrder.Accounting.AllocationReading)
  (rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
  (os : List Rules.OneOrder.Accounting.Obligation) : List ℕ
Rules.OneOrder.Accounting.allocate
  (a :
    Rules.OneOrder.Accounting.AllocationReading)
  (rd :
    Rules.OneOrder.Accounting.Rounding)
  (paid : ℕ)
  (os :
    List
      Rules.OneOrder.Accounting.Obligation) :
  List ℕ

EARS: When a remittance payer pays short and the Clearance Manager has no credit line, the system shall split what was paid across the payer's clearances.

Story: As a settlement payee, I want a short remittance split by one known rule, so that I can tell which of my clearances were settled.

Acceptance criteria:

  • ONE-807.1: When a remittance payer pays short, the system shall settle no clearance for more than the payer owes on it.

  • ONE-807.2: When a remittance payer pays short, the system shall settle a clearance to a settlement payee only after every older clearance to that payee is settled in full.

  • ONE-807.3: Where the Clearance Manager follows the Remittance of Funds page, the system shall give each settlement payee its share of the payment in proportion to what it is owed, rounded to a minor unit and capped at what it is owed.

  • ONE-807.4: Where the Clearance Manager follows the Transfer of Funds page, the system shall apply the payment to the payer's clearances in the order they were recorded, whatever the payee.

  • ONE-807.5: When a remittance payer pays short, the system shall allocate the whole payment and no more.

  • ONE-807.6: If a remittance payer pays short, then the system shall settle each clearance for the same amount whichever source page the Clearance Manager follows.

The clearances are listed in the order they were recorded, oldest first. The page followed is a reading of the sources (AllocationReading), and so is the rounding of a proportional share (Rounding). The result lists the amount settled on each clearance.

54.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-807.1

Proven

Older clearances first, Short remittance within what is owed

ONE-807.2

Proven

Each payee's clearances oldest first, Older clearances first

ONE-807.3

Proven

Proportional shares, Two airlines

ONE-807.4

Proven

Oldest first across payees, Two airlines

ONE-807.5

Open

Whole payment allocated, Three payees

ONE-807.6

Open

One allocation for a short remittance, Two airlines

54.2. Guarantees🔗

54.2.1. Short remittance within what is owed🔗

🔗guarantee
Rules.OneOrder.Accounting.allocation_within_owed
  (a : Rules.OneOrder.Accounting.AllocationReading)
  (rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
  (os : List Rules.OneOrder.Accounting.Obligation) :
  List.Forall₂ (fun x o ↦ x ≤ o.owed)
    (Rules.OneOrder.Accounting.allocate a rd paid os) os
Rules.OneOrder.Accounting.allocation_within_owed
  (a :
    Rules.OneOrder.Accounting.AllocationReading)
  (rd :
    Rules.OneOrder.Accounting.Rounding)
  (paid : ℕ)
  (os :
    List
      Rules.OneOrder.Accounting.Obligation) :
  List.Forall₂ (fun x o ↦ x ≤ o.owed)
    (Rules.OneOrder.Accounting.allocate a
      rd paid os)
    os

No clearance is settled for more than the payer owes on it, under every reading and every rounding.

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

Checks acceptance criteria ONE-807.1.

54.2.2. Each payee's clearances oldest first🔗

🔗guarantee
Rules.OneOrder.Accounting.allocation_oldest_first_per_payee
  (a : Rules.OneOrder.Accounting.AllocationReading)
  (rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
  (os : List Rules.OneOrder.Accounting.Obligation) :
  Rules.OneOrder.Accounting.OldestFirst (fun x ↦ x.payee)
    (os.zip (Rules.OneOrder.Accounting.allocate a rd paid os))
Rules.OneOrder.Accounting.allocation_oldest_first_per_payee
  (a :
    Rules.OneOrder.Accounting.AllocationReading)
  (rd :
    Rules.OneOrder.Accounting.Rounding)
  (paid : ℕ)
  (os :
    List
      Rules.OneOrder.Accounting.Obligation) :
  Rules.OneOrder.Accounting.OldestFirst
    (fun x ↦ x.payee)
    (os.zip
      (Rules.OneOrder.Accounting.allocate
        a rd paid os))

The clearances to each settlement payee are settled oldest first, under every reading and every rounding.

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

Checks acceptance criteria ONE-807.2.

54.2.3. Proportional shares🔗

🔗guarantee
Rules.OneOrder.Accounting.proportional_share_settled
  (rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
  (os : List Rules.OneOrder.Accounting.Obligation) (payee : String) :
  (List.map (fun x ↦ x.2)
        (List.filter (fun p ↦ decide (p.1.payee = payee))
          (os.zip
            (Rules.OneOrder.Accounting.allocate
              Rules.OneOrder.Accounting.AllocationReading.proportional
              rd paid os)))).sum =
    min (Rules.OneOrder.Accounting.share rd paid os payee)
      (Rules.OneOrder.Accounting.owedTo os payee)
Rules.OneOrder.Accounting.proportional_share_settled
  (rd :
    Rules.OneOrder.Accounting.Rounding)
  (paid : ℕ)
  (os :
    List
      Rules.OneOrder.Accounting.Obligation)
  (payee : String) :
  (List.map (fun x ↦ x.2)
        (List.filter
          (fun p ↦
            decide (p.1.payee = payee))
          (os.zip
            (Rules.OneOrder.Accounting.allocate
              Rules.OneOrder.Accounting.AllocationReading.proportional
              rd paid os)))).sum =
    min
      (Rules.OneOrder.Accounting.share rd
        paid os payee)
      (Rules.OneOrder.Accounting.owedTo os
        payee)

Under the Remittance of Funds page, each settlement payee's clearances are settled for its proportional share of the payment, capped at what it is owed, under every rounding.

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

Checks acceptance criteria ONE-807.3.

54.2.4. Oldest first across payees🔗

🔗guarantee
Rules.OneOrder.Accounting.transfer_oldest_first
  (rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
  (os : List Rules.OneOrder.Accounting.Obligation) :
  Rules.OneOrder.Accounting.OldestFirst (fun x ↦ ())
    (os.zip
      (Rules.OneOrder.Accounting.allocate
        Rules.OneOrder.Accounting.AllocationReading.oldestFirst rd paid
        os))
Rules.OneOrder.Accounting.transfer_oldest_first
  (rd :
    Rules.OneOrder.Accounting.Rounding)
  (paid : ℕ)
  (os :
    List
      Rules.OneOrder.Accounting.Obligation) :
  Rules.OneOrder.Accounting.OldestFirst
    (fun x ↦ ())
    (os.zip
      (Rules.OneOrder.Accounting.allocate
        Rules.OneOrder.Accounting.AllocationReading.oldestFirst
        rd paid os))

Under the Transfer of Funds page, the payer's clearances are settled in the order they were recorded, whatever the payee, under every rounding.

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

Checks acceptance criteria ONE-807.4.

54.2.5. Whole payment allocated🔗

🔗guarantee
Rules.OneOrder.Accounting.allocation_whole_payment
  (a : Rules.OneOrder.Accounting.AllocationReading)
  (rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
  (os : List Rules.OneOrder.Accounting.Obligation)
  (hshort : paid ≤ Rules.OneOrder.Accounting.totalOwed os) :
  (Rules.OneOrder.Accounting.allocate a rd paid os).sum = paid
Rules.OneOrder.Accounting.allocation_whole_payment
  (a :
    Rules.OneOrder.Accounting.AllocationReading)
  (rd :
    Rules.OneOrder.Accounting.Rounding)
  (paid : ℕ)
  (os :
    List
      Rules.OneOrder.Accounting.Obligation)
  (hshort :
    paid ≤
      Rules.OneOrder.Accounting.totalOwed
        os) :
  (Rules.OneOrder.Accounting.allocate a rd
        paid os).sum =
    paid

A short payment is allocated in full and no more: the amounts settled add up to what was paid.

Open question for the business. Under the Remittance of Funds page each settlement payee's share has to be rounded to a minor unit, and the rounded shares need not add up to the payment. The example threePayees shows it: 100.00 split between three payees owed 100.00 each settles 99.99 when shares are rounded down and 100.02 when they are rounded up. Under the Transfer of Funds page the whole payment is allocated (transfer_allocates_all). How is a proportional share rounded, and who receives the remainder?

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

Checks acceptance criteria ONE-807.5.

54.2.6. One allocation for a short remittance🔗

🔗guarantee
Rules.OneOrder.Accounting.one_allocation
  (rd : Rules.OneOrder.Accounting.Rounding) (paid : ℕ)
  (os : List Rules.OneOrder.Accounting.Obligation)
  (hshort : paid < Rules.OneOrder.Accounting.totalOwed os) :
  Rules.OneOrder.Accounting.allocate
      Rules.OneOrder.Accounting.AllocationReading.proportional rd paid
      os =
    Rules.OneOrder.Accounting.allocate
      Rules.OneOrder.Accounting.AllocationReading.oldestFirst rd paid os
Rules.OneOrder.Accounting.one_allocation
  (rd :
    Rules.OneOrder.Accounting.Rounding)
  (paid : ℕ)
  (os :
    List
      Rules.OneOrder.Accounting.Obligation)
  (hshort :
    paid <
      Rules.OneOrder.Accounting.totalOwed
        os) :
  Rules.OneOrder.Accounting.allocate
      Rules.OneOrder.Accounting.AllocationReading.proportional
      rd paid os =
    Rules.OneOrder.Accounting.allocate
      Rules.OneOrder.Accounting.AllocationReading.oldestFirst
      rd paid os

A short payment settles each clearance for the same amount under either source page.

Open question for the business. The Remittance of Funds page splits a short payment across the settlement payees in proportion to what each is owed; the Transfer of Funds page applies it to the payer's obligations in the order they were recorded, whatever the payee. The example twoAirlines shows them differ: a payer owing airline A 100.00 (older) and airline B 100.00 (newer) pays 100.00, and A and B receive 50.00 each under the first page and 100.00 and nothing under the second. Which allocation does the Clearance Manager use?

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

Checks acceptance criteria ONE-807.6.

54.3. Examples🔗

54.3.1. Older clearances first🔗

🔗example
Rules.OneOrder.Accounting.olderClearancesFirst :
  Rules.OneOrder.Accounting.ShortRemittance
Rules.OneOrder.Accounting.olderClearancesFirst :
  Rules.OneOrder.Accounting.ShortRemittance

Given a remittance payer that owes airline A 60.00 EUR on its oldest clearance, airline B 80.00 EUR on the next, and airline A 60.00 EUR on the newest, and pays 100.00 EUR, with no credit line.

When the Clearance Manager splits the payment.

Then under both pages A's older clearance is settled in full, B receives 40.00 EUR and A's newer clearance nothing. Under Remittance of Funds, A's share of 60.00 EUR goes to its older clearance first. No clearance gets more than it is owed.

What Lean computed:

  • Proportional: 6000, 4000, 0

  • Oldest first: 6000, 4000, 0

Checks acceptance criteria ONE-807.1, ONE-807.2.

54.3.2. Two airlines🔗

🔗example
Rules.OneOrder.Accounting.twoAirlines :
  Rules.OneOrder.Accounting.ShortRemittance
Rules.OneOrder.Accounting.twoAirlines :
  Rules.OneOrder.Accounting.ShortRemittance

Given a remittance payer that owes airline A 100.00 EUR on an older clearance and airline B 100.00 EUR on a newer one, and pays 100.00 EUR, with no credit line.

When the Clearance Manager splits the payment.

Then under the Remittance of Funds page A and B receive 50.00 EUR each. Under the Transfer of Funds page A receives 100.00 EUR and B nothing. The two pages give different results.

What Lean computed:

  • Proportional: 5000, 5000

  • Oldest first: 10000, 0

Checks acceptance criteria ONE-807.3, ONE-807.4, ONE-807.6.

54.3.3. Three payees🔗

🔗example
Rules.OneOrder.Accounting.threePayees :
  Rules.OneOrder.Accounting.AllocatedTotals
Rules.OneOrder.Accounting.threePayees :
  Rules.OneOrder.Accounting.AllocatedTotals

Given a remittance payer that owes three airlines 100.00 EUR each and pays 100.00 EUR, with no credit line.

When the Clearance Manager splits the payment.

Then under the Remittance of Funds page each share is 33.333 EUR. Rounded down, the airlines receive 33.33 EUR each and 0.01 EUR is not allocated. Rounded up, they receive 33.34 EUR each, 0.02 EUR more than was paid. Under the Transfer of Funds page the first airline receives all 100.00 EUR.

What Lean computed:

  • Proportional down: 3333, 3333, 3333, 9999

  • Proportional up: 3334, 3334, 3334, 10002

  • Oldest first: 10000, 0, 0, 10000

Checks acceptance criteria ONE-807.5.

54.4. Open question🔗

The guarantee Whole payment allocated is open: the example Three payees shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

54.5. Open question🔗

The guarantee One allocation for a short remittance is open: the example Two airlines shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.