Verified Air

35. Totalling a price from its parts🔗

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

rule

Rules.OneOrder.Offers.priceTotal (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts) :
  Except Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal
Rules.OneOrder.Offers.priceTotal
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts) :
  Except
    Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal

EARS: When an airline states a price with its parts, the system shall total the price as its base amount plus its surcharges, fees, taxes and the consumption tax not included in it.

Story: As a seller, I want every price to add up from its parts, so that the total I show the customer is the total the airline charges.

Acceptance criteria:

ONE-506.1: If the amounts of a price are not all in one currency, then the system shall reject the price.
ONE-506.2: If a price's discount is larger than its amount before discounts, then the system shall reject the price.
ONE-506.3: The system shall state a price's base amount as its amount before discounts less its discount.
ONE-506.4: The system shall make a tax summary's total the sum of its entries.
ONE-506.5: The system shall make a price's total its base amount plus its surcharges, its fees, its tax summary total and the consumption tax not included in it.
ONE-506.6: When a consumption tax line is marked as not included in the price, the system shall add its tax to the price's total.

Where the consumption tax not included comes from is a reading of the guide (ExcludedTax).

35.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-506.1	Proven	Mixed-currency prices are rejected, Price in two currencies
ONE-506.2	Proven	Discount above the base is rejected, Discount above base
ONE-506.3	Proven	Price that adds up, Base amount after discounts
ONE-506.4	Proven	Tax summary total from its entries, Price that adds up
ONE-506.5	Proven	Price that adds up, Excluded tax readings, Total from base, surcharges, fees and taxes
ONE-506.6	Open	Price total from its parts, Excluded tax readings

35.2. Guarantees🔗

35.2.1. Mixed-currency prices are rejected🔗

guarantee

Rules.OneOrder.Offers.price_rejects_mixed_currency
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (h : ∃ m ∈ p.amounts, m.currency ≠ p.beforeDiscount.currency) :
  Rules.OneOrder.Offers.priceTotal x p =
    Except.error Rules.OneOrder.Offers.PriceRejection.mixedCurrency
Rules.OneOrder.Offers.price_rejects_mixed_currency
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (h :
    ∃ m ∈ p.amounts,
      m.currency ≠
        p.beforeDiscount.currency) :
  Rules.OneOrder.Offers.priceTotal x p =
    Except.error
      Rules.OneOrder.Offers.PriceRejection.mixedCurrency

A price with an amount in a currency other than that of its amount before discounts is rejected.

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

Checks acceptance criteria ONE-506.1.

35.2.2. Discount above the base is rejected🔗

guarantee

Rules.OneOrder.Offers.price_rejects_large_discount
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (h : p.beforeDiscount.amount < p.discount.amount)
  (t : Rules.OneOrder.Offers.PriceTotal) :
  Rules.OneOrder.Offers.priceTotal x p ≠ Except.ok t
Rules.OneOrder.Offers.price_rejects_large_discount
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (h :
    p.beforeDiscount.amount <
      p.discount.amount)
  (t : Rules.OneOrder.Offers.PriceTotal) :
  Rules.OneOrder.Offers.priceTotal x p ≠
    Except.ok t

A price whose discount is larger than its amount before discounts is never totalled.

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

Checks acceptance criteria ONE-506.2.

35.2.3. Base amount after discounts🔗

guarantee

Rules.OneOrder.Offers.price_base (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h : Rules.OneOrder.Offers.priceTotal x p = Except.ok t) :
  t.base.amount = p.beforeDiscount.amount - p.discount.amount ∧
    p.discount.amount ≤ p.beforeDiscount.amount
Rules.OneOrder.Offers.price_base
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h :
    Rules.OneOrder.Offers.priceTotal x p =
      Except.ok t) :
  t.base.amount =
      p.beforeDiscount.amount -
        p.discount.amount ∧
    p.discount.amount ≤
      p.beforeDiscount.amount

A totalled price's base amount is its amount before discounts less its discount, and the discount is no larger than that amount.

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

Checks acceptance criteria ONE-506.3.

35.2.4. Tax summary total from its entries🔗

guarantee

Rules.OneOrder.Offers.price_tax_total
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h : Rules.OneOrder.Offers.priceTotal x p = Except.ok t) :
  t.taxTotal.amount =
    Rules.OneOrder.Offers.sumOf (List.map (fun x ↦ x.amount) p.taxes)
Rules.OneOrder.Offers.price_tax_total
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h :
    Rules.OneOrder.Offers.priceTotal x p =
      Except.ok t) :
  t.taxTotal.amount =
    Rules.OneOrder.Offers.sumOf
      (List.map (fun x ↦ x.amount)
        p.taxes)

A totalled price's tax summary total is the sum of its entries.

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

Checks acceptance criteria ONE-506.4.

35.2.5. Total from base, surcharges, fees and taxes🔗

guarantee

Rules.OneOrder.Offers.price_total_from_parts
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h : Rules.OneOrder.Offers.priceTotal x p = Except.ok t) :
  t.total.amount =
      t.base.amount + Rules.OneOrder.Offers.sumOf p.surcharges +
            Rules.OneOrder.Offers.sumOf
              (List.map (fun x ↦ x.amount) p.fees) +
          t.taxTotal.amount +
        t.excludedTax.amount ∧
    t.total.currency = p.beforeDiscount.currency
Rules.OneOrder.Offers.price_total_from_parts
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h :
    Rules.OneOrder.Offers.priceTotal x p =
      Except.ok t) :
  t.total.amount =
      t.base.amount +
              Rules.OneOrder.Offers.sumOf
                p.surcharges +
            Rules.OneOrder.Offers.sumOf
              (List.map (fun x ↦ x.amount)
                p.fees) +
          t.taxTotal.amount +
        t.excludedTax.amount ∧
    t.total.currency =
      p.beforeDiscount.currency

A totalled price's total is its base amount plus its surcharges, its fees, its tax summary total and the consumption tax not included in it, all in the price's currency.

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

Checks acceptance criteria ONE-506.5.

35.2.6. Price total from its parts🔗

guarantee

Rules.OneOrder.Offers.price_adds_excluded_lines
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h : Rules.OneOrder.Offers.priceTotal x p = Except.ok t) :
  t.excludedTax.amount = p.lineExcluded
Rules.OneOrder.Offers.price_adds_excluded_lines
  (x : Rules.OneOrder.Offers.ExcludedTax)
  (p : Rules.OneOrder.Offers.PriceParts)
  (t : Rules.OneOrder.Offers.PriceTotal)
  (h :
    Rules.OneOrder.Offers.priceTotal x p =
      Except.ok t) :
  t.excludedTax.amount = p.lineExcluded

A totalled price adds the tax of every consumption tax line marked as not included in it.

Open question for the business. The guide's examples state both the tax lines and a total of excluded tax, and one example marks every HST line as not included while stating an excluded total of zero. Under the reading that trusts the stated total, that tax is left out of the price's total. The example excludedTaxReadings shows the two readings differ by the whole tax. When a line marked as not included and the stated total of excluded tax disagree, which one does the price's total follow?

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

Checks acceptance criteria ONE-506.6.

35.3. Examples🔗

35.3.1. Price in two currencies🔗

example

Rules.OneOrder.Offers.priceInTwoCurrencies :
  Except Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal
Rules.OneOrder.Offers.priceInTwoCurrencies :
  Except
    Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal

Given a price whose gross amount is in pounds and whose consumption tax is in euros. The guide's Australian example states its gross amount in Australian dollars and its tax in euros; the model has no Australian dollar, so pounds stand in.

When the price is totalled.

Then it is rejected for mixing currencies.

What Lean computed:

Rejected: mixed currency.

Checks acceptance criteria ONE-506.1.

35.3.2. Discount above base🔗

example

Rules.OneOrder.Offers.discountAboveBase :
  Except Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal
Rules.OneOrder.Offers.discountAboveBase :
  Except
    Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal

Given a price of 100.00 EUR before a discount of 120.00 EUR.

When the price is totalled.

Then it is rejected: the discount is larger than the amount before discounts.

What Lean computed:

Rejected: discount above base.

Checks acceptance criteria ONE-506.2.

35.3.3. Price that adds up🔗

example

Rules.OneOrder.Offers.priceThatAddsUp :
  Except Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal
Rules.OneOrder.Offers.priceThatAddsUp :
  Except
    Rules.OneOrder.Offers.PriceRejection
    Rules.OneOrder.Offers.PriceTotal

Given a price of 100.00 EUR before a discount of 5.00 EUR, with a tax of 20.00 EUR. The guide's one example that adds up has a base of 95.00 and a tax of 20.00 for a total of 115.00.

When the price is totalled.

Then the base amount is 95.00 EUR, the tax summary total 20.00 EUR and the total 115.00 EUR.

What Lean computed:

Accepted. The result:

Base: 95.00 EUR
Tax total: 20.00 EUR
Excluded tax: 0.00 EUR
Total: 115.00 EUR

Checks acceptance criteria ONE-506.3, ONE-506.4, ONE-506.5.

35.3.4. Excluded tax readings🔗

example

Rules.OneOrder.Offers.excludedTaxReadings :
  List Rules.OneOrder.Offers.ExcludedTaxRow
Rules.OneOrder.Offers.excludedTaxReadings :
  List
    Rules.OneOrder.Offers.ExcludedTaxRow

Given a base of 452.15 USD with an HST line of 58.78 USD marked as not included in the price, and a stated total of excluded tax of zero.

When the price is totalled under each reading of the guide.

Then taking the excluded tax from the lines gives a total of 510.93 USD. Trusting the stated total gives 452.15 USD, leaving out the 58.78 USD of HST the line says is not included.

What Lean computed:

Reading	Excluded tax	Total
lines	58.78 USD	510.93 USD
stated total	0.00 USD	452.15 USD

Checks acceptance criteria ONE-506.5, ONE-506.6.

35.4. Open question🔗

The guarantee Price total from its parts is open: the example Excluded tax readings shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.