Verified Air

48. Commission on an item🔗

Requirement ONE-801. Of its 5 acceptance criteria, 5 are proven.

rule

Rules.OneOrder.Accounting.commissionOwed
  (r : Rules.OneOrder.Accounting.Rounding) (c : Rules.Core.Currency)
  (cs : List Rules.OneOrder.Accounting.Commission) :
  Option Rules.Core.Money
Rules.OneOrder.Accounting.commissionOwed
  (r : Rules.OneOrder.Accounting.Rounding)
  (c : Rules.Core.Currency)
  (cs :
    List
      Rules.OneOrder.Accounting.Commission) :
  Option Rules.Core.Money

EARS: The system shall owe the seller of an order item the total of the item's commissions, each a fixed amount or a percentage of a stated base amount.

Story: As a seller, I want every commission on an order item worked out the same way and added up, so that I know what the airline owes me for the sale.

Acceptance criteria:

ONE-801.1: Where a commission is a fixed amount, the system shall owe the seller that amount.
ONE-801.2: Where a commission is a percentage of a stated base amount, the system shall owe the seller that share of the base to within one minor unit.
ONE-801.3: When an order item carries several commissions in the item's currency, the system shall owe the seller their total.
ONE-801.4: If the commissions on an order item are not all in the item's currency, then the system shall state no total.
ONE-801.5: Where a commission is a percentage of no more than 100 percent, the system shall never owe more than its base amount.

The guide says several commissions apply without saying how they combine; the model adds them. How a percentage is rounded is a reading of the guide (Rounding). Whether the base is the fare alone or includes taxes, and whether a commission subject to consumption tax is stated gross or net of that tax, are left to the amounts the airline states. The result is the total, or none when the currencies differ.

48.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-801.1	Proven	Trip commissions, Fixed commission
ONE-801.2	Proven	Percentage commission to within a cent, Trip commissions, Rounded commission
ONE-801.3	Proven	Trip commissions, Several commissions add up
ONE-801.4	Proven	Commissions in another currency, Mixed currency commission
ONE-801.5	Proven	Percentage commission within its base

48.2. Guarantees🔗

48.2.1. Fixed commission🔗

guarantee

Rules.OneOrder.Accounting.fixed_commission_owed
  (r : Rules.OneOrder.Accounting.Rounding) (m : Rules.Core.Money) :
  Rules.OneOrder.Accounting.CommissionTerms.value r
      (Rules.OneOrder.Accounting.CommissionTerms.fixed m) =
    m
Rules.OneOrder.Accounting.fixed_commission_owed
  (r : Rules.OneOrder.Accounting.Rounding)
  (m : Rules.Core.Money) :
  Rules.OneOrder.Accounting.CommissionTerms.value
      r
      (Rules.OneOrder.Accounting.CommissionTerms.fixed
        m) =
    m

A fixed commission comes to its amount, under every rounding.

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

Checks acceptance criteria ONE-801.1.

48.2.2. Percentage commission to within a cent🔗

guarantee

Rules.OneOrder.Accounting.percentage_commission_owed
  (r : Rules.OneOrder.Accounting.Rounding) (bp : ℕ)
  (base : Rules.Core.Money) :
  (Rules.OneOrder.Accounting.CommissionTerms.value r
          (Rules.OneOrder.Accounting.CommissionTerms.percentage bp
            base)).currency =
      base.currency ∧
    (Rules.OneOrder.Accounting.CommissionTerms.value r
              (Rules.OneOrder.Accounting.CommissionTerms.percentage bp
                base)).amount *
          10000 <
        bp * base.amount + 10000 ∧
      bp * base.amount <
        (Rules.OneOrder.Accounting.CommissionTerms.value r
                (Rules.OneOrder.Accounting.CommissionTerms.percentage bp
                  base)).amount *
            10000 +
          10000
Rules.OneOrder.Accounting.percentage_commission_owed
  (r : Rules.OneOrder.Accounting.Rounding)
  (bp : ℕ) (base : Rules.Core.Money) :
  (Rules.OneOrder.Accounting.CommissionTerms.value
          r
          (Rules.OneOrder.Accounting.CommissionTerms.percentage
            bp base)).currency =
      base.currency ∧
    (Rules.OneOrder.Accounting.CommissionTerms.value
              r
              (Rules.OneOrder.Accounting.CommissionTerms.percentage
                bp base)).amount *
          10000 <
        bp * base.amount + 10000 ∧
      bp * base.amount <
        (Rules.OneOrder.Accounting.CommissionTerms.value
                r
                (Rules.OneOrder.Accounting.CommissionTerms.percentage
                  bp base)).amount *
            10000 +
          10000

A percentage commission comes to its share of the base, in the base's currency, less than one minor unit away from the exact share, under every rounding.

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

Checks acceptance criteria ONE-801.2.

48.2.3. Several commissions add up🔗

guarantee

Rules.OneOrder.Accounting.commission_total
  (r : Rules.OneOrder.Accounting.Rounding) (c : Rules.Core.Currency)
  (cs : List Rules.OneOrder.Accounting.Commission)
  (h :
    ∀ x ∈ cs,
      (Rules.OneOrder.Accounting.CommissionTerms.value r
            x.terms).currency =
        c) :
  Rules.OneOrder.Accounting.commissionOwed r c cs =
    some
      {
        amount :=
          (List.map
              (fun x ↦
                (Rules.OneOrder.Accounting.CommissionTerms.value r
                    x.terms).amount)
              cs).sum,
        currency := c }
Rules.OneOrder.Accounting.commission_total
  (r : Rules.OneOrder.Accounting.Rounding)
  (c : Rules.Core.Currency)
  (cs :
    List
      Rules.OneOrder.Accounting.Commission)
  (h :
    ∀ x ∈ cs,
      (Rules.OneOrder.Accounting.CommissionTerms.value
            r x.terms).currency =
        c) :
  Rules.OneOrder.Accounting.commissionOwed
      r c cs =
    some
      {
        amount :=
          (List.map
              (fun x ↦
                (Rules.OneOrder.Accounting.CommissionTerms.value
                    r x.terms).amount)
              cs).sum,
        currency := c }

An order item's commissions, all in its currency, come to their total, under every rounding.

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

Checks acceptance criteria ONE-801.3.

48.2.4. Commissions in another currency🔗

guarantee

Rules.OneOrder.Accounting.commission_mixed_currency
  (r : Rules.OneOrder.Accounting.Rounding) (c : Rules.Core.Currency)
  (cs : List Rules.OneOrder.Accounting.Commission)
  (h :
    ∃ x ∈ cs,
      (Rules.OneOrder.Accounting.CommissionTerms.value r
            x.terms).currency ≠
        c) :
  Rules.OneOrder.Accounting.commissionOwed r c cs = none
Rules.OneOrder.Accounting.commission_mixed_currency
  (r : Rules.OneOrder.Accounting.Rounding)
  (c : Rules.Core.Currency)
  (cs :
    List
      Rules.OneOrder.Accounting.Commission)
  (h :
    ∃ x ∈ cs,
      (Rules.OneOrder.Accounting.CommissionTerms.value
            r x.terms).currency ≠
        c) :
  Rules.OneOrder.Accounting.commissionOwed
      r c cs =
    none

An order item with a commission in another currency gets no total, under every rounding.

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

Checks acceptance criteria ONE-801.4.

48.2.5. Percentage commission within its base🔗

guarantee

Rules.OneOrder.Accounting.percentage_within_base
  (r : Rules.OneOrder.Accounting.Rounding) (bp : ℕ)
  (base : Rules.Core.Money) (h : bp ≤ 10000) :
  (Rules.OneOrder.Accounting.CommissionTerms.value r
        (Rules.OneOrder.Accounting.CommissionTerms.percentage bp
          base)).amount ≤
    base.amount
Rules.OneOrder.Accounting.percentage_within_base
  (r : Rules.OneOrder.Accounting.Rounding)
  (bp : ℕ) (base : Rules.Core.Money)
  (h : bp ≤ 10000) :
  (Rules.OneOrder.Accounting.CommissionTerms.value
        r
        (Rules.OneOrder.Accounting.CommissionTerms.percentage
          bp base)).amount ≤
    base.amount

A percentage commission of no more than 100 percent never comes to more than its base, under every rounding.

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

Checks acceptance criteria ONE-801.5.

48.3. Examples🔗

48.3.1. Trip commissions🔗

example

Rules.OneOrder.Accounting.tripCommissions :
  Rules.OneOrder.Accounting.CommissionCase
Rules.OneOrder.Accounting.tripCommissions :
  Rules.OneOrder.Accounting.CommissionCase

Given an order item with a fare of 820.00 EUR and three commissions: a standard commission of 5 percent of the fare, a supplemental commission of 10.00 EUR, and a clearance incentive of 0.5 percent of the fare.

When the commission owed to the seller is worked out.

Then the commissions come to 41.00, 10.00 and 4.10 EUR, and the seller is owed 55.10 EUR.

What Lean computed:

Each: see the table below.
Total: 55.10 EUR

Each:

Amount	Currency
4100	EUR
1000	EUR
410	EUR

Checks acceptance criteria ONE-801.1, ONE-801.2, ONE-801.3.

48.3.2. Rounded commission🔗

example

Rules.OneOrder.Accounting.roundedCommission :
  Rules.OneOrder.Accounting.RoundedCommission
Rules.OneOrder.Accounting.roundedCommission :
  Rules.OneOrder.Accounting.RoundedCommission

Given a standard commission of 5 percent of a fare of 333.30 EUR. The exact share is 16.665 EUR.

When the commission is worked out under each rounding.

Then it is 16.66 EUR rounded down and 16.67 EUR rounded to the nearest cent or up. Each is less than a cent from the exact share.

What Lean computed:

Down: 16.66 EUR
Half up: 16.67 EUR
Up: 16.67 EUR

Checks acceptance criteria ONE-801.2.

48.3.3. Mixed currency commission🔗

example

Rules.OneOrder.Accounting.mixedCurrencyCommission :
  Rules.OneOrder.Accounting.CommissionCase
Rules.OneOrder.Accounting.mixedCurrencyCommission :
  Rules.OneOrder.Accounting.CommissionCase

Given an order item priced in euros with a standard commission of 41.00 EUR and a supplemental commission stated as 10.00 USD.

When the commission owed to the seller is worked out.

Then there is no total: the commissions are not all in the item's currency.

What Lean computed:

Each: see the table below.
Total: none

Each:

Amount	Currency
4100	EUR
1000	USD

Checks acceptance criteria ONE-801.4.