Verified Air

49. Net clearance amount🔗

Requirement ONE-802. Of its 6 acceptance criteria, 5 are proven and 1 is open.

🔗rule
Rules.OneOrder.Accounting.clearancesFor
  (p : Rules.OneOrder.Accounting.PaymentCommitment) :
  List Rules.OneOrder.Accounting.ClearanceLeg
Rules.OneOrder.Accounting.clearancesFor
  (p :
    Rules.OneOrder.Accounting.PaymentCommitment) :
  List
    Rules.OneOrder.Accounting.ClearanceLeg

EARS: When a payment commitment is made, the system shall state the clearances between the ORA and the seller for it, with their net clearance amounts.

Story: As a seller, I want each payment cleared with the ORA by one rule, so that I receive my commission once and the airline receives the rest.

Acceptance criteria:

  • ONE-802.1: When the seller collected the customer's payment and nets its commission, the system shall state one clearance in which the seller pays the ORA the payment amount less the commission.

  • ONE-802.2: When the seller collected the customer's payment and its commission is cleared separately, the system shall state one clearance in which the seller pays the ORA the payment amount and one in which the ORA pays the seller the commission.

  • ONE-802.3: When the airline collected the customer's payment, the system shall state one clearance in which the ORA pays the seller the commission.

  • ONE-802.4: The system shall clear the seller's commission on each payment exactly once, leaving the ORA the payment amount less the commission and the seller the commission.

  • ONE-802.5: When a payment is refunded through the seller, the system shall state one clearance in which the ORA pays the seller the refund less the commission recalled on it.

  • ONE-802.6: If a payment is refunded through the seller, then the system shall not leave the seller paying the ORA for the refund.

The standard defines the net clearance amount only as what the two parties agreed; the formulas come from the worked examples. A refund is cleared by refundClearance, and how much commission it recalls is a reading of the sources (RecallReading).

49.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-802.1

Proven

Commission cleared once, Seller collects and nets the commission

ONE-802.2

Proven

Commission cleared once, Seller collects, commission cleared separately

ONE-802.3

Proven

Airline collects, Commission cleared once

ONE-802.4

Proven

Commission cleared once, Commission cleared exactly once

ONE-802.5

Proven

Refund through the seller, Refund clearances

ONE-802.6

Open

Refund clearances, Seller never pays for a refund

49.2. Guarantees🔗

49.2.1. Seller collects and nets the commission🔗

🔗guarantee
Rules.OneOrder.Accounting.seller_collected_netted
  (p : Rules.OneOrder.Accounting.PaymentCommitment)
  (hc : p.collector = Rules.OneOrder.Accounting.Collector.seller)
  (hh :
    p.handling = Rules.OneOrder.Accounting.CommissionHandling.netted) :
  Rules.OneOrder.Accounting.clearancesFor p =
    [{ payer := Rules.OneOrder.Accounting.Role.seller,
        payee := Rules.OneOrder.Accounting.Role.ora,
        amount := ↑p.amount - ↑p.commission }]
Rules.OneOrder.Accounting.seller_collected_netted
  (p :
    Rules.OneOrder.Accounting.PaymentCommitment)
  (hc :
    p.collector =
      Rules.OneOrder.Accounting.Collector.seller)
  (hh :
    p.handling =
      Rules.OneOrder.Accounting.CommissionHandling.netted) :
  Rules.OneOrder.Accounting.clearancesFor
      p =
    [{
        payer :=
          Rules.OneOrder.Accounting.Role.seller,
        payee :=
          Rules.OneOrder.Accounting.Role.ora,
        amount :=
          ↑p.amount - ↑p.commission }]

A payment the seller collected, with the commission netted, gives one clearance: the seller pays the ORA the payment amount less the commission.

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

Checks acceptance criteria ONE-802.1.

49.2.2. Seller collects, commission cleared separately🔗

🔗guarantee
Rules.OneOrder.Accounting.seller_collected_separate
  (p : Rules.OneOrder.Accounting.PaymentCommitment)
  (hc : p.collector = Rules.OneOrder.Accounting.Collector.seller)
  (hh :
    p.handling =
      Rules.OneOrder.Accounting.CommissionHandling.separate) :
  Rules.OneOrder.Accounting.clearancesFor p =
    [{ payer := Rules.OneOrder.Accounting.Role.seller,
        payee := Rules.OneOrder.Accounting.Role.ora,
        amount := ↑p.amount },
      { payer := Rules.OneOrder.Accounting.Role.ora,
        payee := Rules.OneOrder.Accounting.Role.seller,
        amount := ↑p.commission }]
Rules.OneOrder.Accounting.seller_collected_separate
  (p :
    Rules.OneOrder.Accounting.PaymentCommitment)
  (hc :
    p.collector =
      Rules.OneOrder.Accounting.Collector.seller)
  (hh :
    p.handling =
      Rules.OneOrder.Accounting.CommissionHandling.separate) :
  Rules.OneOrder.Accounting.clearancesFor
      p =
    [{
        payer :=
          Rules.OneOrder.Accounting.Role.seller,
        payee :=
          Rules.OneOrder.Accounting.Role.ora,
        amount := ↑p.amount },
      {
        payer :=
          Rules.OneOrder.Accounting.Role.ora,
        payee :=
          Rules.OneOrder.Accounting.Role.seller,
        amount := ↑p.commission }]

A payment the seller collected, with the commission cleared separately, gives two clearances: the seller pays the ORA the payment amount, and the ORA pays the seller the commission.

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

Checks acceptance criteria ONE-802.2.

49.2.3. Airline collects🔗

🔗guarantee
Rules.OneOrder.Accounting.airline_collected
  (p : Rules.OneOrder.Accounting.PaymentCommitment)
  (hc : p.collector = Rules.OneOrder.Accounting.Collector.airline) :
  Rules.OneOrder.Accounting.clearancesFor p =
    [{ payer := Rules.OneOrder.Accounting.Role.ora,
        payee := Rules.OneOrder.Accounting.Role.seller,
        amount := ↑p.commission }]
Rules.OneOrder.Accounting.airline_collected
  (p :
    Rules.OneOrder.Accounting.PaymentCommitment)
  (hc :
    p.collector =
      Rules.OneOrder.Accounting.Collector.airline) :
  Rules.OneOrder.Accounting.clearancesFor
      p =
    [{
        payer :=
          Rules.OneOrder.Accounting.Role.ora,
        payee :=
          Rules.OneOrder.Accounting.Role.seller,
        amount := ↑p.commission }]

A payment the airline collected gives one clearance: the ORA pays the seller the commission.

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

Checks acceptance criteria ONE-802.3.

49.2.4. Commission cleared exactly once🔗

🔗guarantee
Rules.OneOrder.Accounting.commission_cleared_once
  (p : Rules.OneOrder.Accounting.PaymentCommitment) :
  p.endsWith Rules.OneOrder.Accounting.Role.ora =
      ↑p.amount - ↑p.commission ∧
    p.endsWith Rules.OneOrder.Accounting.Role.seller = ↑p.commission
Rules.OneOrder.Accounting.commission_cleared_once
  (p :
    Rules.OneOrder.Accounting.PaymentCommitment) :
  p.endsWith
        Rules.OneOrder.Accounting.Role.ora =
      ↑p.amount - ↑p.commission ∧
    p.endsWith
        Rules.OneOrder.Accounting.Role.seller =
      ↑p.commission

However the customer's money was collected and the commission cleared, the ORA ends with the payment amount less the commission and the seller with the commission: the commission is cleared exactly once.

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

Checks acceptance criteria ONE-802.4.

49.2.5. Refund through the seller🔗

🔗guarantee
Rules.OneOrder.Accounting.refund_cleared
  (rr : Rules.OneOrder.Accounting.RecallReading)
  (r : Rules.OneOrder.Accounting.SellerRefund) :
  Rules.OneOrder.Accounting.refundClearance rr r =
    { payer := Rules.OneOrder.Accounting.Role.ora,
      payee := Rules.OneOrder.Accounting.Role.seller,
      amount := ↑r.refund - ↑(rr.recalled r) }
Rules.OneOrder.Accounting.refund_cleared
  (rr :
    Rules.OneOrder.Accounting.RecallReading)
  (r :
    Rules.OneOrder.Accounting.SellerRefund) :
  Rules.OneOrder.Accounting.refundClearance
      rr r =
    {
      payer :=
        Rules.OneOrder.Accounting.Role.ora,
      payee :=
        Rules.OneOrder.Accounting.Role.seller,
      amount :=
        ↑r.refund - ↑(rr.recalled r) }

A refund through the seller gives one clearance: the ORA pays the seller the refund less the commission recalled on it, under every reading.

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

Checks acceptance criteria ONE-802.5.

49.2.6. Seller never pays for a refund🔗

🔗guarantee
Rules.OneOrder.Accounting.refund_not_paid_by_seller
  (rr : Rules.OneOrder.Accounting.RecallReading)
  (r : Rules.OneOrder.Accounting.SellerRefund)
  (hrefund : r.refund ≤ r.payment) (hcomm : r.commission ≤ r.payment) :
  0 ≤ (Rules.OneOrder.Accounting.refundClearance rr r).amount
Rules.OneOrder.Accounting.refund_not_paid_by_seller
  (rr :
    Rules.OneOrder.Accounting.RecallReading)
  (r :
    Rules.OneOrder.Accounting.SellerRefund)
  (hrefund : r.refund ≤ r.payment)
  (hcomm : r.commission ≤ r.payment) :
  0 ≤
    (Rules.OneOrder.Accounting.refundClearance
        rr r).amount

The clearance for a refund through the seller never has the seller paying the ORA: its amount is never negative.

Open question for the business. Under the reading that recalls the commission first paid in full on any refund, a partial refund smaller than that commission gives a negative amount. The example refundClearances shows it: a 5.00 refund of a 75.00 payment that carried 7.50 of commission leaves the seller paying the ORA 2.50. Recalling no commission, or the share that matches the share refunded, never does (refund_clearance_nonneg_without_full_recall). How much commission is recalled on a partial refund?

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

Checks acceptance criteria ONE-802.6.

49.3. Examples🔗

49.3.1. Commission cleared once🔗

🔗example
Rules.OneOrder.Accounting.commissionClearedOnce :
  List Rules.OneOrder.Accounting.PaymentClearing
Rules.OneOrder.Accounting.commissionClearedOnce :
  List
    Rules.OneOrder.Accounting.PaymentClearing

Given a payment of 410.00 EUR with a seller's commission of 41.00 EUR.

When the payment is cleared in three ways: the seller collects it through EasyPay and nets the commission; the seller collects it and the commission is cleared separately; the airline collects it by card.

Then netted, the seller pays the ORA 369.00 EUR. Separately, the seller pays 410.00 EUR and the ORA pays back 41.00 EUR. Collected by the airline, the ORA pays the seller 41.00 EUR. Each way the ORA ends with 369.00 EUR and the seller with 41.00 EUR: the commission is cleared once.

What Lean computed:

Case

Clearances

Ora ends with

Seller ends with

seller collects, commission netted

payer seller, payee ora, amount 36900

36900

4100

seller collects, commission separate

payer seller, payee ora, amount 41000, payer ora, payee seller, amount 4100

36900

4100

airline collects

payer ora, payee seller, amount 4100

36900

4100

Checks acceptance criteria ONE-802.1, ONE-802.2, ONE-802.3, ONE-802.4.

49.3.2. Refund clearances🔗

🔗example
Rules.OneOrder.Accounting.refundClearances :
  List Rules.OneOrder.Accounting.RefundRow
Rules.OneOrder.Accounting.refundClearances :
  List Rules.OneOrder.Accounting.RefundRow

Given a payment of 75.00 EUR, made through the seller, that carried a commission of 7.50 EUR. These are the figures of the source's refund example.

When it is refunded in full through the seller, and when 5.00 EUR of it is refunded.

Then for the full refund the ORA pays the seller 75.00 EUR if no commission is recalled and 67.50 EUR otherwise. For the partial refund it pays 5.00 EUR with no recall and 4.50 EUR with proportional recall. With the commission recalled in full the amount is minus 2.50 EUR: the seller pays the ORA for the customer's refund.

What Lean computed:

Refund

No recall

Full

Proportional

7500

7500

6750

6750

500

500

-250

450

Checks acceptance criteria ONE-802.5, ONE-802.6.

49.4. Open question🔗

The guarantee Seller never pays for a refund is open: the example Refund clearances shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.